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

Theorem ltsopr 6570
 Description: Positive real 'less than' is a weak linear order (in the sense of df-iso 4025). 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 𝑟 𝑞 𝑠 x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ltpopr 6569 . 2 <P Po P
2 ltdfpr 6489 . . . . 5 ((x P y P) → (x<P y𝑞 Q (𝑞 (2ndx) 𝑞 (1sty))))
323adant3 923 . . . 4 ((x P y P z P) → (x<P y𝑞 Q (𝑞 (2ndx) 𝑞 (1sty))))
4 prop 6458 . . . . . . . . . . . 12 (x P → ⟨(1stx), (2ndx)⟩ P)
5 prnminu 6472 . . . . . . . . . . . 12 ((⟨(1stx), (2ndx)⟩ P 𝑞 (2ndx)) → 𝑟 (2ndx)𝑟 <Q 𝑞)
64, 5sylan 267 . . . . . . . . . . 11 ((x P 𝑞 (2ndx)) → 𝑟 (2ndx)𝑟 <Q 𝑞)
7 prop 6458 . . . . . . . . . . . 12 (y P → ⟨(1sty), (2ndy)⟩ P)
8 prnmaxl 6471 . . . . . . . . . . . 12 ((⟨(1sty), (2ndy)⟩ P 𝑞 (1sty)) → 𝑠 (1sty)𝑞 <Q 𝑠)
97, 8sylan 267 . . . . . . . . . . 11 ((y P 𝑞 (1sty)) → 𝑠 (1sty)𝑞 <Q 𝑠)
106, 9anim12i 321 . . . . . . . . . 10 (((x P 𝑞 (2ndx)) (y P 𝑞 (1sty))) → (𝑟 (2ndx)𝑟 <Q 𝑞 𝑠 (1sty)𝑞 <Q 𝑠))
1110an4s 522 . . . . . . . . 9 (((x P y P) (𝑞 (2ndx) 𝑞 (1sty))) → (𝑟 (2ndx)𝑟 <Q 𝑞 𝑠 (1sty)𝑞 <Q 𝑠))
12 reeanv 2473 . . . . . . . . 9 (𝑟 (2ndx)𝑠 (1sty)(𝑟 <Q 𝑞 𝑞 <Q 𝑠) ↔ (𝑟 (2ndx)𝑟 <Q 𝑞 𝑠 (1sty)𝑞 <Q 𝑠))
1311, 12sylibr 137 . . . . . . . 8 (((x P y P) (𝑞 (2ndx) 𝑞 (1sty))) → 𝑟 (2ndx)𝑠 (1sty)(𝑟 <Q 𝑞 𝑞 <Q 𝑠))
14133adantl3 1061 . . . . . . 7 (((x P y P z P) (𝑞 (2ndx) 𝑞 (1sty))) → 𝑟 (2ndx)𝑠 (1sty)(𝑟 <Q 𝑞 𝑞 <Q 𝑠))
15 ltsonq 6382 . . . . . . . . . . . . 13 <Q Or Q
16 ltrelnq 6349 . . . . . . . . . . . . 13 <Q ⊆ (Q × Q)
1715, 16sotri 4663 . . . . . . . . . . . 12 ((𝑟 <Q 𝑞 𝑞 <Q 𝑠) → 𝑟 <Q 𝑠)
1817adantl 262 . . . . . . . . . . 11 (((((x P y P z P) (𝑞 (2ndx) 𝑞 (1sty))) (𝑟 (2ndx) 𝑠 (1sty))) (𝑟 <Q 𝑞 𝑞 <Q 𝑠)) → 𝑟 <Q 𝑠)
19 prop 6458 . . . . . . . . . . . . . . . 16 (z P → ⟨(1stz), (2ndz)⟩ P)
20 prloc 6474 . . . . . . . . . . . . . . . 16 ((⟨(1stz), (2ndz)⟩ P 𝑟 <Q 𝑠) → (𝑟 (1stz) 𝑠 (2ndz)))
2119, 20sylan 267 . . . . . . . . . . . . . . 15 ((z P 𝑟 <Q 𝑠) → (𝑟 (1stz) 𝑠 (2ndz)))
22213ad2antl3 1067 . . . . . . . . . . . . . 14 (((x P y P z P) 𝑟 <Q 𝑠) → (𝑟 (1stz) 𝑠 (2ndz)))
2322ex 108 . . . . . . . . . . . . 13 ((x P y P z P) → (𝑟 <Q 𝑠 → (𝑟 (1stz) 𝑠 (2ndz))))
2423adantr 261 . . . . . . . . . . . 12 (((x P y P z P) (𝑞 (2ndx) 𝑞 (1sty))) → (𝑟 <Q 𝑠 → (𝑟 (1stz) 𝑠 (2ndz))))
2524ad2antrr 457 . . . . . . . . . . 11 (((((x P y P z P) (𝑞 (2ndx) 𝑞 (1sty))) (𝑟 (2ndx) 𝑠 (1sty))) (𝑟 <Q 𝑞 𝑞 <Q 𝑠)) → (𝑟 <Q 𝑠 → (𝑟 (1stz) 𝑠 (2ndz))))
2618, 25mpd 13 . . . . . . . . . 10 (((((x P y P z P) (𝑞 (2ndx) 𝑞 (1sty))) (𝑟 (2ndx) 𝑠 (1sty))) (𝑟 <Q 𝑞 𝑞 <Q 𝑠)) → (𝑟 (1stz) 𝑠 (2ndz)))
27 elprnqu 6465 . . . . . . . . . . . . . . . . . . . . 21 ((⟨(1stx), (2ndx)⟩ P 𝑟 (2ndx)) → 𝑟 Q)
284, 27sylan 267 . . . . . . . . . . . . . . . . . . . 20 ((x P 𝑟 (2ndx)) → 𝑟 Q)
29 ax-ia3 101 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 (2ndx) → (𝑟 (1stz) → (𝑟 (2ndx) 𝑟 (1stz))))
3029adantl 262 . . . . . . . . . . . . . . . . . . . 20 ((x P 𝑟 (2ndx)) → (𝑟 (1stz) → (𝑟 (2ndx) 𝑟 (1stz))))
31 19.8a 1479 . . . . . . . . . . . . . . . . . . . 20 ((𝑟 Q (𝑟 (2ndx) 𝑟 (1stz))) → 𝑟(𝑟 Q (𝑟 (2ndx) 𝑟 (1stz))))
3228, 30, 31syl6an 1320 . . . . . . . . . . . . . . . . . . 19 ((x P 𝑟 (2ndx)) → (𝑟 (1stz) → 𝑟(𝑟 Q (𝑟 (2ndx) 𝑟 (1stz)))))
33323ad2antl1 1065 . . . . . . . . . . . . . . . . . 18 (((x P y P z P) 𝑟 (2ndx)) → (𝑟 (1stz) → 𝑟(𝑟 Q (𝑟 (2ndx) 𝑟 (1stz)))))
3433imp 115 . . . . . . . . . . . . . . . . 17 ((((x P y P z P) 𝑟 (2ndx)) 𝑟 (1stz)) → 𝑟(𝑟 Q (𝑟 (2ndx) 𝑟 (1stz))))
35 df-rex 2306 . . . . . . . . . . . . . . . . 17 (𝑟 Q (𝑟 (2ndx) 𝑟 (1stz)) ↔ 𝑟(𝑟 Q (𝑟 (2ndx) 𝑟 (1stz))))
3634, 35sylibr 137 . . . . . . . . . . . . . . . 16 ((((x P y P z P) 𝑟 (2ndx)) 𝑟 (1stz)) → 𝑟 Q (𝑟 (2ndx) 𝑟 (1stz)))
37 ltdfpr 6489 . . . . . . . . . . . . . . . . . . 19 ((x P z P) → (x<P z𝑟 Q (𝑟 (2ndx) 𝑟 (1stz))))
3837biimprd 147 . . . . . . . . . . . . . . . . . 18 ((x P z P) → (𝑟 Q (𝑟 (2ndx) 𝑟 (1stz)) → x<P z))
39383adant2 922 . . . . . . . . . . . . . . . . 17 ((x P y P z P) → (𝑟 Q (𝑟 (2ndx) 𝑟 (1stz)) → x<P z))
4039ad2antrr 457 . . . . . . . . . . . . . . . 16 ((((x P y P z P) 𝑟 (2ndx)) 𝑟 (1stz)) → (𝑟 Q (𝑟 (2ndx) 𝑟 (1stz)) → x<P z))
4136, 40mpd 13 . . . . . . . . . . . . . . 15 ((((x P y P z P) 𝑟 (2ndx)) 𝑟 (1stz)) → x<P z)
4241ex 108 . . . . . . . . . . . . . 14 (((x P y P z P) 𝑟 (2ndx)) → (𝑟 (1stz) → x<P z))
4342adantrr 448 . . . . . . . . . . . . 13 (((x P y P z P) (𝑟 (2ndx) 𝑠 (1sty))) → (𝑟 (1stz) → x<P z))
44 elprnql 6464 . . . . . . . . . . . . . . . . . . . . 21 ((⟨(1sty), (2ndy)⟩ P 𝑠 (1sty)) → 𝑠 Q)
457, 44sylan 267 . . . . . . . . . . . . . . . . . . . 20 ((y P 𝑠 (1sty)) → 𝑠 Q)
46 pm3.21 251 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 (1sty) → (𝑠 (2ndz) → (𝑠 (2ndz) 𝑠 (1sty))))
4746adantl 262 . . . . . . . . . . . . . . . . . . . 20 ((y P 𝑠 (1sty)) → (𝑠 (2ndz) → (𝑠 (2ndz) 𝑠 (1sty))))
48 19.8a 1479 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 Q (𝑠 (2ndz) 𝑠 (1sty))) → 𝑠(𝑠 Q (𝑠 (2ndz) 𝑠 (1sty))))
4945, 47, 48syl6an 1320 . . . . . . . . . . . . . . . . . . 19 ((y P 𝑠 (1sty)) → (𝑠 (2ndz) → 𝑠(𝑠 Q (𝑠 (2ndz) 𝑠 (1sty)))))
50493ad2antl2 1066 . . . . . . . . . . . . . . . . . 18 (((x P y P z P) 𝑠 (1sty)) → (𝑠 (2ndz) → 𝑠(𝑠 Q (𝑠 (2ndz) 𝑠 (1sty)))))
5150imp 115 . . . . . . . . . . . . . . . . 17 ((((x P y P z P) 𝑠 (1sty)) 𝑠 (2ndz)) → 𝑠(𝑠 Q (𝑠 (2ndz) 𝑠 (1sty))))
52 df-rex 2306 . . . . . . . . . . . . . . . . 17 (𝑠 Q (𝑠 (2ndz) 𝑠 (1sty)) ↔ 𝑠(𝑠 Q (𝑠 (2ndz) 𝑠 (1sty))))
5351, 52sylibr 137 . . . . . . . . . . . . . . . 16 ((((x P y P z P) 𝑠 (1sty)) 𝑠 (2ndz)) → 𝑠 Q (𝑠 (2ndz) 𝑠 (1sty)))
54 ltdfpr 6489 . . . . . . . . . . . . . . . . . . . 20 ((z P y P) → (z<P y𝑠 Q (𝑠 (2ndz) 𝑠 (1sty))))
5554biimprd 147 . . . . . . . . . . . . . . . . . . 19 ((z P y P) → (𝑠 Q (𝑠 (2ndz) 𝑠 (1sty)) → z<P y))
5655ancoms 255 . . . . . . . . . . . . . . . . . 18 ((y P z P) → (𝑠 Q (𝑠 (2ndz) 𝑠 (1sty)) → z<P y))
57563adant1 921 . . . . . . . . . . . . . . . . 17 ((x P y P z P) → (𝑠 Q (𝑠 (2ndz) 𝑠 (1sty)) → z<P y))
5857ad2antrr 457 . . . . . . . . . . . . . . . 16 ((((x P y P z P) 𝑠 (1sty)) 𝑠 (2ndz)) → (𝑠 Q (𝑠 (2ndz) 𝑠 (1sty)) → z<P y))
5953, 58mpd 13 . . . . . . . . . . . . . . 15 ((((x P y P z P) 𝑠 (1sty)) 𝑠 (2ndz)) → z<P y)
6059ex 108 . . . . . . . . . . . . . 14 (((x P y P z P) 𝑠 (1sty)) → (𝑠 (2ndz) → z<P y))
6160adantrl 447 . . . . . . . . . . . . 13 (((x P y P z P) (𝑟 (2ndx) 𝑠 (1sty))) → (𝑠 (2ndz) → z<P y))
6243, 61orim12d 699 . . . . . . . . . . . 12 (((x P y P z P) (𝑟 (2ndx) 𝑠 (1sty))) → ((𝑟 (1stz) 𝑠 (2ndz)) → (x<P z z<P y)))
6362adantlr 446 . . . . . . . . . . 11 ((((x P y P z P) (𝑞 (2ndx) 𝑞 (1sty))) (𝑟 (2ndx) 𝑠 (1sty))) → ((𝑟 (1stz) 𝑠 (2ndz)) → (x<P z z<P y)))
6463adantr 261 . . . . . . . . . 10 (((((x P y P z P) (𝑞 (2ndx) 𝑞 (1sty))) (𝑟 (2ndx) 𝑠 (1sty))) (𝑟 <Q 𝑞 𝑞 <Q 𝑠)) → ((𝑟 (1stz) 𝑠 (2ndz)) → (x<P z z<P y)))
6526, 64mpd 13 . . . . . . . . 9 (((((x P y P z P) (𝑞 (2ndx) 𝑞 (1sty))) (𝑟 (2ndx) 𝑠 (1sty))) (𝑟 <Q 𝑞 𝑞 <Q 𝑠)) → (x<P z z<P y))
6665ex 108 . . . . . . . 8 ((((x P y P z P) (𝑞 (2ndx) 𝑞 (1sty))) (𝑟 (2ndx) 𝑠 (1sty))) → ((𝑟 <Q 𝑞 𝑞 <Q 𝑠) → (x<P z z<P y)))
6766rexlimdvva 2434 . . . . . . 7 (((x P y P z P) (𝑞 (2ndx) 𝑞 (1sty))) → (𝑟 (2ndx)𝑠 (1sty)(𝑟 <Q 𝑞 𝑞 <Q 𝑠) → (x<P z z<P y)))
6814, 67mpd 13 . . . . . 6 (((x P y P z P) (𝑞 (2ndx) 𝑞 (1sty))) → (x<P z z<P y))
6968ex 108 . . . . 5 ((x P y P z P) → ((𝑞 (2ndx) 𝑞 (1sty)) → (x<P z z<P y)))
7069rexlimdvw 2430 . . . 4 ((x P y P z P) → (𝑞 Q (𝑞 (2ndx) 𝑞 (1sty)) → (x<P z z<P y)))
713, 70sylbid 139 . . 3 ((x P y P z P) → (x<P y → (x<P z z<P y)))
7271rgen3 2400 . 2 x P y P z P (x<P y → (x<P z z<P y))
73 df-iso 4025 . 2 (<P Or P ↔ (<P Po P x P y P z P (x<P y → (x<P z z<P y))))
741, 72, 73mpbir2an 848 1 <P Or P
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 628   ∧ w3a 884  ∃wex 1378   ∈ wcel 1390  ∀wral 2300  ∃wrex 2301  ⟨cop 3370   class class class wbr 3755   Po wpo 4022   Or wor 4023  ‘cfv 4845  1st c1st 5707  2nd c2nd 5708  Qcnq 6264
 Copyright terms: Public domain W3C validator