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∈𝑷,v∈𝑷⟼x|∃y∈w∃z∈vx=yGz
genp.2 ⊢y∈𝑸∧z∈𝑸→yGz∈𝑸
genpnmax.2 ⊢v∈𝑸→z<𝑸w↔vGz<𝑸vGw
genpnmax.3 ⊢zGw=wGz
Assertion genpnmax ⊢A∈𝑷∧B∈𝑷→f∈AFB→∃x∈AFBf<𝑸x

Proof

Step Hyp Ref Expression
1 genp.1 ⊢F=w∈𝑷,v∈𝑷⟼x|∃y∈w∃z∈vx=yGz
2 genp.2 ⊢y∈𝑸∧z∈𝑸→yGz∈𝑸
3 genpnmax.2 ⊢v∈𝑸→z<𝑸w↔vGz<𝑸vGw
4 genpnmax.3 ⊢zGw=wGz
5 1 2 genpelv ⊢A∈𝑷∧B∈𝑷→f∈AFB↔∃g∈A∃h∈Bf=gGh
6 prnmax ⊢A∈𝑷∧g∈A→∃y∈Ag<𝑸y
7 6 adantr ⊢A∈𝑷∧g∈A∧B∈𝑷∧h∈B→∃y∈Ag<𝑸y
8 1 2 genpprecl ⊢A∈𝑷∧B∈𝑷→y∈A∧h∈B→yGh∈AFB
9 8 exp4b ⊢A∈𝑷→B∈𝑷→y∈A→h∈B→yGh∈AFB
10 9 com34 ⊢A∈𝑷→B∈𝑷→h∈B→y∈A→yGh∈AFB
11 10 imp32 ⊢A∈𝑷∧B∈𝑷∧h∈B→y∈A→yGh∈AFB
12 elprnq ⊢B∈𝑷∧h∈B→h∈𝑸
13 vex ⊢g∈V
14 vex ⊢y∈V
15 vex ⊢h∈V
16 13 14 3 15 4 caovord2 ⊢h∈𝑸→g<𝑸y↔gGh<𝑸yGh
17 16 biimpd ⊢h∈𝑸→g<𝑸y→gGh<𝑸yGh
18 12 17 syl ⊢B∈𝑷∧h∈B→g<𝑸y→gGh<𝑸yGh
19 18 adantl ⊢A∈𝑷∧B∈𝑷∧h∈B→g<𝑸y→gGh<𝑸yGh
20 11 19 anim12d ⊢A∈𝑷∧B∈𝑷∧h∈B→y∈A∧g<𝑸y→yGh∈AFB∧gGh<𝑸yGh
21 breq2 ⊢x=yGh→gGh<𝑸x↔gGh<𝑸yGh
22 21 rspcev ⊢yGh∈AFB∧gGh<𝑸yGh→∃x∈AFBgGh<𝑸x
23 20 22 syl6 ⊢A∈𝑷∧B∈𝑷∧h∈B→y∈A∧g<𝑸y→∃x∈AFBgGh<𝑸x
24 23 adantlr ⊢A∈𝑷∧g∈A∧B∈𝑷∧h∈B→y∈A∧g<𝑸y→∃x∈AFBgGh<𝑸x
25 24 expd ⊢A∈𝑷∧g∈A∧B∈𝑷∧h∈B→y∈A→g<𝑸y→∃x∈AFBgGh<𝑸x
26 25 rexlimdv ⊢A∈𝑷∧g∈A∧B∈𝑷∧h∈B→∃y∈Ag<𝑸y→∃x∈AFBgGh<𝑸x
27 7 26 mpd ⊢A∈𝑷∧g∈A∧B∈𝑷∧h∈B→∃x∈AFBgGh<𝑸x
28 27 an4s ⊢A∈𝑷∧B∈𝑷∧g∈A∧h∈B→∃x∈AFBgGh<𝑸x
29 breq1 ⊢f=gGh→f<𝑸x↔gGh<𝑸x
30 29 rexbidv ⊢f=gGh→∃x∈AFBf<𝑸x↔∃x∈AFBgGh<𝑸x
31 28 30 imbitrrid ⊢f=gGh→A∈𝑷∧B∈𝑷∧g∈A∧h∈B→∃x∈AFBf<𝑸x
32 31 expdcom ⊢A∈𝑷∧B∈𝑷→g∈A∧h∈B→f=gGh→∃x∈AFBf<𝑸x
33 32 rexlimdvv ⊢A∈𝑷∧B∈𝑷→∃g∈A∃h∈Bf=gGh→∃x∈AFBf<𝑸x
34 5 33 sylbid ⊢A∈𝑷∧B∈𝑷→f∈AFB→∃x∈AFBf<𝑸x