This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem genpdm

Description: Domain of general operation on positive reals. (Contributed by NM, 18-Nov-1995) (Revised by Mario Carneiro, 17-Nov-2014) (New usage is discouraged.)

Ref Expression
Hypotheses genp.1 
|- F = ( w e. P. , v e. P. |-> { x | E. y e. w E. z e. v x = ( y G z ) } )
genp.2 
|- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )
Assertion genpdm 
|- dom F = ( P. X. P. )

Proof

Step Hyp Ref Expression
1 genp.1 
 |-  F = ( w e. P. , v e. P. |-> { x | E. y e. w E. z e. v x = ( y G z ) } )
2 genp.2 
 |-  ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )
3 elprnq 
 |-  ( ( w e. P. /\ y e. w ) -> y e. Q. )
4 elprnq 
 |-  ( ( v e. P. /\ z e. v ) -> z e. Q. )
5 eleq1 
 |-  ( x = ( y G z ) -> ( x e. Q. <-> ( y G z ) e. Q. ) )
6 2 5 syl5ibrcom 
 |-  ( ( y e. Q. /\ z e. Q. ) -> ( x = ( y G z ) -> x e. Q. ) )
7 3 4 6 syl2an 
 |-  ( ( ( w e. P. /\ y e. w ) /\ ( v e. P. /\ z e. v ) ) -> ( x = ( y G z ) -> x e. Q. ) )
8 7 an4s 
 |-  ( ( ( w e. P. /\ v e. P. ) /\ ( y e. w /\ z e. v ) ) -> ( x = ( y G z ) -> x e. Q. ) )
9 8 rexlimdvva 
 |-  ( ( w e. P. /\ v e. P. ) -> ( E. y e. w E. z e. v x = ( y G z ) -> x e. Q. ) )
10 9 abssdv 
 |-  ( ( w e. P. /\ v e. P. ) -> { x | E. y e. w E. z e. v x = ( y G z ) } C_ Q. )
11 nqex 
 |-  Q. e. _V
12 ssexg 
 |-  ( ( { x | E. y e. w E. z e. v x = ( y G z ) } C_ Q. /\ Q. e. _V ) -> { x | E. y e. w E. z e. v x = ( y G z ) } e. _V )
13 10 11 12 sylancl 
 |-  ( ( w e. P. /\ v e. P. ) -> { x | E. y e. w E. z e. v x = ( y G z ) } e. _V )
14 13 rgen2 
 |-  A. w e. P. A. v e. P. { x | E. y e. w E. z e. v x = ( y G z ) } e. _V
15 1 fnmpo 
 |-  ( A. w e. P. A. v e. P. { x | E. y e. w E. z e. v x = ( y G z ) } e. _V -> F Fn ( P. X. P. ) )
16 fndm 
 |-  ( F Fn ( P. X. P. ) -> dom F = ( P. X. P. ) )
17 14 15 16 mp2b 
 |-  dom F = ( P. X. P. )