Hi Jon & Benoît,
I've created the deduction version of that theorem
<https://github.com/metamath/set.mm/pull/925> (whatever we choose to
name it). It is not a particularly hard task, just a bit long and a bit
boring as explained by Benoît. This is typically the kind of task that
could be easily automated.
About this:
h1::subarea.1 |- A e. dom area
h2::subarea.2 |- C C_ RR
h3::subarea.3 |- B = { <. x , y >. | ( <. x , y >. e. A /\ x e.
C ) }
!qed:: |- B e. dom area
I believe what you need is
h1::subarea.1 |- A e. dom area
h2::subarea.2 |- ( x e. dom A -> C C_ RR )
h3::subarea.3 |- B = { <. x , y >. | ( <. x , y >. e. A /\ y e.
C ) }
!qed:: |- B e. dom area
Also, why not try directly with the deduction version this time? ;-)
(or at least the closed version)
BR,
_
Thierry
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/a3556da2-4a7f-7e81-2bdd-f8662c8a8aa7%40gmx.net.
