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

Theorem suplocexprlemru 7681
Description: Lemma for suplocexpr 7687. The upper cut of the putative supremum is rounded. (Contributed by Jim Kingdon, 9-Jan-2024.)
Hypotheses
Ref Expression
suplocexpr.m (𝜑 → ∃𝑥 𝑥𝐴)
suplocexpr.ub (𝜑 → ∃𝑥P𝑦𝐴 𝑦<P 𝑥)
suplocexpr.loc (𝜑 → ∀𝑥P𝑦P (𝑥<P 𝑦 → (∃𝑧𝐴 𝑥<P 𝑧 ∨ ∀𝑧𝐴 𝑧<P 𝑦)))
suplocexpr.b 𝐵 = ⟨ (1st𝐴), {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}⟩
Assertion
Ref Expression
suplocexprlemru (𝜑 → ∀𝑟Q (𝑟 ∈ (2nd𝐵) ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))))
Distinct variable groups:   𝐴,𝑞,𝑢   𝑥,𝐴,𝑦   𝐵,𝑞,𝑤   𝜑,𝑞,𝑟,𝑤   𝜑,𝑥,𝑦   𝑢,𝑟,𝑤
Allowed substitution hints:   𝜑(𝑧,𝑢)   𝐴(𝑧,𝑤,𝑟)   𝐵(𝑥,𝑦,𝑧,𝑢,𝑟)

