Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  genpnmax Structured version   Visualization version   GIF version

Theorem genpnmax 9708
 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.)
Hypotheses
Ref Expression
genp.1 𝐹 = (𝑤P, 𝑣P ↦ {𝑥 ∣ ∃𝑦𝑤𝑧𝑣 𝑥 = (𝑦𝐺𝑧)})
genp.2 ((𝑦Q𝑧Q) → (𝑦𝐺𝑧) ∈ Q)
genpnmax.2 (𝑣Q → (𝑧 <Q 𝑤 ↔ (𝑣𝐺𝑧) <Q (𝑣𝐺𝑤)))
genpnmax.3 (𝑧𝐺𝑤) = (𝑤𝐺𝑧)
Assertion
Ref Expression
genpnmax ((𝐴P𝐵P) → (𝑓 ∈ (𝐴𝐹𝐵) → ∃𝑥 ∈ (𝐴𝐹𝐵)𝑓 <Q 𝑥))
Distinct variable groups:   𝑥,𝑦,𝑧,𝑓,𝐴   𝑥,𝐵,𝑦,𝑧,𝑓   𝑥,𝑤,𝑣,𝐺,𝑦,𝑧,𝑓   𝑓,𝐹,𝑥,𝑦
Allowed substitution hints:   𝐴(𝑤,𝑣)   𝐵(𝑤,𝑣)   𝐹(𝑧,𝑤,𝑣)

