ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dedekindeulemlu GIF version

Theorem dedekindeulemlu 13766
Description: Lemma for dedekindeu 13768. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 31-Jan-2024.)
Hypotheses
Ref Expression
dedekindeu.lss (𝜑𝐿 ⊆ ℝ)
dedekindeu.uss (𝜑𝑈 ⊆ ℝ)
dedekindeu.lm (𝜑 → ∃𝑞 ∈ ℝ 𝑞𝐿)
dedekindeu.um (𝜑 → ∃𝑟 ∈ ℝ 𝑟𝑈)
dedekindeu.lr (𝜑 → ∀𝑞 ∈ ℝ (𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟))
dedekindeu.ur (𝜑 → ∀𝑟 ∈ ℝ (𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟))
dedekindeu.disj (𝜑 → (𝐿𝑈) = ∅)
dedekindeu.loc (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞𝐿𝑟𝑈)))
Assertion
Ref Expression
dedekindeulemlu (𝜑 → ∃𝑥 ∈ ℝ (∀𝑞𝐿 𝑞 < 𝑥 ∧ ∀𝑟𝑈 𝑥 < 𝑟))
Distinct variable groups:   𝐿,𝑞,𝑟,𝑥   𝑈,𝑞,𝑟   𝜑,𝑞,𝑟,𝑥
Allowed substitution hint:   𝑈(𝑥)