Proof of Theorem suplocexprlemru
StepHypRef Expression
1 suplocexpr.m . . . . . . . . . . . 12 (𝜑 → ∃𝑥 𝑥𝐴)
2 suplocexpr.ub . . . . . . . . . . . 12 (𝜑 → ∃𝑥P𝑦𝐴 𝑦<P 𝑥)
3 suplocexpr.loc . . . . . . . . . . . 12 (𝜑 → ∀𝑥P𝑦P (𝑥<P 𝑦 → (∃𝑧𝐴 𝑥<P 𝑧 ∨ ∀𝑧𝐴 𝑧<P 𝑦)))
41, 2, 3suplocexprlemss 7677 . . . . . . . . . . 11 (𝜑𝐴P)
5 suplocexpr.b . . . . . . . . . . . 12 𝐵 = ⟨ (1st𝐴), {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}⟩
65suplocexprlem2b 7676 . . . . . . . . . . 11 (𝐴P → (2nd𝐵) = {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢})
74, 6syl 14 . . . . . . . . . 10 (𝜑 → (2nd𝐵) = {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢})
87eleq2d 2240 . . . . . . . . 9 (𝜑 → (𝑟 ∈ (2nd𝐵) ↔ 𝑟 ∈ {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}))
98adantr 274 . . . . . . . 8 ((𝜑𝑟Q) → (𝑟 ∈ (2nd𝐵) ↔ 𝑟 ∈ {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}))
109biimpa 294 . . . . . . 7 (((𝜑𝑟Q) ∧ 𝑟 ∈ (2nd𝐵)) → 𝑟 ∈ {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢})
11 breq2 3993 . . . . . . . . 9 (𝑢 = 𝑟 → (𝑤 <Q 𝑢𝑤 <Q 𝑟))
1211rexbidv 2471 . . . . . . . 8 (𝑢 = 𝑟 → (∃𝑤 (2nd𝐴)𝑤 <Q 𝑢 ↔ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑟))
1312elrab 2886 . . . . . . 7 (𝑟 ∈ {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢} ↔ (𝑟Q ∧ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑟))
1410, 13sylib 121 . . . . . 6 (((𝜑𝑟Q) ∧ 𝑟 ∈ (2nd𝐵)) → (𝑟Q ∧ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑟))
1514simprd 113 . . . . 5 (((𝜑𝑟Q) ∧ 𝑟 ∈ (2nd𝐵)) → ∃𝑤 (2nd𝐴)𝑤 <Q 𝑟)
16 ltbtwnnqq 7377 . . . . . . . 8 (𝑤 <Q 𝑟 ↔ ∃𝑞Q (𝑤 <Q 𝑞𝑞 <Q 𝑟))
1716biimpi 119 . . . . . . 7 (𝑤 <Q 𝑟 → ∃𝑞Q (𝑤 <Q 𝑞𝑞 <Q 𝑟))
1817ad2antll 488 . . . . . 6 ((((𝜑𝑟Q) ∧ 𝑟 ∈ (2nd𝐵)) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑟)) → ∃𝑞Q (𝑤 <Q 𝑞𝑞 <Q 𝑟))
19 simprr 527 . . . . . . . . 9 ((((((𝜑𝑟Q) ∧ 𝑟 ∈ (2nd𝐵)) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑟)) ∧ 𝑞Q) ∧ (𝑤 <Q 𝑞𝑞 <Q 𝑟)) → 𝑞 <Q 𝑟)
20 breq2 3993 . . . . . . . . . . . 12 (𝑢 = 𝑞 → (𝑤 <Q 𝑢𝑤 <Q 𝑞))
2120rexbidv 2471 . . . . . . . . . . 11 (𝑢 = 𝑞 → (∃𝑤 (2nd𝐴)𝑤 <Q 𝑢 ↔ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑞))
22 simplr 525 . . . . . . . . . . 11 ((((((𝜑𝑟Q) ∧ 𝑟 ∈ (2nd𝐵)) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑟)) ∧ 𝑞Q) ∧ (𝑤 <Q 𝑞𝑞 <Q 𝑟)) → 𝑞Q)
23 simprl 526 . . . . . . . . . . . . . 14 ((((𝜑𝑟Q) ∧ 𝑟 ∈ (2nd𝐵)) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑟)) → 𝑤 (2nd𝐴))
2423ad2antrr 485 . . . . . . . . . . . . 13 ((((((𝜑𝑟Q) ∧ 𝑟 ∈ (2nd𝐵)) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑟)) ∧ 𝑞Q) ∧ (𝑤 <Q 𝑞𝑞 <Q 𝑟)) → 𝑤 (2nd𝐴))
25 simprl 526 . . . . . . . . . . . . 13 ((((((𝜑𝑟Q) ∧ 𝑟 ∈ (2nd𝐵)) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑟)) ∧ 𝑞Q) ∧ (𝑤 <Q 𝑞𝑞 <Q 𝑟)) → 𝑤 <Q 𝑞)
2624, 25jca 304 . . . . . . . . . . . 12 ((((((𝜑𝑟Q) ∧ 𝑟 ∈ (2nd𝐵)) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑟)) ∧ 𝑞Q) ∧ (𝑤 <Q 𝑞𝑞 <Q 𝑟)) → (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑞))
27 rspe 2519 . . . . . . . . . . . 12 ((𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑞) → ∃𝑤 (2nd𝐴)𝑤 <Q 𝑞)
2826, 27syl 14 . . . . . . . . . . 11 ((((((𝜑𝑟Q) ∧ 𝑟 ∈ (2nd𝐵)) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑟)) ∧ 𝑞Q) ∧ (𝑤 <Q 𝑞𝑞 <Q 𝑟)) → ∃𝑤 (2nd𝐴)𝑤 <Q 𝑞)
2921, 22, 28elrabd 2888 . . . . . . . . . 10 ((((((𝜑𝑟Q) ∧ 𝑟 ∈ (2nd𝐵)) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑟)) ∧ 𝑞Q) ∧ (𝑤 <Q 𝑞𝑞 <Q 𝑟)) → 𝑞 ∈ {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢})
307eleq2d 2240 . . . . . . . . . . 11 (𝜑 → (𝑞 ∈ (2nd𝐵) ↔ 𝑞 ∈ {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}))
3130ad5antr 493 . . . . . . . . . 10 ((((((𝜑𝑟Q) ∧ 𝑟 ∈ (2nd𝐵)) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑟)) ∧ 𝑞Q) ∧ (𝑤 <Q 𝑞𝑞 <Q 𝑟)) → (𝑞 ∈ (2nd𝐵) ↔ 𝑞 ∈ {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}))
3229, 31mpbird 166 . . . . . . . . 9 ((((((𝜑𝑟Q) ∧ 𝑟 ∈ (2nd𝐵)) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑟)) ∧ 𝑞Q) ∧ (𝑤 <Q 𝑞𝑞 <Q 𝑟)) → 𝑞 ∈ (2nd𝐵))
3319, 32jca 304 . . . . . . . 8 ((((((𝜑𝑟Q) ∧ 𝑟 ∈ (2nd𝐵)) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑟)) ∧ 𝑞Q) ∧ (𝑤 <Q 𝑞𝑞 <Q 𝑟)) → (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵)))
3433ex 114 . . . . . . 7 (((((𝜑𝑟Q) ∧ 𝑟 ∈ (2nd𝐵)) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑟)) ∧ 𝑞Q) → ((𝑤 <Q 𝑞𝑞 <Q 𝑟) → (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))))
3534reximdva 2572 . . . . . 6 ((((𝜑𝑟Q) ∧ 𝑟 ∈ (2nd𝐵)) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑟)) → (∃𝑞Q (𝑤 <Q 𝑞𝑞 <Q 𝑟) → ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))))
3618, 35mpd 13 . . . . 5 ((((𝜑𝑟Q) ∧ 𝑟 ∈ (2nd𝐵)) ∧ (𝑤 (2nd𝐴) ∧ 𝑤 <Q 𝑟)) → ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵)))
3715, 36rexlimddv 2592 . . . 4 (((𝜑𝑟Q) ∧ 𝑟 ∈ (2nd𝐵)) → ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵)))
3837ex 114 . . 3 ((𝜑𝑟Q) → (𝑟 ∈ (2nd𝐵) → ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))))
39 simpllr 529 . . . . . 6 ((((𝜑𝑟Q) ∧ 𝑞Q) ∧ (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))) → 𝑟Q)
40 simprr 527 . . . . . . . . . 10 ((((𝜑𝑟Q) ∧ 𝑞Q) ∧ (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))) → 𝑞 ∈ (2nd𝐵))
4130ad3antrrr 489 . . . . . . . . . 10 ((((𝜑𝑟Q) ∧ 𝑞Q) ∧ (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))) → (𝑞 ∈ (2nd𝐵) ↔ 𝑞 ∈ {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}))
4240, 41mpbid 146 . . . . . . . . 9 ((((𝜑𝑟Q) ∧ 𝑞Q) ∧ (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))) → 𝑞 ∈ {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢})
4321elrab 2886 . . . . . . . . 9 (𝑞 ∈ {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢} ↔ (𝑞Q ∧ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑞))
4442, 43sylib 121 . . . . . . . 8 ((((𝜑𝑟Q) ∧ 𝑞Q) ∧ (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))) → (𝑞Q ∧ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑞))
4544simprd 113 . . . . . . 7 ((((𝜑𝑟Q) ∧ 𝑞Q) ∧ (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))) → ∃𝑤 (2nd𝐴)𝑤 <Q 𝑞)
46 simpr 109 . . . . . . . . . . 11 ((((((𝜑𝑟Q) ∧ 𝑞Q) ∧ (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))) ∧ 𝑤 (2nd𝐴)) ∧ 𝑤 <Q 𝑞) → 𝑤 <Q 𝑞)
47 simprl 526 . . . . . . . . . . . 12 ((((𝜑𝑟Q) ∧ 𝑞Q) ∧ (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))) → 𝑞 <Q 𝑟)
4847ad2antrr 485 . . . . . . . . . . 11 ((((((𝜑𝑟Q) ∧ 𝑞Q) ∧ (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))) ∧ 𝑤 (2nd𝐴)) ∧ 𝑤 <Q 𝑞) → 𝑞 <Q 𝑟)
4946, 48jca 304 . . . . . . . . . 10 ((((((𝜑𝑟Q) ∧ 𝑞Q) ∧ (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))) ∧ 𝑤 (2nd𝐴)) ∧ 𝑤 <Q 𝑞) → (𝑤 <Q 𝑞𝑞 <Q 𝑟))
50 ltrelnq 7327 . . . . . . . . . . . . . 14 <Q ⊆ (Q × Q)
5150brel 4663 . . . . . . . . . . . . 13 (𝑤 <Q 𝑞 → (𝑤Q𝑞Q))
5251simpld 111 . . . . . . . . . . . 12 (𝑤 <Q 𝑞𝑤Q)
5352adantl 275 . . . . . . . . . . 11 ((((((𝜑𝑟Q) ∧ 𝑞Q) ∧ (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))) ∧ 𝑤 (2nd𝐴)) ∧ 𝑤 <Q 𝑞) → 𝑤Q)
54 simp-4r 537 . . . . . . . . . . 11 ((((((𝜑𝑟Q) ∧ 𝑞Q) ∧ (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))) ∧ 𝑤 (2nd𝐴)) ∧ 𝑤 <Q 𝑞) → 𝑞Q)
5539ad2antrr 485 . . . . . . . . . . 11 ((((((𝜑𝑟Q) ∧ 𝑞Q) ∧ (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))) ∧ 𝑤 (2nd𝐴)) ∧ 𝑤 <Q 𝑞) → 𝑟Q)
56 ltsonq 7360 . . . . . . . . . . . 12 <Q Or Q
57 sotr 4303 . . . . . . . . . . . 12 (( <Q Or Q ∧ (𝑤Q𝑞Q𝑟Q)) → ((𝑤 <Q 𝑞𝑞 <Q 𝑟) → 𝑤 <Q 𝑟))
5856, 57mpan 422 . . . . . . . . . . 11 ((𝑤Q𝑞Q𝑟Q) → ((𝑤 <Q 𝑞𝑞 <Q 𝑟) → 𝑤 <Q 𝑟))
5953, 54, 55, 58syl3anc 1233 . . . . . . . . . 10 ((((((𝜑𝑟Q) ∧ 𝑞Q) ∧ (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))) ∧ 𝑤 (2nd𝐴)) ∧ 𝑤 <Q 𝑞) → ((𝑤 <Q 𝑞𝑞 <Q 𝑟) → 𝑤 <Q 𝑟))
6049, 59mpd 13 . . . . . . . . 9 ((((((𝜑𝑟Q) ∧ 𝑞Q) ∧ (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))) ∧ 𝑤 (2nd𝐴)) ∧ 𝑤 <Q 𝑞) → 𝑤 <Q 𝑟)
6160ex 114 . . . . . . . 8 (((((𝜑𝑟Q) ∧ 𝑞Q) ∧ (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))) ∧ 𝑤 (2nd𝐴)) → (𝑤 <Q 𝑞𝑤 <Q 𝑟))
6261reximdva 2572 . . . . . . 7 ((((𝜑𝑟Q) ∧ 𝑞Q) ∧ (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))) → (∃𝑤 (2nd𝐴)𝑤 <Q 𝑞 → ∃𝑤 (2nd𝐴)𝑤 <Q 𝑟))
6345, 62mpd 13 . . . . . 6 ((((𝜑𝑟Q) ∧ 𝑞Q) ∧ (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))) → ∃𝑤 (2nd𝐴)𝑤 <Q 𝑟)
6412, 39, 63elrabd 2888 . . . . 5 ((((𝜑𝑟Q) ∧ 𝑞Q) ∧ (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))) → 𝑟 ∈ {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢})
658ad3antrrr 489 . . . . 5 ((((𝜑𝑟Q) ∧ 𝑞Q) ∧ (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))) → (𝑟 ∈ (2nd𝐵) ↔ 𝑟 ∈ {𝑢Q ∣ ∃𝑤 (2nd𝐴)𝑤 <Q 𝑢}))
6664, 65mpbird 166 . . . 4 ((((𝜑𝑟Q) ∧ 𝑞Q) ∧ (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))) → 𝑟 ∈ (2nd𝐵))
6766rexlimdva2 2590 . . 3 ((𝜑𝑟Q) → (∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵)) → 𝑟 ∈ (2nd𝐵)))
6838, 67impbid 128 . 2 ((𝜑𝑟Q) → (𝑟 ∈ (2nd𝐵) ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))))
6968ralrimiva 2543 1 (𝜑 → ∀𝑟Q (𝑟 ∈ (2nd𝐵) ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  wo 703  w3a 973   = wceq 1348  wex 1485  wcel 2141  wral 2448  wrex 2449  {crab 2452  wss 3121  cop 3586   cuni 3796   cint 3831   class class class wbr 3989   Or wor 4280  cima 4614  cfv 5198  1st c1st 6117  2nd c2nd 6118  Qcnq 7242   <Q cltq 7247  Pcnp 7253  <P cltp 7257
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-coll 4104  ax-sep 4107  ax-nul 4115  ax-pow 4160  ax-pr 4194  ax-un 4418  ax-setind 4521  ax-iinf 4572
This theorem depends on definitions:  df-bi 116  df-dc 830  df-3or 974  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-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-int 3832  df-iun 3875  df-br 3990  df-opab 4051  df-mpt 4052  df-tr 4088  df-eprel 4274  df-id 4278  df-po 4281  df-iso 4282  df-iord 4351  df-on 4353  df-suc 4356  df-iom 4575  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-f1 5203  df-fo 5204  df-f1o 5205  df-fv 5206  df-ov 5856  df-oprab 5857  df-mpo 5858  df-1st 6119  df-2nd 6120  df-recs 6284  df-irdg 6349  df-1o 6395  df-oadd 6399  df-omul 6400  df-er 6513  df-ec 6515  df-qs 6519  df-ni 7266  df-pli 7267  df-mi 7268  df-lti 7269  df-plpq 7306  df-mpq 7307  df-enq 7309  df-nqqs 7310  df-plqqs 7311  df-mqqs 7312  df-1nqqs 7313  df-rq 7314  df-ltnqqs 7315  df-inp 7428  df-iltp 7432
This theorem is referenced by:  suplocexprlemex  7684
  Copyright terms: Public domain W3C validator