Proof of Theorem genpnmax
Dummy variables 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 genp.1 . . 3 𝐹 = (𝑤P, 𝑣P ↦ {𝑥 ∣ ∃𝑦𝑤𝑧𝑣 𝑥 = (𝑦𝐺𝑧)})
2 genp.2 . . 3 ((𝑦Q𝑧Q) → (𝑦𝐺𝑧) ∈ Q)
31, 2genpelv 9701 . 2 ((𝐴P𝐵P) → (𝑓 ∈ (𝐴𝐹𝐵) ↔ ∃𝑔𝐴𝐵 𝑓 = (𝑔𝐺)))
4 prnmax 9696 . . . . . . . 8 ((𝐴P𝑔𝐴) → ∃𝑦𝐴 𝑔 <Q 𝑦)
54adantr 480 . . . . . . 7 (((𝐴P𝑔𝐴) ∧ (𝐵P𝐵)) → ∃𝑦𝐴 𝑔 <Q 𝑦)
61, 2genpprecl 9702 . . . . . . . . . . . . . . 15 ((𝐴P𝐵P) → ((𝑦𝐴𝐵) → (𝑦𝐺) ∈ (𝐴𝐹𝐵)))
76exp4b 630 . . . . . . . . . . . . . 14 (𝐴P → (𝐵P → (𝑦𝐴 → (𝐵 → (𝑦𝐺) ∈ (𝐴𝐹𝐵)))))
87com34 89 . . . . . . . . . . . . 13 (𝐴P → (𝐵P → (𝐵 → (𝑦𝐴 → (𝑦𝐺) ∈ (𝐴𝐹𝐵)))))
98imp32 448 . . . . . . . . . . . 12 ((𝐴P ∧ (𝐵P𝐵)) → (𝑦𝐴 → (𝑦𝐺) ∈ (𝐴𝐹𝐵)))
10 elprnq 9692 . . . . . . . . . . . . . 14 ((𝐵P𝐵) → Q)
11 vex 3176 . . . . . . . . . . . . . . . 16 𝑔 ∈ V
12 vex 3176 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
13 genpnmax.2 . . . . . . . . . . . . . . . 16 (𝑣Q → (𝑧 <Q 𝑤 ↔ (𝑣𝐺𝑧) <Q (𝑣𝐺𝑤)))
14 vex 3176 . . . . . . . . . . . . . . . 16 ∈ V
15 genpnmax.3 . . . . . . . . . . . . . . . 16 (𝑧𝐺𝑤) = (𝑤𝐺𝑧)
1611, 12, 13, 14, 15caovord2 6744 . . . . . . . . . . . . . . 15 (Q → (𝑔 <Q 𝑦 ↔ (𝑔𝐺) <Q (𝑦𝐺)))
1716biimpd 218 . . . . . . . . . . . . . 14 (Q → (𝑔 <Q 𝑦 → (𝑔𝐺) <Q (𝑦𝐺)))
1810, 17syl 17 . . . . . . . . . . . . 13 ((𝐵P𝐵) → (𝑔 <Q 𝑦 → (𝑔𝐺) <Q (𝑦𝐺)))
1918adantl 481 . . . . . . . . . . . 12 ((𝐴P ∧ (𝐵P𝐵)) → (𝑔 <Q 𝑦 → (𝑔𝐺) <Q (𝑦𝐺)))
209, 19anim12d 584 . . . . . . . . . . 11 ((𝐴P ∧ (𝐵P𝐵)) → ((𝑦𝐴𝑔 <Q 𝑦) → ((𝑦𝐺) ∈ (𝐴𝐹𝐵) ∧ (𝑔𝐺) <Q (𝑦𝐺))))
21 breq2 4587 . . . . . . . . . . . 12 (𝑥 = (𝑦𝐺) → ((𝑔𝐺) <Q 𝑥 ↔ (𝑔𝐺) <Q (𝑦𝐺)))
2221rspcev 3282 . . . . . . . . . . 11 (((𝑦𝐺) ∈ (𝐴𝐹𝐵) ∧ (𝑔𝐺) <Q (𝑦𝐺)) → ∃𝑥 ∈ (𝐴𝐹𝐵)(𝑔𝐺) <Q 𝑥)
2320, 22syl6 34 . . . . . . . . . 10 ((𝐴P ∧ (𝐵P𝐵)) → ((𝑦𝐴𝑔 <Q 𝑦) → ∃𝑥 ∈ (𝐴𝐹𝐵)(𝑔𝐺) <Q 𝑥))
2423adantlr 747 . . . . . . . . 9 (((𝐴P𝑔𝐴) ∧ (𝐵P𝐵)) → ((𝑦𝐴𝑔 <Q 𝑦) → ∃𝑥 ∈ (𝐴𝐹𝐵)(𝑔𝐺) <Q 𝑥))
2524expd 451 . . . . . . . 8 (((𝐴P𝑔𝐴) ∧ (𝐵P𝐵)) → (𝑦𝐴 → (𝑔 <Q 𝑦 → ∃𝑥 ∈ (𝐴𝐹𝐵)(𝑔𝐺) <Q 𝑥)))
2625rexlimdv 3012 . . . . . . 7 (((𝐴P𝑔𝐴) ∧ (𝐵P𝐵)) → (∃𝑦𝐴 𝑔 <Q 𝑦 → ∃𝑥 ∈ (𝐴𝐹𝐵)(𝑔𝐺) <Q 𝑥))
275, 26mpd 15 . . . . . 6 (((𝐴P𝑔𝐴) ∧ (𝐵P𝐵)) → ∃𝑥 ∈ (𝐴𝐹𝐵)(𝑔𝐺) <Q 𝑥)
2827an4s 865 . . . . 5 (((𝐴P𝐵P) ∧ (𝑔𝐴𝐵)) → ∃𝑥 ∈ (𝐴𝐹𝐵)(𝑔𝐺) <Q 𝑥)
29 breq1 4586 . . . . . 6 (𝑓 = (𝑔𝐺) → (𝑓 <Q 𝑥 ↔ (𝑔𝐺) <Q 𝑥))
3029rexbidv 3034 . . . . 5 (𝑓 = (𝑔𝐺) → (∃𝑥 ∈ (𝐴𝐹𝐵)𝑓 <Q 𝑥 ↔ ∃𝑥 ∈ (𝐴𝐹𝐵)(𝑔𝐺) <Q 𝑥))
3128, 30syl5ibr 235 . . . 4 (𝑓 = (𝑔𝐺) → (((𝐴P𝐵P) ∧ (𝑔𝐴𝐵)) → ∃𝑥 ∈ (𝐴𝐹𝐵)𝑓 <Q 𝑥))
3231expdcom 454 . . 3 ((𝐴P𝐵P) → ((𝑔𝐴𝐵) → (𝑓 = (𝑔𝐺) → ∃𝑥 ∈ (𝐴𝐹𝐵)𝑓 <Q 𝑥)))
3332rexlimdvv 3019 . 2 ((𝐴P𝐵P) → (∃𝑔𝐴𝐵 𝑓 = (𝑔𝐺) → ∃𝑥 ∈ (𝐴𝐹𝐵)𝑓 <Q 𝑥))
343, 33sylbid 229 1 ((𝐴P𝐵P) → (𝑓 ∈ (𝐴𝐹𝐵) → ∃𝑥 ∈ (𝐴𝐹𝐵)𝑓 <Q 𝑥))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  {cab 2596  ∃wrex 2897   class class class wbr 4583  (class class class)co 6549   ↦ cmpt2 6551  Qcnq 9553
 Copyright terms: Public domain W3C validator