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

Theorem axpre-sup 10028
 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 10151. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-sup 10052. (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 9991 . . . . . . 7 (𝑥 ∈ ℝ ↔ ((1st𝑥) ∈ R𝑥 = ⟨(1st𝑥), 0R⟩))
21simplbi 475 . . . . . 6 (𝑥 ∈ ℝ → (1st𝑥) ∈ R)
32adantl 481 . . . . 5 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ℝ) → (1st𝑥) ∈ R)
4 fo1st 7230 . . . . . . . . . . . 12 1st :V–onto→V
5 fof 6153 . . . . . . . . . . . 12 (1st :V–onto→V → 1st :V⟶V)
6 ffn 6083 . . . . . . . . . . . 12 (1st :V⟶V → 1st Fn V)
74, 5, 6mp2b 10 . . . . . . . . . . 11 1st Fn V
8 ssv 3658 . . . . . . . . . . 11 𝐴 ⊆ V
9 fvelimab 6292 . . . . . . . . . . 11 ((1st Fn V ∧ 𝐴 ⊆ V) → (𝑤 ∈ (1st𝐴) ↔ ∃𝑦𝐴 (1st𝑦) = 𝑤))
107, 8, 9mp2an 708 . . . . . . . . . 10 (𝑤 ∈ (1st𝐴) ↔ ∃𝑦𝐴 (1st𝑦) = 𝑤)
11 r19.29 3101 . . . . . . . . . . . 12 ((∀𝑦𝐴 𝑦 < 𝑥 ∧ ∃𝑦𝐴 (1st𝑦) = 𝑤) → ∃𝑦𝐴 (𝑦 < 𝑥 ∧ (1st𝑦) = 𝑤))
12 ssel2 3631 . . . . . . . . . . . . . . . . 17 ((𝐴 ⊆ ℝ ∧ 𝑦𝐴) → 𝑦 ∈ ℝ)
13 ltresr2 10000 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑦 < 𝑥 ↔ (1st𝑦) <R (1st𝑥)))
14 breq1 4688 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑦) = 𝑤 → ((1st𝑦) <R (1st𝑥) ↔ 𝑤 <R (1st𝑥)))
1513, 14sylan9bb 736 . . . . . . . . . . . . . . . . . . 19 (((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) ∧ (1st𝑦) = 𝑤) → (𝑦 < 𝑥𝑤 <R (1st𝑥)))
1615biimpd 219 . . . . . . . . . . . . . . . . . 18 (((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) ∧ (1st𝑦) = 𝑤) → (𝑦 < 𝑥𝑤 <R (1st𝑥)))
1716exp31 629 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ → (𝑥 ∈ ℝ → ((1st𝑦) = 𝑤 → (𝑦 < 𝑥𝑤 <R (1st𝑥)))))
1812, 17syl 17 . . . . . . . . . . . . . . . 16 ((𝐴 ⊆ ℝ ∧ 𝑦𝐴) → (𝑥 ∈ ℝ → ((1st𝑦) = 𝑤 → (𝑦 < 𝑥𝑤 <R (1st𝑥)))))
1918imp4b 612 . . . . . . . . . . . . . . 15 (((𝐴 ⊆ ℝ ∧ 𝑦𝐴) ∧ 𝑥 ∈ ℝ) → (((1st𝑦) = 𝑤𝑦 < 𝑥) → 𝑤 <R (1st𝑥)))
2019ancomsd 469 . . . . . . . . . . . . . 14 (((𝐴 ⊆ ℝ ∧ 𝑦𝐴) ∧ 𝑥 ∈ ℝ) → ((𝑦 < 𝑥 ∧ (1st𝑦) = 𝑤) → 𝑤 <R (1st𝑥)))
2120an32s 863 . . . . . . . . . . . . 13 (((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) ∧ 𝑦𝐴) → ((𝑦 < 𝑥 ∧ (1st𝑦) = 𝑤) → 𝑤 <R (1st𝑥)))
2221rexlimdva 3060 . . . . . . . . . . . 12 ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) → (∃𝑦𝐴 (𝑦 < 𝑥 ∧ (1st𝑦) = 𝑤) → 𝑤 <R (1st𝑥)))
2311, 22syl5 34 . . . . . . . . . . 11 ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) → ((∀𝑦𝐴 𝑦 < 𝑥 ∧ ∃𝑦𝐴 (1st𝑦) = 𝑤) → 𝑤 <R (1st𝑥)))
2423expd 451 . . . . . . . . . 10 ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) → (∀𝑦𝐴 𝑦 < 𝑥 → (∃𝑦𝐴 (1st𝑦) = 𝑤𝑤 <R (1st𝑥))))
2510, 24syl7bi 245 . . . . . . . . 9 ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) → (∀𝑦𝐴 𝑦 < 𝑥 → (𝑤 ∈ (1st𝐴) → 𝑤 <R (1st𝑥))))
2625impr 648 . . . . . . . 8 ((𝐴 ⊆ ℝ ∧ (𝑥 ∈ ℝ ∧ ∀𝑦𝐴 𝑦 < 𝑥)) → (𝑤 ∈ (1st𝐴) → 𝑤 <R (1st𝑥)))
2726adantlr 751 . . . . . . 7 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦𝐴 𝑦 < 𝑥)) → (𝑤 ∈ (1st𝐴) → 𝑤 <R (1st𝑥)))
2827ralrimiv 2994 . . . . . 6 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ (𝑥 ∈ ℝ ∧ ∀𝑦𝐴 𝑦 < 𝑥)) → ∀𝑤 ∈ (1st𝐴)𝑤 <R (1st𝑥))
2928expr 642 . . . . 5 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ℝ) → (∀𝑦𝐴 𝑦 < 𝑥 → ∀𝑤 ∈ (1st𝐴)𝑤 <R (1st𝑥)))
30 breq2 4689 . . . . . . 7 (𝑣 = (1st𝑥) → (𝑤 <R 𝑣𝑤 <R (1st𝑥)))
3130ralbidv 3015 . . . . . 6 (𝑣 = (1st𝑥) → (∀𝑤 ∈ (1st𝐴)𝑤 <R 𝑣 ↔ ∀𝑤 ∈ (1st𝐴)𝑤 <R (1st𝑥)))
3231rspcev 3340 . . . . 5 (((1st𝑥) ∈ R ∧ ∀𝑤 ∈ (1st𝐴)𝑤 <R (1st𝑥)) → ∃𝑣R𝑤 ∈ (1st𝐴)𝑤 <R 𝑣)
333, 29, 32syl6an 567 . . . 4 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ℝ) → (∀𝑦𝐴 𝑦 < 𝑥 → ∃𝑣R𝑤 ∈ (1st𝐴)𝑤 <R 𝑣))
3433rexlimdva 3060 . . 3 ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → (∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦 < 𝑥 → ∃𝑣R𝑤 ∈ (1st𝐴)𝑤 <R 𝑣))
35 n0 3964 . . . . . 6 (𝐴 ≠ ∅ ↔ ∃𝑦 𝑦𝐴)
36 fnfvima 6536 . . . . . . . . 9 ((1st Fn V ∧ 𝐴 ⊆ V ∧ 𝑦𝐴) → (1st𝑦) ∈ (1st𝐴))
377, 8, 36mp3an12 1454 . . . . . . . 8 (𝑦𝐴 → (1st𝑦) ∈ (1st𝐴))
38 ne0i 3954 . . . . . . . 8 ((1st𝑦) ∈ (1st𝐴) → (1st𝐴) ≠ ∅)
3937, 38syl 17 . . . . . . 7 (𝑦𝐴 → (1st𝐴) ≠ ∅)
4039exlimiv 1898 . . . . . 6 (∃𝑦 𝑦𝐴 → (1st𝐴) ≠ ∅)
4135, 40sylbi 207 . . . . 5 (𝐴 ≠ ∅ → (1st𝐴) ≠ ∅)
42 supsr 9971 . . . . . 6 (((1st𝐴) ≠ ∅ ∧ ∃𝑣R𝑤 ∈ (1st𝐴)𝑤 <R 𝑣) → ∃𝑣R (∀𝑤 ∈ (1st𝐴) ¬ 𝑣 <R 𝑤 ∧ ∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢)))
4342ex 449 . . . . 5 ((1st𝐴) ≠ ∅ → (∃𝑣R𝑤 ∈ (1st𝐴)𝑤 <R 𝑣 → ∃𝑣R (∀𝑤 ∈ (1st𝐴) ¬ 𝑣 <R 𝑤 ∧ ∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢))))
4441, 43syl 17 . . . 4 (𝐴 ≠ ∅ → (∃𝑣R𝑤 ∈ (1st𝐴)𝑤 <R 𝑣 → ∃𝑣R (∀𝑤 ∈ (1st𝐴) ¬ 𝑣 <R 𝑤 ∧ ∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢))))
4544adantl 481 . . 3 ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → (∃𝑣R𝑤 ∈ (1st𝐴)𝑤 <R 𝑣 → ∃𝑣R (∀𝑤 ∈ (1st𝐴) ¬ 𝑣 <R 𝑤 ∧ ∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢))))
46 breq2 4689 . . . . . . . . . . . 12 (𝑤 = (1st𝑦) → (𝑣 <R 𝑤𝑣 <R (1st𝑦)))
4746notbid 307 . . . . . . . . . . 11 (𝑤 = (1st𝑦) → (¬ 𝑣 <R 𝑤 ↔ ¬ 𝑣 <R (1st𝑦)))
4847rspccv 3337 . . . . . . . . . 10 (∀𝑤 ∈ (1st𝐴) ¬ 𝑣 <R 𝑤 → ((1st𝑦) ∈ (1st𝐴) → ¬ 𝑣 <R (1st𝑦)))
4937, 48syl5com 31 . . . . . . . . 9 (𝑦𝐴 → (∀𝑤 ∈ (1st𝐴) ¬ 𝑣 <R 𝑤 → ¬ 𝑣 <R (1st𝑦)))
5049adantl 481 . . . . . . . 8 ((𝐴 ⊆ ℝ ∧ 𝑦𝐴) → (∀𝑤 ∈ (1st𝐴) ¬ 𝑣 <R 𝑤 → ¬ 𝑣 <R (1st𝑦)))
51 elreal2 9991 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ ↔ ((1st𝑦) ∈ R𝑦 = ⟨(1st𝑦), 0R⟩))
5251simprbi 479 . . . . . . . . . . . 12 (𝑦 ∈ ℝ → 𝑦 = ⟨(1st𝑦), 0R⟩)
5352breq2d 4697 . . . . . . . . . . 11 (𝑦 ∈ ℝ → (⟨𝑣, 0R⟩ < 𝑦 ↔ ⟨𝑣, 0R⟩ < ⟨(1st𝑦), 0R⟩))
54 ltresr 9999 . . . . . . . . . . 11 (⟨𝑣, 0R⟩ < ⟨(1st𝑦), 0R⟩ ↔ 𝑣 <R (1st𝑦))
5553, 54syl6bb 276 . . . . . . . . . 10 (𝑦 ∈ ℝ → (⟨𝑣, 0R⟩ < 𝑦𝑣 <R (1st𝑦)))
5612, 55syl 17 . . . . . . . . 9 ((𝐴 ⊆ ℝ ∧ 𝑦𝐴) → (⟨𝑣, 0R⟩ < 𝑦𝑣 <R (1st𝑦)))
5756notbid 307 . . . . . . . 8 ((𝐴 ⊆ ℝ ∧ 𝑦𝐴) → (¬ ⟨𝑣, 0R⟩ < 𝑦 ↔ ¬ 𝑣 <R (1st𝑦)))
5850, 57sylibrd 249 . . . . . . 7 ((𝐴 ⊆ ℝ ∧ 𝑦𝐴) → (∀𝑤 ∈ (1st𝐴) ¬ 𝑣 <R 𝑤 → ¬ ⟨𝑣, 0R⟩ < 𝑦))
5958ralrimdva 2998 . . . . . 6 (𝐴 ⊆ ℝ → (∀𝑤 ∈ (1st𝐴) ¬ 𝑣 <R 𝑤 → ∀𝑦𝐴 ¬ ⟨𝑣, 0R⟩ < 𝑦))
6059ad2antrr 762 . . . . 5 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣R) → (∀𝑤 ∈ (1st𝐴) ¬ 𝑣 <R 𝑤 → ∀𝑦𝐴 ¬ ⟨𝑣, 0R⟩ < 𝑦))
6152breq1d 4695 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ → (𝑦 <𝑣, 0R⟩ ↔ ⟨(1st𝑦), 0R⟩ <𝑣, 0R⟩))
62 ltresr 9999 . . . . . . . . . . . . . 14 (⟨(1st𝑦), 0R⟩ <𝑣, 0R⟩ ↔ (1st𝑦) <R 𝑣)
6361, 62syl6bb 276 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ → (𝑦 <𝑣, 0R⟩ ↔ (1st𝑦) <R 𝑣))
6451simplbi 475 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℝ → (1st𝑦) ∈ R)
65 breq1 4688 . . . . . . . . . . . . . . . . 17 (𝑤 = (1st𝑦) → (𝑤 <R 𝑣 ↔ (1st𝑦) <R 𝑣))
66 breq1 4688 . . . . . . . . . . . . . . . . . 18 (𝑤 = (1st𝑦) → (𝑤 <R 𝑢 ↔ (1st𝑦) <R 𝑢))
6766rexbidv 3081 . . . . . . . . . . . . . . . . 17 (𝑤 = (1st𝑦) → (∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢 ↔ ∃𝑢 ∈ (1st𝐴)(1st𝑦) <R 𝑢))
6865, 67imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑤 = (1st𝑦) → ((𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢) ↔ ((1st𝑦) <R 𝑣 → ∃𝑢 ∈ (1st𝐴)(1st𝑦) <R 𝑢)))
6968rspccv 3337 . . . . . . . . . . . . . . 15 (∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢) → ((1st𝑦) ∈ R → ((1st𝑦) <R 𝑣 → ∃𝑢 ∈ (1st𝐴)(1st𝑦) <R 𝑢)))
7064, 69syl5 34 . . . . . . . . . . . . . 14 (∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢) → (𝑦 ∈ ℝ → ((1st𝑦) <R 𝑣 → ∃𝑢 ∈ (1st𝐴)(1st𝑦) <R 𝑢)))
7170com3l 89 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ → ((1st𝑦) <R 𝑣 → (∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢) → ∃𝑢 ∈ (1st𝐴)(1st𝑦) <R 𝑢)))
7263, 71sylbid 230 . . . . . . . . . . . 12 (𝑦 ∈ ℝ → (𝑦 <𝑣, 0R⟩ → (∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢) → ∃𝑢 ∈ (1st𝐴)(1st𝑦) <R 𝑢)))
7372adantr 480 . . . . . . . . . . 11 ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (𝑦 <𝑣, 0R⟩ → (∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢) → ∃𝑢 ∈ (1st𝐴)(1st𝑦) <R 𝑢)))
74 fvelimab 6292 . . . . . . . . . . . . . . . 16 ((1st Fn V ∧ 𝐴 ⊆ V) → (𝑢 ∈ (1st𝐴) ↔ ∃𝑧𝐴 (1st𝑧) = 𝑢))
757, 8, 74mp2an 708 . . . . . . . . . . . . . . 15 (𝑢 ∈ (1st𝐴) ↔ ∃𝑧𝐴 (1st𝑧) = 𝑢)
76 ssel2 3631 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ⊆ ℝ ∧ 𝑧𝐴) → 𝑧 ∈ ℝ)
77 ltresr2 10000 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 < 𝑧 ↔ (1st𝑦) <R (1st𝑧)))
7876, 77sylan2 490 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 ∈ ℝ ∧ (𝐴 ⊆ ℝ ∧ 𝑧𝐴)) → (𝑦 < 𝑧 ↔ (1st𝑦) <R (1st𝑧)))
79 breq2 4689 . . . . . . . . . . . . . . . . . . . . 21 ((1st𝑧) = 𝑢 → ((1st𝑦) <R (1st𝑧) ↔ (1st𝑦) <R 𝑢))
8078, 79sylan9bb 736 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 ∈ ℝ ∧ (𝐴 ⊆ ℝ ∧ 𝑧𝐴)) ∧ (1st𝑧) = 𝑢) → (𝑦 < 𝑧 ↔ (1st𝑦) <R 𝑢))
8180exbiri 651 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ℝ ∧ (𝐴 ⊆ ℝ ∧ 𝑧𝐴)) → ((1st𝑧) = 𝑢 → ((1st𝑦) <R 𝑢𝑦 < 𝑧)))
8281expr 642 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (𝑧𝐴 → ((1st𝑧) = 𝑢 → ((1st𝑦) <R 𝑢𝑦 < 𝑧))))
8382com4r 94 . . . . . . . . . . . . . . . . 17 ((1st𝑦) <R 𝑢 → ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (𝑧𝐴 → ((1st𝑧) = 𝑢𝑦 < 𝑧))))
8483imp 444 . . . . . . . . . . . . . . . 16 (((1st𝑦) <R 𝑢 ∧ (𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ)) → (𝑧𝐴 → ((1st𝑧) = 𝑢𝑦 < 𝑧)))
8584reximdvai 3044 . . . . . . . . . . . . . . 15 (((1st𝑦) <R 𝑢 ∧ (𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ)) → (∃𝑧𝐴 (1st𝑧) = 𝑢 → ∃𝑧𝐴 𝑦 < 𝑧))
8675, 85syl5bi 232 . . . . . . . . . . . . . 14 (((1st𝑦) <R 𝑢 ∧ (𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ)) → (𝑢 ∈ (1st𝐴) → ∃𝑧𝐴 𝑦 < 𝑧))
8786expcom 450 . . . . . . . . . . . . 13 ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → ((1st𝑦) <R 𝑢 → (𝑢 ∈ (1st𝐴) → ∃𝑧𝐴 𝑦 < 𝑧)))
8887com23 86 . . . . . . . . . . . 12 ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (𝑢 ∈ (1st𝐴) → ((1st𝑦) <R 𝑢 → ∃𝑧𝐴 𝑦 < 𝑧)))
8988rexlimdv 3059 . . . . . . . . . . 11 ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (∃𝑢 ∈ (1st𝐴)(1st𝑦) <R 𝑢 → ∃𝑧𝐴 𝑦 < 𝑧))
9073, 89syl6d 75 . . . . . . . . . 10 ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (𝑦 <𝑣, 0R⟩ → (∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢) → ∃𝑧𝐴 𝑦 < 𝑧)))
9190com23 86 . . . . . . . . 9 ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢) → (𝑦 <𝑣, 0R⟩ → ∃𝑧𝐴 𝑦 < 𝑧)))
9291ex 449 . . . . . . . 8 (𝑦 ∈ ℝ → (𝐴 ⊆ ℝ → (∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢) → (𝑦 <𝑣, 0R⟩ → ∃𝑧𝐴 𝑦 < 𝑧))))
9392com3l 89 . . . . . . 7 (𝐴 ⊆ ℝ → (∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢) → (𝑦 ∈ ℝ → (𝑦 <𝑣, 0R⟩ → ∃𝑧𝐴 𝑦 < 𝑧))))
9493ad2antrr 762 . . . . . 6 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣R) → (∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢) → (𝑦 ∈ ℝ → (𝑦 <𝑣, 0R⟩ → ∃𝑧𝐴 𝑦 < 𝑧))))
9594ralrimdv 2997 . . . . 5 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣R) → (∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢) → ∀𝑦 ∈ ℝ (𝑦 <𝑣, 0R⟩ → ∃𝑧𝐴 𝑦 < 𝑧)))
96 opelreal 9989 . . . . . . . 8 (⟨𝑣, 0R⟩ ∈ ℝ ↔ 𝑣R)
9796biimpri 218 . . . . . . 7 (𝑣R → ⟨𝑣, 0R⟩ ∈ ℝ)
9897adantl 481 . . . . . 6 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣R) → ⟨𝑣, 0R⟩ ∈ ℝ)
99 breq1 4688 . . . . . . . . . . 11 (𝑥 = ⟨𝑣, 0R⟩ → (𝑥 < 𝑦 ↔ ⟨𝑣, 0R⟩ < 𝑦))
10099notbid 307 . . . . . . . . . 10 (𝑥 = ⟨𝑣, 0R⟩ → (¬ 𝑥 < 𝑦 ↔ ¬ ⟨𝑣, 0R⟩ < 𝑦))
101100ralbidv 3015 . . . . . . . . 9 (𝑥 = ⟨𝑣, 0R⟩ → (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ↔ ∀𝑦𝐴 ¬ ⟨𝑣, 0R⟩ < 𝑦))
102 breq2 4689 . . . . . . . . . . 11 (𝑥 = ⟨𝑣, 0R⟩ → (𝑦 < 𝑥𝑦 <𝑣, 0R⟩))
103102imbi1d 330 . . . . . . . . . 10 (𝑥 = ⟨𝑣, 0R⟩ → ((𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧) ↔ (𝑦 <𝑣, 0R⟩ → ∃𝑧𝐴 𝑦 < 𝑧)))
104103ralbidv 3015 . . . . . . . . 9 (𝑥 = ⟨𝑣, 0R⟩ → (∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧) ↔ ∀𝑦 ∈ ℝ (𝑦 <𝑣, 0R⟩ → ∃𝑧𝐴 𝑦 < 𝑧)))
105101, 104anbi12d 747 . . . . . . . 8 (𝑥 = ⟨𝑣, 0R⟩ → ((∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)) ↔ (∀𝑦𝐴 ¬ ⟨𝑣, 0R⟩ < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <𝑣, 0R⟩ → ∃𝑧𝐴 𝑦 < 𝑧))))
106105rspcev 3340 . . . . . . 7 ((⟨𝑣, 0R⟩ ∈ ℝ ∧ (∀𝑦𝐴 ¬ ⟨𝑣, 0R⟩ < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <𝑣, 0R⟩ → ∃𝑧𝐴 𝑦 < 𝑧))) → ∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
107106ex 449 . . . . . 6 (⟨𝑣, 0R⟩ ∈ ℝ → ((∀𝑦𝐴 ¬ ⟨𝑣, 0R⟩ < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <𝑣, 0R⟩ → ∃𝑧𝐴 𝑦 < 𝑧)) → ∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧))))
10898, 107syl 17 . . . . 5 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣R) → ((∀𝑦𝐴 ¬ ⟨𝑣, 0R⟩ < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <𝑣, 0R⟩ → ∃𝑧𝐴 𝑦 < 𝑧)) → ∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧))))
10960, 95, 108syl2and 499 . . . 4 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣R) → ((∀𝑤 ∈ (1st𝐴) ¬ 𝑣 <R 𝑤 ∧ ∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢)) → ∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧))))
110109rexlimdva 3060 . . 3 ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → (∃𝑣R (∀𝑤 ∈ (1st𝐴) ¬ 𝑣 <R 𝑤 ∧ ∀𝑤R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st𝐴)𝑤 <R 𝑢)) → ∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧))))
11134, 45, 1103syld 60 . 2 ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → (∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦 < 𝑥 → ∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧))))
1121113impia 1280 1 ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦 < 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1054   = wceq 1523  ∃wex 1744   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  ∃wrex 2942  Vcvv 3231   ⊆ wss 3607  ∅c0 3948  ⟨cop 4216   class class class wbr 4685   “ cima 5146   Fn wfn 5921  ⟶wf 5922  –onto→wfo 5924  ‘cfv 5926  1st c1st 7208  Rcnr 9725  0Rc0r 9726
 Copyright terms: Public domain W3C validator