Metamath Proof Explorer

Theorem genpnmax

Description: An operation on positive reals has no largest member. (Contributed by NM, 10-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. )
genpnmax.2 
|- ( v e. Q. -> ( z  ( v G z )
genpnmax.3 
|- ( z G w ) = ( w G z )
Assertion genpnmax 
|- ( ( A e. P. /\ B e. P. ) -> ( f e. ( A F B ) -> E. x e. ( A F B ) f

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 genpnmax.2 
 |-  ( v e. Q. -> ( z  ( v G z )
4 genpnmax.3 
 |-  ( z G w ) = ( w G z )
5 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 ) ) )
6 prnmax 
 |-  ( ( A e. P. /\ g e. A ) -> E. y e. A g
7 6 adantr 
 |-  ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) -> E. y e. A g
8 1 2 genpprecl 
 |-  ( ( A e. P. /\ B e. P. ) -> ( ( y e. A /\ h e. B ) -> ( y G h ) e. ( A F B ) ) )
9 8 exp4b 
 |-  ( A e. P. -> ( B e. P. -> ( y e. A -> ( h e. B -> ( y G h ) e. ( A F B ) ) ) ) )
10 9 com34 
 |-  ( A e. P. -> ( B e. P. -> ( h e. B -> ( y e. A -> ( y G h ) e. ( A F B ) ) ) ) )
11 10 imp32 
 |-  ( ( A e. P. /\ ( B e. P. /\ h e. B ) ) -> ( y e. A -> ( y G h ) e. ( A F B ) ) )
12 elprnq 
 |-  ( ( B e. P. /\ h e. B ) -> h e. Q. )
13 vex 
 |-  g e. _V
14 vex 
 |-  y e. _V
15 vex 
 |-  h e. _V
16 13 14 3 15 4 caovord2 
 |-  ( h e. Q. -> ( g  ( g G h )
17 16 biimpd 
 |-  ( h e. Q. -> ( g  ( g G h )
18 12 17 syl 
 |-  ( ( B e. P. /\ h e. B ) -> ( g  ( g G h )
19 18 adantl 
 |-  ( ( A e. P. /\ ( B e. P. /\ h e. B ) ) -> ( g  ( g G h )
20 11 19 anim12d 
 |-  ( ( A e. P. /\ ( B e. P. /\ h e. B ) ) -> ( ( y e. A /\ g  ( ( y G h ) e. ( A F B ) /\ ( g G h )
21 breq2 
 |-  ( x = ( y G h ) -> ( ( g G h )  ( g G h )
22 21 rspcev 
 |-  ( ( ( y G h ) e. ( A F B ) /\ ( g G h )  E. x e. ( A F B ) ( g G h )
23 20 22 syl6 
 |-  ( ( A e. P. /\ ( B e. P. /\ h e. B ) ) -> ( ( y e. A /\ g  E. x e. ( A F B ) ( g G h )
24 23 adantlr 
 |-  ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) -> ( ( y e. A /\ g  E. x e. ( A F B ) ( g G h )
25 24 expd 
 |-  ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) -> ( y e. A -> ( g  E. x e. ( A F B ) ( g G h )
26 25 rexlimdv 
 |-  ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) -> ( E. y e. A g  E. x e. ( A F B ) ( g G h )
27 7 26 mpd 
 |-  ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) -> E. x e. ( A F B ) ( g G h )
28 27 an4s 
 |-  ( ( ( A e. P. /\ B e. P. ) /\ ( g e. A /\ h e. B ) ) -> E. x e. ( A F B ) ( g G h )
29 breq1 
 |-  ( f = ( g G h ) -> ( f  ( g G h )
30 29 rexbidv 
 |-  ( f = ( g G h ) -> ( E. x e. ( A F B ) f  E. x e. ( A F B ) ( g G h )
31 28 30 imbitrrid 
 |-  ( f = ( g G h ) -> ( ( ( A e. P. /\ B e. P. ) /\ ( g e. A /\ h e. B ) ) -> E. x e. ( A F B ) f
32 31 expdcom 
 |-  ( ( A e. P. /\ B e. P. ) -> ( ( g e. A /\ h e. B ) -> ( f = ( g G h ) -> E. x e. ( A F B ) f
33 32 rexlimdvv 
 |-  ( ( A e. P. /\ B e. P. ) -> ( E. g e. A E. h e. B f = ( g G h ) -> E. x e. ( A F B ) f
34 5 33 sylbid 
 |-  ( ( A e. P. /\ B e. P. ) -> ( f e. ( A F B ) -> E. x e. ( A F B ) f