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

Theorem dedekindeulemlu 13352
Description: Lemma for dedekindeu 13354. 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 13351 . 2 (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧)))
10 simpr 109 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) → 𝑞𝐿)
111ad3antrrr 489 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) → 𝐿 ⊆ ℝ)
1211, 10sseldd 3148 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) → 𝑞 ∈ ℝ)
13 rsp 2517 . . . . . . . . . . 11 (∀𝑞 ∈ ℝ (𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟) → (𝑞 ∈ ℝ → (𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟)))
145, 13syl 14 . . . . . . . . . 10 (𝜑 → (𝑞 ∈ ℝ → (𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟)))
1514ad3antrrr 489 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) → (𝑞 ∈ ℝ → (𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟)))
1612, 15mpd 13 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) → (𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟))
1710, 16mpbid 146 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) → ∃𝑟𝐿 𝑞 < 𝑟)
1812adantr 274 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → 𝑞 ∈ ℝ)
1911adantr 274 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → 𝐿 ⊆ ℝ)
20 simprl 526 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → 𝑟𝐿)
2119, 20sseldd 3148 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → 𝑟 ∈ ℝ)
22 simp-4r 537 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → 𝑥 ∈ ℝ)
23 simprr 527 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → 𝑞 < 𝑟)
24 breq2 3991 . . . . . . . . . . 11 (𝑦 = 𝑟 → (𝑥 < 𝑦𝑥 < 𝑟))
2524notbid 662 . . . . . . . . . 10 (𝑦 = 𝑟 → (¬ 𝑥 < 𝑦 ↔ ¬ 𝑥 < 𝑟))
26 simprl 526 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) → ∀𝑦𝐿 ¬ 𝑥 < 𝑦)
2726ad2antrr 485 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → ∀𝑦𝐿 ¬ 𝑥 < 𝑦)
2825, 27, 20rspcdva 2839 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → ¬ 𝑥 < 𝑟)
2921, 22, 28nltled 8027 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → 𝑟𝑥)
3018, 21, 22, 23, 29ltletrd 8329 . . . . . . 7 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → 𝑞 < 𝑥)
3117, 30rexlimddv 2592 . . . . . 6 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) → 𝑞 < 𝑥)
3231ralrimiva 2543 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) → ∀𝑞𝐿 𝑞 < 𝑥)
33 simpr 109 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) → 𝑟𝑈)
34 simplll 528 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) → 𝜑)
3534, 2syl 14 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) → 𝑈 ⊆ ℝ)
3635, 33sseldd 3148 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) → 𝑟 ∈ ℝ)
37 rsp 2517 . . . . . . . . . 10 (∀𝑟 ∈ ℝ (𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟) → (𝑟 ∈ ℝ → (𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟)))
386, 37syl 14 . . . . . . . . 9 (𝜑 → (𝑟 ∈ ℝ → (𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟)))
3934, 36, 38sylc 62 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) → (𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟))
4033, 39mpbid 146 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) → ∃𝑞𝑈 𝑞 < 𝑟)
41 simp-4r 537 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) → 𝑥 ∈ ℝ)
4235adantr 274 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) → 𝑈 ⊆ ℝ)
43 simprl 526 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) → 𝑞𝑈)
4442, 43sseldd 3148 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) → 𝑞 ∈ ℝ)
4536adantr 274 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) → 𝑟 ∈ ℝ)
4643adantr 274 . . . . . . . . . 10 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝑞𝑈)
4734ad2antrr 485 . . . . . . . . . . 11 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝜑)
48 simpr 109 . . . . . . . . . . . . . 14 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝑞 < 𝑥)
49 breq1 3990 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑞 → (𝑦 < 𝑥𝑞 < 𝑥))
50 breq1 3990 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑞 → (𝑦 < 𝑧𝑞 < 𝑧))
5150rexbidv 2471 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑞 → (∃𝑧𝐿 𝑦 < 𝑧 ↔ ∃𝑧𝐿 𝑞 < 𝑧))
5249, 51imbi12d 233 . . . . . . . . . . . . . . 15 (𝑦 = 𝑞 → ((𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧) ↔ (𝑞 < 𝑥 → ∃𝑧𝐿 𝑞 < 𝑧)))
53 simprr 527 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) → ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))
5453ad3antrrr 489 . . . . . . . . . . . . . . 15 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))
5544adantr 274 . . . . . . . . . . . . . . 15 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝑞 ∈ ℝ)
5652, 54, 55rspcdva 2839 . . . . . . . . . . . . . 14 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → (𝑞 < 𝑥 → ∃𝑧𝐿 𝑞 < 𝑧))
5748, 56mpd 13 . . . . . . . . . . . . 13 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → ∃𝑧𝐿 𝑞 < 𝑧)
58 breq2 3991 . . . . . . . . . . . . . 14 (𝑧 = 𝑟 → (𝑞 < 𝑧𝑞 < 𝑟))
5958cbvrexv 2697 . . . . . . . . . . . . 13 (∃𝑧𝐿 𝑞 < 𝑧 ↔ ∃𝑟𝐿 𝑞 < 𝑟)
6057, 59sylib 121 . . . . . . . . . . . 12 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → ∃𝑟𝐿 𝑞 < 𝑟)
6147, 55, 14sylc 62 . . . . . . . . . . . 12 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → (𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟))
6260, 61mpbird 166 . . . . . . . . . . 11 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝑞𝐿)
63 disj 3462 . . . . . . . . . . . . 13 ((𝐿𝑈) = ∅ ↔ ∀𝑞𝐿 ¬ 𝑞𝑈)
647, 63sylib 121 . . . . . . . . . . . 12 (𝜑 → ∀𝑞𝐿 ¬ 𝑞𝑈)
6564r19.21bi 2558 . . . . . . . . . . 11 ((𝜑𝑞𝐿) → ¬ 𝑞𝑈)
6647, 62, 65syl2anc 409 . . . . . . . . . 10 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → ¬ 𝑞𝑈)
6746, 66pm2.65da 656 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) → ¬ 𝑞 < 𝑥)
6841, 44, 67nltled 8027 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) → 𝑥𝑞)
69 simprr 527 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) → 𝑞 < 𝑟)
7041, 44, 45, 68, 69lelttrd 8031 . . . . . . 7 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) → 𝑥 < 𝑟)
7140, 70rexlimddv 2592 . . . . . 6 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) → 𝑥 < 𝑟)
7271ralrimiva 2543 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) → ∀𝑟𝑈 𝑥 < 𝑟)
7332, 72jca 304 . . . 4 (((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) → (∀𝑞𝐿 𝑞 < 𝑥 ∧ ∀𝑟𝑈 𝑥 < 𝑟))
7473ex 114 . . 3 ((𝜑𝑥 ∈ ℝ) → ((∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧)) → (∀𝑞𝐿 𝑞 < 𝑥 ∧ ∀𝑟𝑈 𝑥 < 𝑟)))
7574reximdva 2572 . 2 (𝜑 → (∃𝑥 ∈ ℝ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧)) → ∃𝑥 ∈ ℝ (∀𝑞𝐿 𝑞 < 𝑥 ∧ ∀𝑟𝑈 𝑥 < 𝑟)))
769, 75mpd 13 1 (𝜑 → ∃𝑥 ∈ ℝ (∀𝑞𝐿 𝑞 < 𝑥 ∧ ∀𝑟𝑈 𝑥 < 𝑟))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104  wo 703   = wceq 1348  wcel 2141  wral 2448  wrex 2449  cin 3120  wss 3121  c0 3414   class class class wbr 3987  cr 7760   < clt 7941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-sep 4105  ax-pow 4158  ax-pr 4192  ax-un 4416  ax-setind 4519  ax-cnex 7852  ax-resscn 7853  ax-pre-ltwlin 7874  ax-pre-suploc 7882
This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-rab 2457  df-v 2732  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-pw 3566  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-br 3988  df-opab 4049  df-xp 4615  df-cnv 4617  df-pnf 7943  df-mnf 7944  df-xr 7945  df-ltxr 7946  df-le 7947
This theorem is referenced by:  dedekindeu  13354
  Copyright terms: Public domain W3C validator