Metamath Proof Explorer

Theorem genpcd

Description: Downward closure of an operation on positive reals. (Contributed by NM, 13-Mar-1996) (Revised by Mario Carneiro, 12-Jun-2013) (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. )
genpcd.2 
|- ( ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) /\ x e. Q. ) -> ( x  x e. ( A F B ) ) )
Assertion genpcd 
|- ( ( A e. P. /\ B e. P. ) -> ( f e. ( A F B ) -> ( x  x e. ( A F B ) ) ) )

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 genpcd.2 
 |-  ( ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) /\ x e. Q. ) -> ( x  x e. ( A F B ) ) )
4 ltrelnq 
 |-
5 4 brel 
 |-  ( x  ( x e. Q. /\ f e. Q. ) )
6 5 simpld 
 |-  ( x  x e. Q. )
7 1 2 genpelv 
 |-  ( ( A e. P. /\ B e. P. ) -> ( f e. ( A F B ) <-> E. g e. A E. h e. B f = ( g G h ) ) )
8 7 adantr 
 |-  ( ( ( A e. P. /\ B e. P. ) /\ x e. Q. ) -> ( f e. ( A F B ) <-> E. g e. A E. h e. B f = ( g G h ) ) )
9 breq2 
 |-  ( f = ( g G h ) -> ( x  x
10 9 biimpd 
 |-  ( f = ( g G h ) -> ( x  x
11 10 3 sylan9r 
 |-  ( ( ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) /\ x e. Q. ) /\ f = ( g G h ) ) -> ( x  x e. ( A F B ) ) )
12 11 exp31 
 |-  ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) -> ( x e. Q. -> ( f = ( g G h ) -> ( x  x e. ( A F B ) ) ) ) )
13 12 an4s 
 |-  ( ( ( A e. P. /\ B e. P. ) /\ ( g e. A /\ h e. B ) ) -> ( x e. Q. -> ( f = ( g G h ) -> ( x  x e. ( A F B ) ) ) ) )
14 13 impancom 
 |-  ( ( ( A e. P. /\ B e. P. ) /\ x e. Q. ) -> ( ( g e. A /\ h e. B ) -> ( f = ( g G h ) -> ( x  x e. ( A F B ) ) ) ) )
15 14 rexlimdvv 
 |-  ( ( ( A e. P. /\ B e. P. ) /\ x e. Q. ) -> ( E. g e. A E. h e. B f = ( g G h ) -> ( x  x e. ( A F B ) ) ) )
16 8 15 sylbid 
 |-  ( ( ( A e. P. /\ B e. P. ) /\ x e. Q. ) -> ( f e. ( A F B ) -> ( x  x e. ( A F B ) ) ) )
17 16 ex 
 |-  ( ( A e. P. /\ B e. P. ) -> ( x e. Q. -> ( f e. ( A F B ) -> ( x  x e. ( A F B ) ) ) ) )
18 6 17 syl5 
 |-  ( ( A e. P. /\ B e. P. ) -> ( x  ( f e. ( A F B ) -> ( x  x e. ( A F B ) ) ) ) )
19 18 com34 
 |-  ( ( A e. P. /\ B e. P. ) -> ( x  ( x  ( f e. ( A F B ) -> x e. ( A F B ) ) ) ) )
20 19 pm2.43d 
 |-  ( ( A e. P. /\ B e. P. ) -> ( x  ( f e. ( A F B ) -> x e. ( A F B ) ) ) )
21 20 com23 
 |-  ( ( A e. P. /\ B e. P. ) -> ( f e. ( A F B ) -> ( x  x e. ( A F B ) ) ) )