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

Theorem ltsopr 7455
 Description: Positive real 'less than' is a weak linear order (in the sense of df-iso 4229). Proposition 11.2.3 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 16-Dec-2019.)
Assertion
Ref Expression
ltsopr <P Or P

Proof of Theorem ltsopr
Dummy variables 𝑟 𝑞 𝑠 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ltpopr 7454 . 2 <P Po P
2 ltdfpr 7365 . . . . 5 ((𝑥P𝑦P) → (𝑥<P 𝑦 ↔ ∃𝑞Q (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))))
323adant3 1002 . . . 4 ((𝑥P𝑦P𝑧P) → (𝑥<P 𝑦 ↔ ∃𝑞Q (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))))
4 prop 7334 . . . . . . . . . . . 12 (𝑥P → ⟨(1st𝑥), (2nd𝑥)⟩ ∈ P)
5 prnminu 7348 . . . . . . . . . . . 12 ((⟨(1st𝑥), (2nd𝑥)⟩ ∈ P𝑞 ∈ (2nd𝑥)) → ∃𝑟 ∈ (2nd𝑥)𝑟 <Q 𝑞)
64, 5sylan 281 . . . . . . . . . . 11 ((𝑥P𝑞 ∈ (2nd𝑥)) → ∃𝑟 ∈ (2nd𝑥)𝑟 <Q 𝑞)
7 prop 7334 . . . . . . . . . . . 12 (𝑦P → ⟨(1st𝑦), (2nd𝑦)⟩ ∈ P)
8 prnmaxl 7347 . . . . . . . . . . . 12 ((⟨(1st𝑦), (2nd𝑦)⟩ ∈ P𝑞 ∈ (1st𝑦)) → ∃𝑠 ∈ (1st𝑦)𝑞 <Q 𝑠)
97, 8sylan 281 . . . . . . . . . . 11 ((𝑦P𝑞 ∈ (1st𝑦)) → ∃𝑠 ∈ (1st𝑦)𝑞 <Q 𝑠)
106, 9anim12i 336 . . . . . . . . . 10 (((𝑥P𝑞 ∈ (2nd𝑥)) ∧ (𝑦P𝑞 ∈ (1st𝑦))) → (∃𝑟 ∈ (2nd𝑥)𝑟 <Q 𝑞 ∧ ∃𝑠 ∈ (1st𝑦)𝑞 <Q 𝑠))
1110an4s 578 . . . . . . . . 9 (((𝑥P𝑦P) ∧ (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))) → (∃𝑟 ∈ (2nd𝑥)𝑟 <Q 𝑞 ∧ ∃𝑠 ∈ (1st𝑦)𝑞 <Q 𝑠))
12 reeanv 2604 . . . . . . . . 9 (∃𝑟 ∈ (2nd𝑥)∃𝑠 ∈ (1st𝑦)(𝑟 <Q 𝑞𝑞 <Q 𝑠) ↔ (∃𝑟 ∈ (2nd𝑥)𝑟 <Q 𝑞 ∧ ∃𝑠 ∈ (1st𝑦)𝑞 <Q 𝑠))
1311, 12sylibr 133 . . . . . . . 8 (((𝑥P𝑦P) ∧ (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))) → ∃𝑟 ∈ (2nd𝑥)∃𝑠 ∈ (1st𝑦)(𝑟 <Q 𝑞𝑞 <Q 𝑠))
14133adantl3 1140 . . . . . . 7 (((𝑥P𝑦P𝑧P) ∧ (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))) → ∃𝑟 ∈ (2nd𝑥)∃𝑠 ∈ (1st𝑦)(𝑟 <Q 𝑞𝑞 <Q 𝑠))
15 ltsonq 7257 . . . . . . . . . . . . 13 <Q Or Q
16 ltrelnq 7224 . . . . . . . . . . . . 13 <Q ⊆ (Q × Q)
1715, 16sotri 4945 . . . . . . . . . . . 12 ((𝑟 <Q 𝑞𝑞 <Q 𝑠) → 𝑟 <Q 𝑠)
1817adantl 275 . . . . . . . . . . 11 (((((𝑥P𝑦P𝑧P) ∧ (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))) ∧ (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (1st𝑦))) ∧ (𝑟 <Q 𝑞𝑞 <Q 𝑠)) → 𝑟 <Q 𝑠)
19 prop 7334 . . . . . . . . . . . . . . . 16 (𝑧P → ⟨(1st𝑧), (2nd𝑧)⟩ ∈ P)
20 prloc 7350 . . . . . . . . . . . . . . . 16 ((⟨(1st𝑧), (2nd𝑧)⟩ ∈ P𝑟 <Q 𝑠) → (𝑟 ∈ (1st𝑧) ∨ 𝑠 ∈ (2nd𝑧)))
2119, 20sylan 281 . . . . . . . . . . . . . . 15 ((𝑧P𝑟 <Q 𝑠) → (𝑟 ∈ (1st𝑧) ∨ 𝑠 ∈ (2nd𝑧)))
22213ad2antl3 1146 . . . . . . . . . . . . . 14 (((𝑥P𝑦P𝑧P) ∧ 𝑟 <Q 𝑠) → (𝑟 ∈ (1st𝑧) ∨ 𝑠 ∈ (2nd𝑧)))
2322ex 114 . . . . . . . . . . . . 13 ((𝑥P𝑦P𝑧P) → (𝑟 <Q 𝑠 → (𝑟 ∈ (1st𝑧) ∨ 𝑠 ∈ (2nd𝑧))))
2423adantr 274 . . . . . . . . . . . 12 (((𝑥P𝑦P𝑧P) ∧ (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))) → (𝑟 <Q 𝑠 → (𝑟 ∈ (1st𝑧) ∨ 𝑠 ∈ (2nd𝑧))))
2524ad2antrr 480 . . . . . . . . . . 11 (((((𝑥P𝑦P𝑧P) ∧ (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))) ∧ (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (1st𝑦))) ∧ (𝑟 <Q 𝑞𝑞 <Q 𝑠)) → (𝑟 <Q 𝑠 → (𝑟 ∈ (1st𝑧) ∨ 𝑠 ∈ (2nd𝑧))))
2618, 25mpd 13 . . . . . . . . . 10 (((((𝑥P𝑦P𝑧P) ∧ (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))) ∧ (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (1st𝑦))) ∧ (𝑟 <Q 𝑞𝑞 <Q 𝑠)) → (𝑟 ∈ (1st𝑧) ∨ 𝑠 ∈ (2nd𝑧)))
27 elprnqu 7341 . . . . . . . . . . . . . . . . . . . . 21 ((⟨(1st𝑥), (2nd𝑥)⟩ ∈ P𝑟 ∈ (2nd𝑥)) → 𝑟Q)
284, 27sylan 281 . . . . . . . . . . . . . . . . . . . 20 ((𝑥P𝑟 ∈ (2nd𝑥)) → 𝑟Q)
29 ax-ia3 107 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 ∈ (2nd𝑥) → (𝑟 ∈ (1st𝑧) → (𝑟 ∈ (2nd𝑥) ∧ 𝑟 ∈ (1st𝑧))))
3029adantl 275 . . . . . . . . . . . . . . . . . . . 20 ((𝑥P𝑟 ∈ (2nd𝑥)) → (𝑟 ∈ (1st𝑧) → (𝑟 ∈ (2nd𝑥) ∧ 𝑟 ∈ (1st𝑧))))
31 19.8a 1570 . . . . . . . . . . . . . . . . . . . 20 ((𝑟Q ∧ (𝑟 ∈ (2nd𝑥) ∧ 𝑟 ∈ (1st𝑧))) → ∃𝑟(𝑟Q ∧ (𝑟 ∈ (2nd𝑥) ∧ 𝑟 ∈ (1st𝑧))))
3228, 30, 31syl6an 1411 . . . . . . . . . . . . . . . . . . 19 ((𝑥P𝑟 ∈ (2nd𝑥)) → (𝑟 ∈ (1st𝑧) → ∃𝑟(𝑟Q ∧ (𝑟 ∈ (2nd𝑥) ∧ 𝑟 ∈ (1st𝑧)))))
33323ad2antl1 1144 . . . . . . . . . . . . . . . . . 18 (((𝑥P𝑦P𝑧P) ∧ 𝑟 ∈ (2nd𝑥)) → (𝑟 ∈ (1st𝑧) → ∃𝑟(𝑟Q ∧ (𝑟 ∈ (2nd𝑥) ∧ 𝑟 ∈ (1st𝑧)))))
3433imp 123 . . . . . . . . . . . . . . . . 17 ((((𝑥P𝑦P𝑧P) ∧ 𝑟 ∈ (2nd𝑥)) ∧ 𝑟 ∈ (1st𝑧)) → ∃𝑟(𝑟Q ∧ (𝑟 ∈ (2nd𝑥) ∧ 𝑟 ∈ (1st𝑧))))
35 df-rex 2423 . . . . . . . . . . . . . . . . 17 (∃𝑟Q (𝑟 ∈ (2nd𝑥) ∧ 𝑟 ∈ (1st𝑧)) ↔ ∃𝑟(𝑟Q ∧ (𝑟 ∈ (2nd𝑥) ∧ 𝑟 ∈ (1st𝑧))))
3634, 35sylibr 133 . . . . . . . . . . . . . . . 16 ((((𝑥P𝑦P𝑧P) ∧ 𝑟 ∈ (2nd𝑥)) ∧ 𝑟 ∈ (1st𝑧)) → ∃𝑟Q (𝑟 ∈ (2nd𝑥) ∧ 𝑟 ∈ (1st𝑧)))
37 ltdfpr 7365 . . . . . . . . . . . . . . . . . . 19 ((𝑥P𝑧P) → (𝑥<P 𝑧 ↔ ∃𝑟Q (𝑟 ∈ (2nd𝑥) ∧ 𝑟 ∈ (1st𝑧))))
3837biimprd 157 . . . . . . . . . . . . . . . . . 18 ((𝑥P𝑧P) → (∃𝑟Q (𝑟 ∈ (2nd𝑥) ∧ 𝑟 ∈ (1st𝑧)) → 𝑥<P 𝑧))
39383adant2 1001 . . . . . . . . . . . . . . . . 17 ((𝑥P𝑦P𝑧P) → (∃𝑟Q (𝑟 ∈ (2nd𝑥) ∧ 𝑟 ∈ (1st𝑧)) → 𝑥<P 𝑧))
4039ad2antrr 480 . . . . . . . . . . . . . . . 16 ((((𝑥P𝑦P𝑧P) ∧ 𝑟 ∈ (2nd𝑥)) ∧ 𝑟 ∈ (1st𝑧)) → (∃𝑟Q (𝑟 ∈ (2nd𝑥) ∧ 𝑟 ∈ (1st𝑧)) → 𝑥<P 𝑧))
4136, 40mpd 13 . . . . . . . . . . . . . . 15 ((((𝑥P𝑦P𝑧P) ∧ 𝑟 ∈ (2nd𝑥)) ∧ 𝑟 ∈ (1st𝑧)) → 𝑥<P 𝑧)
4241ex 114 . . . . . . . . . . . . . 14 (((𝑥P𝑦P𝑧P) ∧ 𝑟 ∈ (2nd𝑥)) → (𝑟 ∈ (1st𝑧) → 𝑥<P 𝑧))
4342adantrr 471 . . . . . . . . . . . . 13 (((𝑥P𝑦P𝑧P) ∧ (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (1st𝑦))) → (𝑟 ∈ (1st𝑧) → 𝑥<P 𝑧))
44 elprnql 7340 . . . . . . . . . . . . . . . . . . . . 21 ((⟨(1st𝑦), (2nd𝑦)⟩ ∈ P𝑠 ∈ (1st𝑦)) → 𝑠Q)
457, 44sylan 281 . . . . . . . . . . . . . . . . . . . 20 ((𝑦P𝑠 ∈ (1st𝑦)) → 𝑠Q)
46 pm3.21 262 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ (1st𝑦) → (𝑠 ∈ (2nd𝑧) → (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦))))
4746adantl 275 . . . . . . . . . . . . . . . . . . . 20 ((𝑦P𝑠 ∈ (1st𝑦)) → (𝑠 ∈ (2nd𝑧) → (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦))))
48 19.8a 1570 . . . . . . . . . . . . . . . . . . . 20 ((𝑠Q ∧ (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦))) → ∃𝑠(𝑠Q ∧ (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦))))
4945, 47, 48syl6an 1411 . . . . . . . . . . . . . . . . . . 19 ((𝑦P𝑠 ∈ (1st𝑦)) → (𝑠 ∈ (2nd𝑧) → ∃𝑠(𝑠Q ∧ (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦)))))
50493ad2antl2 1145 . . . . . . . . . . . . . . . . . 18 (((𝑥P𝑦P𝑧P) ∧ 𝑠 ∈ (1st𝑦)) → (𝑠 ∈ (2nd𝑧) → ∃𝑠(𝑠Q ∧ (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦)))))
5150imp 123 . . . . . . . . . . . . . . . . 17 ((((𝑥P𝑦P𝑧P) ∧ 𝑠 ∈ (1st𝑦)) ∧ 𝑠 ∈ (2nd𝑧)) → ∃𝑠(𝑠Q ∧ (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦))))
52 df-rex 2423 . . . . . . . . . . . . . . . . 17 (∃𝑠Q (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦)) ↔ ∃𝑠(𝑠Q ∧ (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦))))
5351, 52sylibr 133 . . . . . . . . . . . . . . . 16 ((((𝑥P𝑦P𝑧P) ∧ 𝑠 ∈ (1st𝑦)) ∧ 𝑠 ∈ (2nd𝑧)) → ∃𝑠Q (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦)))
54 ltdfpr 7365 . . . . . . . . . . . . . . . . . . . 20 ((𝑧P𝑦P) → (𝑧<P 𝑦 ↔ ∃𝑠Q (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦))))
5554biimprd 157 . . . . . . . . . . . . . . . . . . 19 ((𝑧P𝑦P) → (∃𝑠Q (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦)) → 𝑧<P 𝑦))
5655ancoms 266 . . . . . . . . . . . . . . . . . 18 ((𝑦P𝑧P) → (∃𝑠Q (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦)) → 𝑧<P 𝑦))
57563adant1 1000 . . . . . . . . . . . . . . . . 17 ((𝑥P𝑦P𝑧P) → (∃𝑠Q (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦)) → 𝑧<P 𝑦))
5857ad2antrr 480 . . . . . . . . . . . . . . . 16 ((((𝑥P𝑦P𝑧P) ∧ 𝑠 ∈ (1st𝑦)) ∧ 𝑠 ∈ (2nd𝑧)) → (∃𝑠Q (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦)) → 𝑧<P 𝑦))
5953, 58mpd 13 . . . . . . . . . . . . . . 15 ((((𝑥P𝑦P𝑧P) ∧ 𝑠 ∈ (1st𝑦)) ∧ 𝑠 ∈ (2nd𝑧)) → 𝑧<P 𝑦)
6059ex 114 . . . . . . . . . . . . . 14 (((𝑥P𝑦P𝑧P) ∧ 𝑠 ∈ (1st𝑦)) → (𝑠 ∈ (2nd𝑧) → 𝑧<P 𝑦))
6160adantrl 470 . . . . . . . . . . . . 13 (((𝑥P𝑦P𝑧P) ∧ (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (1st𝑦))) → (𝑠 ∈ (2nd𝑧) → 𝑧<P 𝑦))
6243, 61orim12d 776 . . . . . . . . . . . 12 (((𝑥P𝑦P𝑧P) ∧ (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (1st𝑦))) → ((𝑟 ∈ (1st𝑧) ∨ 𝑠 ∈ (2nd𝑧)) → (𝑥<P 𝑧𝑧<P 𝑦)))
6362adantlr 469 . . . . . . . . . . 11 ((((𝑥P𝑦P𝑧P) ∧ (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))) ∧ (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (1st𝑦))) → ((𝑟 ∈ (1st𝑧) ∨ 𝑠 ∈ (2nd𝑧)) → (𝑥<P 𝑧𝑧<P 𝑦)))
6463adantr 274 . . . . . . . . . 10 (((((𝑥P𝑦P𝑧P) ∧ (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))) ∧ (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (1st𝑦))) ∧ (𝑟 <Q 𝑞𝑞 <Q 𝑠)) → ((𝑟 ∈ (1st𝑧) ∨ 𝑠 ∈ (2nd𝑧)) → (𝑥<P 𝑧𝑧<P 𝑦)))
6526, 64mpd 13 . . . . . . . . 9 (((((𝑥P𝑦P𝑧P) ∧ (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))) ∧ (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (1st𝑦))) ∧ (𝑟 <Q 𝑞𝑞 <Q 𝑠)) → (𝑥<P 𝑧𝑧<P 𝑦))
6665ex 114 . . . . . . . 8 ((((𝑥P𝑦P𝑧P) ∧ (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))) ∧ (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (1st𝑦))) → ((𝑟 <Q 𝑞𝑞 <Q 𝑠) → (𝑥<P 𝑧𝑧<P 𝑦)))
6766rexlimdvva 2561 . . . . . . 7 (((𝑥P𝑦P𝑧P) ∧ (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))) → (∃𝑟 ∈ (2nd𝑥)∃𝑠 ∈ (1st𝑦)(𝑟 <Q 𝑞𝑞 <Q 𝑠) → (𝑥<P 𝑧𝑧<P 𝑦)))
6814, 67mpd 13 . . . . . 6 (((𝑥P𝑦P𝑧P) ∧ (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))) → (𝑥<P 𝑧𝑧<P 𝑦))
6968ex 114 . . . . 5 ((𝑥P𝑦P𝑧P) → ((𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦)) → (𝑥<P 𝑧𝑧<P 𝑦)))
7069rexlimdvw 2557 . . . 4 ((𝑥P𝑦P𝑧P) → (∃𝑞Q (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦)) → (𝑥<P 𝑧𝑧<P 𝑦)))
713, 70sylbid 149 . . 3 ((𝑥P𝑦P𝑧P) → (𝑥<P 𝑦 → (𝑥<P 𝑧𝑧<P 𝑦)))
7271rgen3 2523 . 2 𝑥P𝑦P𝑧P (𝑥<P 𝑦 → (𝑥<P 𝑧𝑧<P 𝑦))
73 df-iso 4229 . 2 (<P Or P ↔ (<P Po P ∧ ∀𝑥P𝑦P𝑧P (𝑥<P 𝑦 → (𝑥<P 𝑧𝑧<P 𝑦))))
741, 72, 73mpbir2an 927 1 <P Or P
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698   ∧ w3a 963  ∃wex 1469   ∈ wcel 1481  ∀wral 2417  ∃wrex 2418  ⟨cop 3536   class class class wbr 3938   Po wpo 4226   Or wor 4227  ‘cfv 5134  1st c1st 6047  2nd c2nd 6048  Qcnq 7139
 Copyright terms: Public domain W3C validator