Proof of Theorem dedekindeulemlu
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dedekindeu.lss . . 3 (𝜑𝐿 ⊆ ℝ)
2 dedekindeu.uss . . 3 (𝜑𝑈 ⊆ ℝ)
3 dedekindeu.lm . . 3 (𝜑 → ∃𝑞 ∈ ℝ 𝑞𝐿)
4 dedekindeu.um . . 3 (𝜑 → ∃𝑟 ∈ ℝ 𝑟𝑈)
5 dedekindeu.lr . . 3 (𝜑 → ∀𝑞 ∈ ℝ (𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟))
6 dedekindeu.ur . . 3 (𝜑 → ∀𝑟 ∈ ℝ (𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟))
7 dedekindeu.disj . . 3 (𝜑 → (𝐿𝑈) = ∅)
8 dedekindeu.loc . . 3 (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞𝐿𝑟𝑈)))
91, 2, 3, 4, 5, 6, 7, 8dedekindeulemlub 13765 . 2 (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧)))
10 simpr 110 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) → 𝑞𝐿)
111ad3antrrr 492 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) → 𝐿 ⊆ ℝ)
1211, 10sseldd 3156 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) → 𝑞 ∈ ℝ)
13 rsp 2524 . . . . . . . . . . 11 (∀𝑞 ∈ ℝ (𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟) → (𝑞 ∈ ℝ → (𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟)))
145, 13syl 14 . . . . . . . . . 10 (𝜑 → (𝑞 ∈ ℝ → (𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟)))
1514ad3antrrr 492 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) → (𝑞 ∈ ℝ → (𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟)))
1612, 15mpd 13 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) → (𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟))
1710, 16mpbid 147 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) → ∃𝑟𝐿 𝑞 < 𝑟)
1812adantr 276 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → 𝑞 ∈ ℝ)
1911adantr 276 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → 𝐿 ⊆ ℝ)
20 simprl 529 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → 𝑟𝐿)
2119, 20sseldd 3156 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → 𝑟 ∈ ℝ)
22 simp-4r 542 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → 𝑥 ∈ ℝ)
23 simprr 531 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → 𝑞 < 𝑟)
24 breq2 4004 . . . . . . . . . . 11 (𝑦 = 𝑟 → (𝑥 < 𝑦𝑥 < 𝑟))
2524notbid 667 . . . . . . . . . 10 (𝑦 = 𝑟 → (¬ 𝑥 < 𝑦 ↔ ¬ 𝑥 < 𝑟))
26 simprl 529 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) → ∀𝑦𝐿 ¬ 𝑥 < 𝑦)
2726ad2antrr 488 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → ∀𝑦𝐿 ¬ 𝑥 < 𝑦)
2825, 27, 20rspcdva 2846 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → ¬ 𝑥 < 𝑟)
2921, 22, 28nltled 8068 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → 𝑟𝑥)
3018, 21, 22, 23, 29ltletrd 8370 . . . . . . 7 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → 𝑞 < 𝑥)
3117, 30rexlimddv 2599 . . . . . 6 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) → 𝑞 < 𝑥)
3231ralrimiva 2550 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) → ∀𝑞𝐿 𝑞 < 𝑥)
33 simpr 110 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) → 𝑟𝑈)
34 simplll 533 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) → 𝜑)
3534, 2syl 14 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) → 𝑈 ⊆ ℝ)
3635, 33sseldd 3156 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) → 𝑟 ∈ ℝ)
37 rsp 2524 . . . . . . . . . 10 (∀𝑟 ∈ ℝ (𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟) → (𝑟 ∈ ℝ → (𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟)))
386, 37syl 14 . . . . . . . . 9 (𝜑 → (𝑟 ∈ ℝ → (𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟)))
3934, 36, 38sylc 62 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) → (𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟))
4033, 39mpbid 147 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) → ∃𝑞𝑈 𝑞 < 𝑟)
41 simp-4r 542 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) → 𝑥 ∈ ℝ)
4235adantr 276 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) → 𝑈 ⊆ ℝ)
43 simprl 529 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) → 𝑞𝑈)
4442, 43sseldd 3156 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) → 𝑞 ∈ ℝ)
4536adantr 276 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) → 𝑟 ∈ ℝ)
4643adantr 276 . . . . . . . . . 10 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝑞𝑈)
4734ad2antrr 488 . . . . . . . . . . 11 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝜑)
48 simpr 110 . . . . . . . . . . . . . 14 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝑞 < 𝑥)
49 breq1 4003 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑞 → (𝑦 < 𝑥𝑞 < 𝑥))
50 breq1 4003 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑞 → (𝑦 < 𝑧𝑞 < 𝑧))
5150rexbidv 2478 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑞 → (∃𝑧𝐿 𝑦 < 𝑧 ↔ ∃𝑧𝐿 𝑞 < 𝑧))
5249, 51imbi12d 234 . . . . . . . . . . . . . . 15 (𝑦 = 𝑞 → ((𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧) ↔ (𝑞 < 𝑥 → ∃𝑧𝐿 𝑞 < 𝑧)))
53 simprr 531 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) → ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))
5453ad3antrrr 492 . . . . . . . . . . . . . . 15 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))
5544adantr 276 . . . . . . . . . . . . . . 15 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝑞 ∈ ℝ)
5652, 54, 55rspcdva 2846 . . . . . . . . . . . . . 14 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → (𝑞 < 𝑥 → ∃𝑧𝐿 𝑞 < 𝑧))
5748, 56mpd 13 . . . . . . . . . . . . 13 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → ∃𝑧𝐿 𝑞 < 𝑧)
58 breq2 4004 . . . . . . . . . . . . . 14 (𝑧 = 𝑟 → (𝑞 < 𝑧𝑞 < 𝑟))
5958cbvrexv 2704 . . . . . . . . . . . . 13 (∃𝑧𝐿 𝑞 < 𝑧 ↔ ∃𝑟𝐿 𝑞 < 𝑟)
6057, 59sylib 122 . . . . . . . . . . . 12 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → ∃𝑟𝐿 𝑞 < 𝑟)
6147, 55, 14sylc 62 . . . . . . . . . . . 12 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → (𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟))
6260, 61mpbird 167 . . . . . . . . . . 11 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝑞𝐿)
63 disj 3471 . . . . . . . . . . . . 13 ((𝐿𝑈) = ∅ ↔ ∀𝑞𝐿 ¬ 𝑞𝑈)
647, 63sylib 122 . . . . . . . . . . . 12 (𝜑 → ∀𝑞𝐿 ¬ 𝑞𝑈)
6564r19.21bi 2565 . . . . . . . . . . 11 ((𝜑𝑞𝐿) → ¬ 𝑞𝑈)
6647, 62, 65syl2anc 411 . . . . . . . . . 10 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → ¬ 𝑞𝑈)
6746, 66pm2.65da 661 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) → ¬ 𝑞 < 𝑥)
6841, 44, 67nltled 8068 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) → 𝑥𝑞)
69 simprr 531 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) → 𝑞 < 𝑟)
7041, 44, 45, 68, 69lelttrd 8072 . . . . . . 7 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) → 𝑥 < 𝑟)
7140, 70rexlimddv 2599 . . . . . 6 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) → 𝑥 < 𝑟)
7271ralrimiva 2550 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) → ∀𝑟𝑈 𝑥 < 𝑟)
7332, 72jca 306 . . . 4 (((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) → (∀𝑞𝐿 𝑞 < 𝑥 ∧ ∀𝑟𝑈 𝑥 < 𝑟))
7473ex 115 . . 3 ((𝜑𝑥 ∈ ℝ) → ((∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧)) → (∀𝑞𝐿 𝑞 < 𝑥 ∧ ∀𝑟𝑈 𝑥 < 𝑟)))
7574reximdva 2579 . 2 (𝜑 → (∃𝑥 ∈ ℝ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧)) → ∃𝑥 ∈ ℝ (∀𝑞𝐿 𝑞 < 𝑥 ∧ ∀𝑟𝑈 𝑥 < 𝑟)))
769, 75mpd 13 1 (𝜑 → ∃𝑥 ∈ ℝ (∀𝑞𝐿 𝑞 < 𝑥 ∧ ∀𝑟𝑈 𝑥 < 𝑟))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 708   = wceq 1353  wcel 2148  wral 2455  wrex 2456  cin 3128  wss 3129  c0 3422   class class class wbr 4000  cr 7801   < clt 7982
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-cnex 7893  ax-resscn 7894  ax-pre-ltwlin 7915  ax-pre-suploc 7923
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-br 4001  df-opab 4062  df-xp 4629  df-cnv 4631  df-pnf 7984  df-mnf 7985  df-xr 7986  df-ltxr 7987  df-le 7988
This theorem is referenced by:  dedekindeu  13768
  Copyright terms: Public domain W3C validator