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

Theorem dedekindeulemlu 12757
Description: Lemma for dedekindeu 12759. 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 12756 . 2 (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧)))
10 simpr 109 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) → 𝑞𝐿)
111ad3antrrr 483 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) → 𝐿 ⊆ ℝ)
1211, 10sseldd 3093 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) → 𝑞 ∈ ℝ)
13 rsp 2478 . . . . . . . . . . 11 (∀𝑞 ∈ ℝ (𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟) → (𝑞 ∈ ℝ → (𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟)))
145, 13syl 14 . . . . . . . . . 10 (𝜑 → (𝑞 ∈ ℝ → (𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟)))
1514ad3antrrr 483 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) → (𝑞 ∈ ℝ → (𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟)))
1612, 15mpd 13 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) → (𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟))
1710, 16mpbid 146 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) → ∃𝑟𝐿 𝑞 < 𝑟)
1812adantr 274 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → 𝑞 ∈ ℝ)
1911adantr 274 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → 𝐿 ⊆ ℝ)
20 simprl 520 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → 𝑟𝐿)
2119, 20sseldd 3093 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → 𝑟 ∈ ℝ)
22 simp-4r 531 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → 𝑥 ∈ ℝ)
23 simprr 521 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → 𝑞 < 𝑟)
24 breq2 3928 . . . . . . . . . . 11 (𝑦 = 𝑟 → (𝑥 < 𝑦𝑥 < 𝑟))
2524notbid 656 . . . . . . . . . 10 (𝑦 = 𝑟 → (¬ 𝑥 < 𝑦 ↔ ¬ 𝑥 < 𝑟))
26 simprl 520 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) → ∀𝑦𝐿 ¬ 𝑥 < 𝑦)
2726ad2antrr 479 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → ∀𝑦𝐿 ¬ 𝑥 < 𝑦)
2825, 27, 20rspcdva 2789 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → ¬ 𝑥 < 𝑟)
2921, 22, 28nltled 7876 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → 𝑟𝑥)
3018, 21, 22, 23, 29ltletrd 8178 . . . . . . 7 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) ∧ (𝑟𝐿𝑞 < 𝑟)) → 𝑞 < 𝑥)
3117, 30rexlimddv 2552 . . . . . 6 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑞𝐿) → 𝑞 < 𝑥)
3231ralrimiva 2503 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) → ∀𝑞𝐿 𝑞 < 𝑥)
33 simpr 109 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) → 𝑟𝑈)
34 simplll 522 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) → 𝜑)
3534, 2syl 14 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) → 𝑈 ⊆ ℝ)
3635, 33sseldd 3093 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) → 𝑟 ∈ ℝ)
37 rsp 2478 . . . . . . . . . 10 (∀𝑟 ∈ ℝ (𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟) → (𝑟 ∈ ℝ → (𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟)))
386, 37syl 14 . . . . . . . . 9 (𝜑 → (𝑟 ∈ ℝ → (𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟)))
3934, 36, 38sylc 62 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) → (𝑟𝑈 ↔ ∃𝑞𝑈 𝑞 < 𝑟))
4033, 39mpbid 146 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) → ∃𝑞𝑈 𝑞 < 𝑟)
41 simp-4r 531 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) → 𝑥 ∈ ℝ)
4235adantr 274 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) → 𝑈 ⊆ ℝ)
43 simprl 520 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) → 𝑞𝑈)
4442, 43sseldd 3093 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) → 𝑞 ∈ ℝ)
4536adantr 274 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) → 𝑟 ∈ ℝ)
4643adantr 274 . . . . . . . . . 10 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝑞𝑈)
4734ad2antrr 479 . . . . . . . . . . 11 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝜑)
48 simpr 109 . . . . . . . . . . . . . 14 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝑞 < 𝑥)
49 breq1 3927 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑞 → (𝑦 < 𝑥𝑞 < 𝑥))
50 breq1 3927 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑞 → (𝑦 < 𝑧𝑞 < 𝑧))
5150rexbidv 2436 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑞 → (∃𝑧𝐿 𝑦 < 𝑧 ↔ ∃𝑧𝐿 𝑞 < 𝑧))
5249, 51imbi12d 233 . . . . . . . . . . . . . . 15 (𝑦 = 𝑞 → ((𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧) ↔ (𝑞 < 𝑥 → ∃𝑧𝐿 𝑞 < 𝑧)))
53 simprr 521 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) → ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))
5453ad3antrrr 483 . . . . . . . . . . . . . . 15 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))
5544adantr 274 . . . . . . . . . . . . . . 15 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝑞 ∈ ℝ)
5652, 54, 55rspcdva 2789 . . . . . . . . . . . . . 14 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → (𝑞 < 𝑥 → ∃𝑧𝐿 𝑞 < 𝑧))
5748, 56mpd 13 . . . . . . . . . . . . 13 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → ∃𝑧𝐿 𝑞 < 𝑧)
58 breq2 3928 . . . . . . . . . . . . . 14 (𝑧 = 𝑟 → (𝑞 < 𝑧𝑞 < 𝑟))
5958cbvrexv 2653 . . . . . . . . . . . . 13 (∃𝑧𝐿 𝑞 < 𝑧 ↔ ∃𝑟𝐿 𝑞 < 𝑟)
6057, 59sylib 121 . . . . . . . . . . . 12 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → ∃𝑟𝐿 𝑞 < 𝑟)
6147, 55, 14sylc 62 . . . . . . . . . . . 12 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → (𝑞𝐿 ↔ ∃𝑟𝐿 𝑞 < 𝑟))
6260, 61mpbird 166 . . . . . . . . . . 11 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝑞𝐿)
63 disj 3406 . . . . . . . . . . . . 13 ((𝐿𝑈) = ∅ ↔ ∀𝑞𝐿 ¬ 𝑞𝑈)
647, 63sylib 121 . . . . . . . . . . . 12 (𝜑 → ∀𝑞𝐿 ¬ 𝑞𝑈)
6564r19.21bi 2518 . . . . . . . . . . 11 ((𝜑𝑞𝐿) → ¬ 𝑞𝑈)
6647, 62, 65syl2anc 408 . . . . . . . . . 10 ((((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → ¬ 𝑞𝑈)
6746, 66pm2.65da 650 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) → ¬ 𝑞 < 𝑥)
6841, 44, 67nltled 7876 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) → 𝑥𝑞)
69 simprr 521 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) → 𝑞 < 𝑟)
7041, 44, 45, 68, 69lelttrd 7880 . . . . . . 7 (((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) ∧ (𝑞𝑈𝑞 < 𝑟)) → 𝑥 < 𝑟)
7140, 70rexlimddv 2552 . . . . . 6 ((((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) ∧ 𝑟𝑈) → 𝑥 < 𝑟)
7271ralrimiva 2503 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) → ∀𝑟𝑈 𝑥 < 𝑟)
7332, 72jca 304 . . . 4 (((𝜑𝑥 ∈ ℝ) ∧ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧))) → (∀𝑞𝐿 𝑞 < 𝑥 ∧ ∀𝑟𝑈 𝑥 < 𝑟))
7473ex 114 . . 3 ((𝜑𝑥 ∈ ℝ) → ((∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧)) → (∀𝑞𝐿 𝑞 < 𝑥 ∧ ∀𝑟𝑈 𝑥 < 𝑟)))
7574reximdva 2532 . 2 (𝜑 → (∃𝑥 ∈ ℝ (∀𝑦𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐿 𝑦 < 𝑧)) → ∃𝑥 ∈ ℝ (∀𝑞𝐿 𝑞 < 𝑥 ∧ ∀𝑟𝑈 𝑥 < 𝑟)))
769, 75mpd 13 1 (𝜑 → ∃𝑥 ∈ ℝ (∀𝑞𝐿 𝑞 < 𝑥 ∧ ∀𝑟𝑈 𝑥 < 𝑟))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104  wo 697   = wceq 1331  wcel 1480  wral 2414  wrex 2415  cin 3065  wss 3066  c0 3358   class class class wbr 3924  cr 7612   < clt 7793
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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-sep 4041  ax-pow 4093  ax-pr 4126  ax-un 4350  ax-setind 4447  ax-cnex 7704  ax-resscn 7705  ax-pre-ltwlin 7726  ax-pre-suploc 7734
This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2000  df-mo 2001  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-ne 2307  df-nel 2402  df-ral 2419  df-rex 2420  df-rab 2423  df-v 2683  df-dif 3068  df-un 3070  df-in 3072  df-ss 3079  df-nul 3359  df-pw 3507  df-sn 3528  df-pr 3529  df-op 3531  df-uni 3732  df-br 3925  df-opab 3985  df-xp 4540  df-cnv 4542  df-pnf 7795  df-mnf 7796  df-xr 7797  df-ltxr 7798  df-le 7799
This theorem is referenced by:  dedekindeu  12759
  Copyright terms: Public domain W3C validator