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. )