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

Theorem axpre-sup 10594
Description: A nonempty, bounded-above set of reals has a supremum. Axiom 22 of 22 for real and complex numbers, derived from ZF set theory. Note: The more general version with ordering on extended reals is axsup 10719. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-sup 10618. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.)
Assertion
Ref Expression
axpre-sup ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦 < 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
Distinct variable group:   𝑥,𝑦,𝑧,𝐴

Proof of Theorem axpre-sup
Dummy variables 𝑤 𝑣 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elreal2 10557 . . . . . . 7 (𝑥 ∈ ℝ ↔ ((1st𝑥) ∈ R𝑥 = ⟨(1st𝑥), 0R⟩))
21simplbi 500 . . . . . 6 (𝑥 ∈ ℝ → (1st𝑥) ∈ R)
32adantl 484 . . . . 5 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ℝ) → (1st𝑥) ∈ R)
4 fo1st 7712 . . . . . . . . . . . 12 1st :V–onto→V
5 fof 6593 . . . . . . . . . . . 12 (1st :V–onto→V → 1st :V⟶V)
6 ffn 6517 . . . . . . . . . . . 12 (1st :V⟶V → 1st Fn V)
74, 5, 6mp2b 10 . . . . . . . . . . 11 1st Fn V
8 ssv 3994 . . . . . . . . . . 11 𝐴 ⊆ V
9 fvelimab 6740 . . . . . . . . . . 11 ((1st Fn V ∧ 𝐴 ⊆ V) → (𝑤 ∈ (1st𝐴) ↔ ∃𝑦𝐴 (1st𝑦) = 𝑤))
107, 8, 9mp2an 690 . . . . . . . . . 10 (𝑤 ∈ (1st𝐴) ↔ ∃𝑦𝐴 (1st𝑦) = 𝑤)
11 r19.29 3257 . . . . . . . . . . . 12 ((∀𝑦𝐴 𝑦 < 𝑥 ∧ ∃𝑦𝐴 (1st𝑦) = 𝑤) → ∃𝑦𝐴 (𝑦 < 𝑥 ∧ (1st𝑦) = 𝑤))
12 ssel2 3965 . . . . . . . . . . . . . . . . 17 ((𝐴 ⊆ ℝ ∧ 𝑦𝐴) → 𝑦 ∈ ℝ)
13 ltresr2 10566 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑦 < 𝑥 ↔ (1st𝑦) <R (1st𝑥)))
14 breq1 5072 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑦) = 𝑤 → ((1st𝑦) <R (1st𝑥) ↔ 𝑤 <R (1st𝑥)))
1513, 14sylan9bb 512 . . . . . . . . . . . . . . . . . . 19 (((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) ∧ (1st𝑦) = 𝑤) → (𝑦 < 𝑥𝑤 <R (1st𝑥)))
1615biimpd 231 . . . . . . . . . . . . . . . . . 18 (((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) ∧ (1st𝑦) = 𝑤) → (𝑦 < 𝑥𝑤 <R (1st𝑥)))
1716exp31 422 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ → (𝑥 ∈ ℝ → ((1st𝑦) = 𝑤 → (𝑦 < 𝑥𝑤 <R (1st𝑥)))))
1812, 17syl 17 . . . . . . . . . . . . . . . 16 ((𝐴 ⊆ ℝ ∧ 𝑦𝐴) → (𝑥 ∈ ℝ → ((1st𝑦) = 𝑤 → (𝑦 < 𝑥𝑤 <R (1st𝑥)))))
1918imp4b 424 . . . . . . . . . . . . . . 15 (((𝐴 ⊆ ℝ ∧ 𝑦𝐴) ∧ 𝑥 ∈ ℝ) → (((1st𝑦) = 𝑤𝑦 < 𝑥) → 𝑤 <R (1st𝑥)))
2019ancomsd 468 . . . . . . . . . . . . . 14 (((𝐴 ⊆ ℝ ∧ 𝑦𝐴) ∧ 𝑥 ∈ ℝ) → ((𝑦 < 𝑥 ∧ (1st𝑦) = 𝑤) → 𝑤 <R (1st𝑥)))
2120an32s 650 . . . . . . . . . . . . 13 (((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) ∧ 𝑦𝐴) → ((𝑦 < 𝑥 ∧ (1st𝑦) = 𝑤) → 𝑤 <R (1st𝑥)))
2221rexlimdva 3287 . . . . . . . . . . . 12 ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) → (∃𝑦𝐴 (𝑦 < 𝑥 ∧ (1st𝑦) = 𝑤) → 𝑤 <R (1st𝑥)))
2311, 22syl5 34 . . . . . . . . . . 11 ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) → ((∀𝑦𝐴 𝑦 < 𝑥 ∧ ∃𝑦𝐴 (1st𝑦) = 𝑤) → 𝑤 <R (1st𝑥)))
2423expd 418 . . . . . . . . . 10 ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) → (∀𝑦𝐴 𝑦 < 𝑥 → (∃𝑦𝐴 (1st𝑦) = 𝑤𝑤 <R (1st𝑥))))
2510, 24syl7bi 257 . . . . . . . . 9 ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) → (∀𝑦𝐴 𝑦 < 𝑥 → (𝑤 ∈ (1st𝐴) → 𝑤 <R (1st𝑥))))
2625impr 457 . . . . . . . 8 ((𝐴 ⊆ ℝ ∧ (𝑥 ∈ ℝ ∧ ∀𝑦𝐴 𝑦 < 𝑥)) → (𝑤 ∈ (1st𝐴) → 𝑤 <R (1st𝑥)))
2726adantlr 713 . . . . . . 7 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦𝐴 𝑦 < 𝑥)) → (𝑤 ∈ (1st𝐴) → 𝑤 <R (1st𝑥)))
2827ralrimiv 3184 . . . . . 6 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦𝐴 𝑦 < 𝑥)) → ∀𝑤 ∈ (1st𝐴)𝑤 <R (1st𝑥))
2928expr 459 . . . . 5 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ℝ) → (∀𝑦𝐴 𝑦 < 𝑥 → ∀𝑤 ∈ (1st𝐴)𝑤 <R (1st𝑥)))
30 brralrspcev 5129 . . . . 5 (((1st𝑥) ∈ R ∧ ∀𝑤 ∈ (1st𝐴)𝑤 <R (1st𝑥)) → ∃𝑣R𝑤 ∈ (1st𝐴)𝑤 <R 𝑣)
313, 29, 30syl6an 682 . . . 4 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ℝ) → (∀𝑦𝐴 𝑦 < 𝑥 → ∃𝑣R𝑤 ∈ (1st𝐴)𝑤 <R 𝑣))
3231rexlimdva 3287 . . 3 ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → (∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦 < 𝑥 → ∃𝑣R𝑤 ∈ (1st𝐴)𝑤 <R 𝑣))
33 n0 4313 . . . . . 6 (𝐴 ≠ ∅ ↔ ∃𝑦 𝑦𝐴)
34 fnfvima 6998 . . . . . . . . 9 ((1st Fn V ∧ 𝐴 ⊆ V ∧ 𝑦𝐴) → (1st𝑦) ∈ (1st𝐴))
357, 8, 34mp3an12 1447 . . . . . . . 8 (𝑦𝐴 → (1st𝑦) ∈ (1st𝐴))
3635ne0d 4304 . . . . . . 7 (𝑦𝐴 → (1st𝐴) ≠ ∅)
3736exlimiv 1930 . . . . . 6 (∃𝑦 𝑦𝐴 → (1st𝐴) ≠ ∅)
3833, 37sylbi 219 . . . . 5 (𝐴 ≠ ∅ → (1st𝐴) ≠ ∅)
39 supsr 10537 . . . . . 6 (((1st𝐴) ≠ ∅ ∧ ∃𝑣R𝑤 ∈ (1st𝐴)𝑤 <R 𝑣) → ∃𝑣R (∀𝑤 ∈ (1st𝐴) ¬ 𝑣 <R 𝑤 ∧ ∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢)))
4039ex 415 . . . . 5 ((1st𝐴) ≠ ∅ → (∃𝑣R𝑤 ∈ (1st𝐴)𝑤 <R 𝑣 → ∃𝑣R (∀𝑤 ∈ (1st𝐴) ¬ 𝑣 <R 𝑤 ∧ ∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢))))
4138, 40syl 17 . . . 4 (𝐴 ≠ ∅ → (∃𝑣R𝑤 ∈ (1st𝐴)𝑤 <R 𝑣 → ∃𝑣R (∀𝑤 ∈ (1st𝐴) ¬ 𝑣 <R 𝑤 ∧ ∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢))))
4241adantl 484 . . 3 ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → (∃𝑣R𝑤 ∈ (1st𝐴)𝑤 <R 𝑣 → ∃𝑣R (∀𝑤 ∈ (1st𝐴) ¬ 𝑣 <R 𝑤 ∧ ∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢))))
43 breq2 5073 . . . . . . . . . . . 12 (𝑤 = (1st𝑦) → (𝑣 <R 𝑤𝑣 <R (1st𝑦)))
4443notbid 320 . . . . . . . . . . 11 (𝑤 = (1st𝑦) → (¬ 𝑣 <R 𝑤 ↔ ¬ 𝑣 <R (1st𝑦)))
4544rspccv 3623 . . . . . . . . . 10 (∀𝑤 ∈ (1st𝐴) ¬ 𝑣 <R 𝑤 → ((1st𝑦) ∈ (1st𝐴) → ¬ 𝑣 <R (1st𝑦)))
4635, 45syl5com 31 . . . . . . . . 9 (𝑦𝐴 → (∀𝑤 ∈ (1st𝐴) ¬ 𝑣 <R 𝑤 → ¬ 𝑣 <R (1st𝑦)))
4746adantl 484 . . . . . . . 8 ((𝐴 ⊆ ℝ ∧ 𝑦𝐴) → (∀𝑤 ∈ (1st𝐴) ¬ 𝑣 <R 𝑤 → ¬ 𝑣 <R (1st𝑦)))
48 elreal2 10557 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ ↔ ((1st𝑦) ∈ R𝑦 = ⟨(1st𝑦), 0R⟩))
4948simprbi 499 . . . . . . . . . . . 12 (𝑦 ∈ ℝ → 𝑦 = ⟨(1st𝑦), 0R⟩)
5049breq2d 5081 . . . . . . . . . . 11 (𝑦 ∈ ℝ → (⟨𝑣, 0R⟩ < 𝑦 ↔ ⟨𝑣, 0R⟩ < ⟨(1st𝑦), 0R⟩))
51 ltresr 10565 . . . . . . . . . . 11 (⟨𝑣, 0R⟩ < ⟨(1st𝑦), 0R⟩ ↔ 𝑣 <R (1st𝑦))
5250, 51syl6bb 289 . . . . . . . . . 10 (𝑦 ∈ ℝ → (⟨𝑣, 0R⟩ < 𝑦𝑣 <R (1st𝑦)))
5312, 52syl 17 . . . . . . . . 9 ((𝐴 ⊆ ℝ ∧ 𝑦𝐴) → (⟨𝑣, 0R⟩ < 𝑦𝑣 <R (1st𝑦)))
5453notbid 320 . . . . . . . 8 ((𝐴 ⊆ ℝ ∧ 𝑦𝐴) → (¬ ⟨𝑣, 0R⟩ < 𝑦 ↔ ¬ 𝑣 <R (1st𝑦)))
5547, 54sylibrd 261 . . . . . . 7 ((𝐴 ⊆ ℝ ∧ 𝑦𝐴) → (∀𝑤 ∈ (1st𝐴) ¬ 𝑣 <R 𝑤 → ¬ ⟨𝑣, 0R⟩ < 𝑦))
5655ralrimdva 3192 . . . . . 6 (𝐴 ⊆ ℝ → (∀𝑤 ∈ (1st𝐴) ¬ 𝑣 <R 𝑤 → ∀𝑦𝐴 ¬ ⟨𝑣, 0R⟩ < 𝑦))
5756ad2antrr 724 . . . . 5 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣R) → (∀𝑤 ∈ (1st𝐴) ¬ 𝑣 <R 𝑤 → ∀𝑦𝐴 ¬ ⟨𝑣, 0R⟩ < 𝑦))
5849breq1d 5079 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ → (𝑦 <𝑣, 0R⟩ ↔ ⟨(1st𝑦), 0R⟩ <𝑣, 0R⟩))
59 ltresr 10565 . . . . . . . . . . . . . 14 (⟨(1st𝑦), 0R⟩ <𝑣, 0R⟩ ↔ (1st𝑦) <R 𝑣)
6058, 59syl6bb 289 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ → (𝑦 <𝑣, 0R⟩ ↔ (1st𝑦) <R 𝑣))
6148simplbi 500 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℝ → (1st𝑦) ∈ R)
62 breq1 5072 . . . . . . . . . . . . . . . . 17 (𝑤 = (1st𝑦) → (𝑤 <R 𝑣 ↔ (1st𝑦) <R 𝑣))
63 breq1 5072 . . . . . . . . . . . . . . . . . 18 (𝑤 = (1st𝑦) → (𝑤 <R 𝑢 ↔ (1st𝑦) <R 𝑢))
6463rexbidv 3300 . . . . . . . . . . . . . . . . 17 (𝑤 = (1st𝑦) → (∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢 ↔ ∃𝑢 ∈ (1st𝐴)(1st𝑦) <R 𝑢))
6562, 64imbi12d 347 . . . . . . . . . . . . . . . 16 (𝑤 = (1st𝑦) → ((𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢) ↔ ((1st𝑦) <R 𝑣 → ∃𝑢 ∈ (1st𝐴)(1st𝑦) <R 𝑢)))
6665rspccv 3623 . . . . . . . . . . . . . . 15 (∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢) → ((1st𝑦) ∈ R → ((1st𝑦) <R 𝑣 → ∃𝑢 ∈ (1st𝐴)(1st𝑦) <R 𝑢)))
6761, 66syl5 34 . . . . . . . . . . . . . 14 (∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢) → (𝑦 ∈ ℝ → ((1st𝑦) <R 𝑣 → ∃𝑢 ∈ (1st𝐴)(1st𝑦) <R 𝑢)))
6867com3l 89 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ → ((1st𝑦) <R 𝑣 → (∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢) → ∃𝑢 ∈ (1st𝐴)(1st𝑦) <R 𝑢)))
6960, 68sylbid 242 . . . . . . . . . . . 12 (𝑦 ∈ ℝ → (𝑦 <𝑣, 0R⟩ → (∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢) → ∃𝑢 ∈ (1st𝐴)(1st𝑦) <R 𝑢)))
7069adantr 483 . . . . . . . . . . 11 ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (𝑦 <𝑣, 0R⟩ → (∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢) → ∃𝑢 ∈ (1st𝐴)(1st𝑦) <R 𝑢)))
71 fvelimab 6740 . . . . . . . . . . . . . . . 16 ((1st Fn V ∧ 𝐴 ⊆ V) → (𝑢 ∈ (1st𝐴) ↔ ∃𝑧𝐴 (1st𝑧) = 𝑢))
727, 8, 71mp2an 690 . . . . . . . . . . . . . . 15 (𝑢 ∈ (1st𝐴) ↔ ∃𝑧𝐴 (1st𝑧) = 𝑢)
73 ssel2 3965 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ⊆ ℝ ∧ 𝑧𝐴) → 𝑧 ∈ ℝ)
74 ltresr2 10566 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 < 𝑧 ↔ (1st𝑦) <R (1st𝑧)))
7573, 74sylan2 594 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 ∈ ℝ ∧ (𝐴 ⊆ ℝ ∧ 𝑧𝐴)) → (𝑦 < 𝑧 ↔ (1st𝑦) <R (1st𝑧)))
76 breq2 5073 . . . . . . . . . . . . . . . . . . . . 21 ((1st𝑧) = 𝑢 → ((1st𝑦) <R (1st𝑧) ↔ (1st𝑦) <R 𝑢))
7775, 76sylan9bb 512 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 ∈ ℝ ∧ (𝐴 ⊆ ℝ ∧ 𝑧𝐴)) ∧ (1st𝑧) = 𝑢) → (𝑦 < 𝑧 ↔ (1st𝑦) <R 𝑢))
7877exbiri 809 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ℝ ∧ (𝐴 ⊆ ℝ ∧ 𝑧𝐴)) → ((1st𝑧) = 𝑢 → ((1st𝑦) <R 𝑢𝑦 < 𝑧)))
7978expr 459 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (𝑧𝐴 → ((1st𝑧) = 𝑢 → ((1st𝑦) <R 𝑢𝑦 < 𝑧))))
8079com4r 94 . . . . . . . . . . . . . . . . 17 ((1st𝑦) <R 𝑢 → ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (𝑧𝐴 → ((1st𝑧) = 𝑢𝑦 < 𝑧))))
8180imp 409 . . . . . . . . . . . . . . . 16 (((1st𝑦) <R 𝑢 ∧ (𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ)) → (𝑧𝐴 → ((1st𝑧) = 𝑢𝑦 < 𝑧)))
8281reximdvai 3275 . . . . . . . . . . . . . . 15 (((1st𝑦) <R 𝑢 ∧ (𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ)) → (∃𝑧𝐴 (1st𝑧) = 𝑢 → ∃𝑧𝐴 𝑦 < 𝑧))
8372, 82syl5bi 244 . . . . . . . . . . . . . 14 (((1st𝑦) <R 𝑢 ∧ (𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ)) → (𝑢 ∈ (1st𝐴) → ∃𝑧𝐴 𝑦 < 𝑧))
8483expcom 416 . . . . . . . . . . . . 13 ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → ((1st𝑦) <R 𝑢 → (𝑢 ∈ (1st𝐴) → ∃𝑧𝐴 𝑦 < 𝑧)))
8584com23 86 . . . . . . . . . . . 12 ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (𝑢 ∈ (1st𝐴) → ((1st𝑦) <R 𝑢 → ∃𝑧𝐴 𝑦 < 𝑧)))
8685rexlimdv 3286 . . . . . . . . . . 11 ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (∃𝑢 ∈ (1st𝐴)(1st𝑦) <R 𝑢 → ∃𝑧𝐴 𝑦 < 𝑧))
8770, 86syl6d 75 . . . . . . . . . 10 ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (𝑦 <𝑣, 0R⟩ → (∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢) → ∃𝑧𝐴 𝑦 < 𝑧)))
8887com23 86 . . . . . . . . 9 ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢) → (𝑦 <𝑣, 0R⟩ → ∃𝑧𝐴 𝑦 < 𝑧)))
8988ex 415 . . . . . . . 8 (𝑦 ∈ ℝ → (𝐴 ⊆ ℝ → (∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢) → (𝑦 <𝑣, 0R⟩ → ∃𝑧𝐴 𝑦 < 𝑧))))
9089com3l 89 . . . . . . 7 (𝐴 ⊆ ℝ → (∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢) → (𝑦 ∈ ℝ → (𝑦 <𝑣, 0R⟩ → ∃𝑧𝐴 𝑦 < 𝑧))))
9190ad2antrr 724 . . . . . 6 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣R) → (∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢) → (𝑦 ∈ ℝ → (𝑦 <𝑣, 0R⟩ → ∃𝑧𝐴 𝑦 < 𝑧))))
9291ralrimdv 3191 . . . . 5 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣R) → (∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢) → ∀𝑦 ∈ ℝ (𝑦 <𝑣, 0R⟩ → ∃𝑧𝐴 𝑦 < 𝑧)))
93 opelreal 10555 . . . . . . . 8 (⟨𝑣, 0R⟩ ∈ ℝ ↔ 𝑣R)
9493biimpri 230 . . . . . . 7 (𝑣R → ⟨𝑣, 0R⟩ ∈ ℝ)
9594adantl 484 . . . . . 6 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣R) → ⟨𝑣, 0R⟩ ∈ ℝ)
96 breq1 5072 . . . . . . . . . . 11 (𝑥 = ⟨𝑣, 0R⟩ → (𝑥 < 𝑦 ↔ ⟨𝑣, 0R⟩ < 𝑦))
9796notbid 320 . . . . . . . . . 10 (𝑥 = ⟨𝑣, 0R⟩ → (¬ 𝑥 < 𝑦 ↔ ¬ ⟨𝑣, 0R⟩ < 𝑦))
9897ralbidv 3200 . . . . . . . . 9 (𝑥 = ⟨𝑣, 0R⟩ → (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ↔ ∀𝑦𝐴 ¬ ⟨𝑣, 0R⟩ < 𝑦))
99 breq2 5073 . . . . . . . . . . 11 (𝑥 = ⟨𝑣, 0R⟩ → (𝑦 < 𝑥𝑦 <𝑣, 0R⟩))
10099imbi1d 344 . . . . . . . . . 10 (𝑥 = ⟨𝑣, 0R⟩ → ((𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧) ↔ (𝑦 <𝑣, 0R⟩ → ∃𝑧𝐴 𝑦 < 𝑧)))
101100ralbidv 3200 . . . . . . . . 9 (𝑥 = ⟨𝑣, 0R⟩ → (∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧) ↔ ∀𝑦 ∈ ℝ (𝑦 <𝑣, 0R⟩ → ∃𝑧𝐴 𝑦 < 𝑧)))
10298, 101anbi12d 632 . . . . . . . 8 (𝑥 = ⟨𝑣, 0R⟩ → ((∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)) ↔ (∀𝑦𝐴 ¬ ⟨𝑣, 0R⟩ < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <𝑣, 0R⟩ → ∃𝑧𝐴 𝑦 < 𝑧))))
103102rspcev 3626 . . . . . . 7 ((⟨𝑣, 0R⟩ ∈ ℝ ∧ (∀𝑦𝐴 ¬ ⟨𝑣, 0R⟩ < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <𝑣, 0R⟩ → ∃𝑧𝐴 𝑦 < 𝑧))) → ∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
104103ex 415 . . . . . 6 (⟨𝑣, 0R⟩ ∈ ℝ → ((∀𝑦𝐴 ¬ ⟨𝑣, 0R⟩ < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <𝑣, 0R⟩ → ∃𝑧𝐴 𝑦 < 𝑧)) → ∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧))))
10595, 104syl 17 . . . . 5 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣R) → ((∀𝑦𝐴 ¬ ⟨𝑣, 0R⟩ < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <𝑣, 0R⟩ → ∃𝑧𝐴 𝑦 < 𝑧)) → ∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧))))
10657, 92, 105syl2and 609 . . . 4 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣R) → ((∀𝑤 ∈ (1st𝐴) ¬ 𝑣 <R 𝑤 ∧ ∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢)) → ∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧))))
107106rexlimdva 3287 . . 3 ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → (∃𝑣R (∀𝑤 ∈ (1st𝐴) ¬ 𝑣 <R 𝑤 ∧ ∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢)) → ∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧))))
10832, 42, 1073syld 60 . 2 ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → (∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦 < 𝑥 → ∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧))))
1091083impia 1113 1 ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦 < 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398  w3a 1083   = wceq 1536  wex 1779  wcel 2113  wne 3019  wral 3141  wrex 3142  Vcvv 3497  wss 3939  c0 4294  cop 4576   class class class wbr 5069  cima 5561   Fn wfn 6353  wf 6354  ontowfo 6356  cfv 6358  1st c1st 7690  Rcnr 10290  0Rc0r 10291   <R cltr 10296  cr 10539   < cltrr 10544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464  ax-inf2 9107
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-ral 3146  df-rex 3147  df-reu 3148  df-rmo 3149  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-tp 4575  df-op 4577  df-uni 4842  df-int 4880  df-iun 4924  df-br 5070  df-opab 5132  df-mpt 5150  df-tr 5176  df-id 5463  df-eprel 5468  df-po 5477  df-so 5478  df-fr 5517  df-we 5519  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-pred 6151  df-ord 6197  df-on 6198  df-lim 6199  df-suc 6200  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-ov 7162  df-oprab 7163  df-mpo 7164  df-om 7584  df-1st 7692  df-2nd 7693  df-wrecs 7950  df-recs 8011  df-rdg 8049  df-1o 8105  df-oadd 8109  df-omul 8110  df-er 8292  df-ec 8294  df-qs 8298  df-ni 10297  df-pli 10298  df-mi 10299  df-lti 10300  df-plpq 10333  df-mpq 10334  df-ltpq 10335  df-enq 10336  df-nq 10337  df-erq 10338  df-plq 10339  df-mq 10340  df-1nq 10341  df-rq 10342  df-ltnq 10343  df-np 10406  df-1p 10407  df-plp 10408  df-mp 10409  df-ltp 10410  df-enr 10480  df-nr 10481  df-plr 10482  df-mr 10483  df-ltr 10484  df-0r 10485  df-1r 10486  df-m1r 10487  df-r 10550  df-lt 10553
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator