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

Theorem ltsopr 7056
Description: Positive real 'less than' is a weak linear order (in the sense of df-iso 4087). 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 7055 . 2 <P Po P
2 ltdfpr 6966 . . . . 5 ((𝑥P𝑦P) → (𝑥<P 𝑦 ↔ ∃𝑞Q (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))))
323adant3 959 . . . 4 ((𝑥P𝑦P𝑧P) → (𝑥<P 𝑦 ↔ ∃𝑞Q (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))))
4 prop 6935 . . . . . . . . . . . 12 (𝑥P → ⟨(1st𝑥), (2nd𝑥)⟩ ∈ P)
5 prnminu 6949 . . . . . . . . . . . 12 ((⟨(1st𝑥), (2nd𝑥)⟩ ∈ P𝑞 ∈ (2nd𝑥)) → ∃𝑟 ∈ (2nd𝑥)𝑟 <Q 𝑞)
64, 5sylan 277 . . . . . . . . . . 11 ((𝑥P𝑞 ∈ (2nd𝑥)) → ∃𝑟 ∈ (2nd𝑥)𝑟 <Q 𝑞)
7 prop 6935 . . . . . . . . . . . 12 (𝑦P → ⟨(1st𝑦), (2nd𝑦)⟩ ∈ P)
8 prnmaxl 6948 . . . . . . . . . . . 12 ((⟨(1st𝑦), (2nd𝑦)⟩ ∈ P𝑞 ∈ (1st𝑦)) → ∃𝑠 ∈ (1st𝑦)𝑞 <Q 𝑠)
97, 8sylan 277 . . . . . . . . . . 11 ((𝑦P𝑞 ∈ (1st𝑦)) → ∃𝑠 ∈ (1st𝑦)𝑞 <Q 𝑠)
106, 9anim12i 331 . . . . . . . . . 10 (((𝑥P𝑞 ∈ (2nd𝑥)) ∧ (𝑦P𝑞 ∈ (1st𝑦))) → (∃𝑟 ∈ (2nd𝑥)𝑟 <Q 𝑞 ∧ ∃𝑠 ∈ (1st𝑦)𝑞 <Q 𝑠))
1110an4s 553 . . . . . . . . 9 (((𝑥P𝑦P) ∧ (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))) → (∃𝑟 ∈ (2nd𝑥)𝑟 <Q 𝑞 ∧ ∃𝑠 ∈ (1st𝑦)𝑞 <Q 𝑠))
12 reeanv 2529 . . . . . . . . 9 (∃𝑟 ∈ (2nd𝑥)∃𝑠 ∈ (1st𝑦)(𝑟 <Q 𝑞𝑞 <Q 𝑠) ↔ (∃𝑟 ∈ (2nd𝑥)𝑟 <Q 𝑞 ∧ ∃𝑠 ∈ (1st𝑦)𝑞 <Q 𝑠))
1311, 12sylibr 132 . . . . . . . 8 (((𝑥P𝑦P) ∧ (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))) → ∃𝑟 ∈ (2nd𝑥)∃𝑠 ∈ (1st𝑦)(𝑟 <Q 𝑞𝑞 <Q 𝑠))
14133adantl3 1097 . . . . . . 7 (((𝑥P𝑦P𝑧P) ∧ (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))) → ∃𝑟 ∈ (2nd𝑥)∃𝑠 ∈ (1st𝑦)(𝑟 <Q 𝑞𝑞 <Q 𝑠))
15 ltsonq 6858 . . . . . . . . . . . . 13 <Q Or Q
16 ltrelnq 6825 . . . . . . . . . . . . 13 <Q ⊆ (Q × Q)
1715, 16sotri 4780 . . . . . . . . . . . 12 ((𝑟 <Q 𝑞𝑞 <Q 𝑠) → 𝑟 <Q 𝑠)
1817adantl 271 . . . . . . . . . . 11 (((((𝑥P𝑦P𝑧P) ∧ (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))) ∧ (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (1st𝑦))) ∧ (𝑟 <Q 𝑞𝑞 <Q 𝑠)) → 𝑟 <Q 𝑠)
19 prop 6935 . . . . . . . . . . . . . . . 16 (𝑧P → ⟨(1st𝑧), (2nd𝑧)⟩ ∈ P)
20 prloc 6951 . . . . . . . . . . . . . . . 16 ((⟨(1st𝑧), (2nd𝑧)⟩ ∈ P𝑟 <Q 𝑠) → (𝑟 ∈ (1st𝑧) ∨ 𝑠 ∈ (2nd𝑧)))
2119, 20sylan 277 . . . . . . . . . . . . . . 15 ((𝑧P𝑟 <Q 𝑠) → (𝑟 ∈ (1st𝑧) ∨ 𝑠 ∈ (2nd𝑧)))
22213ad2antl3 1103 . . . . . . . . . . . . . 14 (((𝑥P𝑦P𝑧P) ∧ 𝑟 <Q 𝑠) → (𝑟 ∈ (1st𝑧) ∨ 𝑠 ∈ (2nd𝑧)))
2322ex 113 . . . . . . . . . . . . 13 ((𝑥P𝑦P𝑧P) → (𝑟 <Q 𝑠 → (𝑟 ∈ (1st𝑧) ∨ 𝑠 ∈ (2nd𝑧))))
2423adantr 270 . . . . . . . . . . . 12 (((𝑥P𝑦P𝑧P) ∧ (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))) → (𝑟 <Q 𝑠 → (𝑟 ∈ (1st𝑧) ∨ 𝑠 ∈ (2nd𝑧))))
2524ad2antrr 472 . . . . . . . . . . 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 6942 . . . . . . . . . . . . . . . . . . . . 21 ((⟨(1st𝑥), (2nd𝑥)⟩ ∈ P𝑟 ∈ (2nd𝑥)) → 𝑟Q)
284, 27sylan 277 . . . . . . . . . . . . . . . . . . . 20 ((𝑥P𝑟 ∈ (2nd𝑥)) → 𝑟Q)
29 ax-ia3 106 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 ∈ (2nd𝑥) → (𝑟 ∈ (1st𝑧) → (𝑟 ∈ (2nd𝑥) ∧ 𝑟 ∈ (1st𝑧))))
3029adantl 271 . . . . . . . . . . . . . . . . . . . 20 ((𝑥P𝑟 ∈ (2nd𝑥)) → (𝑟 ∈ (1st𝑧) → (𝑟 ∈ (2nd𝑥) ∧ 𝑟 ∈ (1st𝑧))))
31 19.8a 1523 . . . . . . . . . . . . . . . . . . . 20 ((𝑟Q ∧ (𝑟 ∈ (2nd𝑥) ∧ 𝑟 ∈ (1st𝑧))) → ∃𝑟(𝑟Q ∧ (𝑟 ∈ (2nd𝑥) ∧ 𝑟 ∈ (1st𝑧))))
3228, 30, 31syl6an 1364 . . . . . . . . . . . . . . . . . . 19 ((𝑥P𝑟 ∈ (2nd𝑥)) → (𝑟 ∈ (1st𝑧) → ∃𝑟(𝑟Q ∧ (𝑟 ∈ (2nd𝑥) ∧ 𝑟 ∈ (1st𝑧)))))
33323ad2antl1 1101 . . . . . . . . . . . . . . . . . 18 (((𝑥P𝑦P𝑧P) ∧ 𝑟 ∈ (2nd𝑥)) → (𝑟 ∈ (1st𝑧) → ∃𝑟(𝑟Q ∧ (𝑟 ∈ (2nd𝑥) ∧ 𝑟 ∈ (1st𝑧)))))
3433imp 122 . . . . . . . . . . . . . . . . 17 ((((𝑥P𝑦P𝑧P) ∧ 𝑟 ∈ (2nd𝑥)) ∧ 𝑟 ∈ (1st𝑧)) → ∃𝑟(𝑟Q ∧ (𝑟 ∈ (2nd𝑥) ∧ 𝑟 ∈ (1st𝑧))))
35 df-rex 2359 . . . . . . . . . . . . . . . . 17 (∃𝑟Q (𝑟 ∈ (2nd𝑥) ∧ 𝑟 ∈ (1st𝑧)) ↔ ∃𝑟(𝑟Q ∧ (𝑟 ∈ (2nd𝑥) ∧ 𝑟 ∈ (1st𝑧))))
3634, 35sylibr 132 . . . . . . . . . . . . . . . 16 ((((𝑥P𝑦P𝑧P) ∧ 𝑟 ∈ (2nd𝑥)) ∧ 𝑟 ∈ (1st𝑧)) → ∃𝑟Q (𝑟 ∈ (2nd𝑥) ∧ 𝑟 ∈ (1st𝑧)))
37 ltdfpr 6966 . . . . . . . . . . . . . . . . . . 19 ((𝑥P𝑧P) → (𝑥<P 𝑧 ↔ ∃𝑟Q (𝑟 ∈ (2nd𝑥) ∧ 𝑟 ∈ (1st𝑧))))
3837biimprd 156 . . . . . . . . . . . . . . . . . 18 ((𝑥P𝑧P) → (∃𝑟Q (𝑟 ∈ (2nd𝑥) ∧ 𝑟 ∈ (1st𝑧)) → 𝑥<P 𝑧))
39383adant2 958 . . . . . . . . . . . . . . . . 17 ((𝑥P𝑦P𝑧P) → (∃𝑟Q (𝑟 ∈ (2nd𝑥) ∧ 𝑟 ∈ (1st𝑧)) → 𝑥<P 𝑧))
4039ad2antrr 472 . . . . . . . . . . . . . . . 16 ((((𝑥P𝑦P𝑧P) ∧ 𝑟 ∈ (2nd𝑥)) ∧ 𝑟 ∈ (1st𝑧)) → (∃𝑟Q (𝑟 ∈ (2nd𝑥) ∧ 𝑟 ∈ (1st𝑧)) → 𝑥<P 𝑧))
4136, 40mpd 13 . . . . . . . . . . . . . . 15 ((((𝑥P𝑦P𝑧P) ∧ 𝑟 ∈ (2nd𝑥)) ∧ 𝑟 ∈ (1st𝑧)) → 𝑥<P 𝑧)
4241ex 113 . . . . . . . . . . . . . 14 (((𝑥P𝑦P𝑧P) ∧ 𝑟 ∈ (2nd𝑥)) → (𝑟 ∈ (1st𝑧) → 𝑥<P 𝑧))
4342adantrr 463 . . . . . . . . . . . . 13 (((𝑥P𝑦P𝑧P) ∧ (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (1st𝑦))) → (𝑟 ∈ (1st𝑧) → 𝑥<P 𝑧))
44 elprnql 6941 . . . . . . . . . . . . . . . . . . . . 21 ((⟨(1st𝑦), (2nd𝑦)⟩ ∈ P𝑠 ∈ (1st𝑦)) → 𝑠Q)
457, 44sylan 277 . . . . . . . . . . . . . . . . . . . 20 ((𝑦P𝑠 ∈ (1st𝑦)) → 𝑠Q)
46 pm3.21 260 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ (1st𝑦) → (𝑠 ∈ (2nd𝑧) → (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦))))
4746adantl 271 . . . . . . . . . . . . . . . . . . . 20 ((𝑦P𝑠 ∈ (1st𝑦)) → (𝑠 ∈ (2nd𝑧) → (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦))))
48 19.8a 1523 . . . . . . . . . . . . . . . . . . . 20 ((𝑠Q ∧ (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦))) → ∃𝑠(𝑠Q ∧ (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦))))
4945, 47, 48syl6an 1364 . . . . . . . . . . . . . . . . . . 19 ((𝑦P𝑠 ∈ (1st𝑦)) → (𝑠 ∈ (2nd𝑧) → ∃𝑠(𝑠Q ∧ (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦)))))
50493ad2antl2 1102 . . . . . . . . . . . . . . . . . 18 (((𝑥P𝑦P𝑧P) ∧ 𝑠 ∈ (1st𝑦)) → (𝑠 ∈ (2nd𝑧) → ∃𝑠(𝑠Q ∧ (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦)))))
5150imp 122 . . . . . . . . . . . . . . . . 17 ((((𝑥P𝑦P𝑧P) ∧ 𝑠 ∈ (1st𝑦)) ∧ 𝑠 ∈ (2nd𝑧)) → ∃𝑠(𝑠Q ∧ (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦))))
52 df-rex 2359 . . . . . . . . . . . . . . . . 17 (∃𝑠Q (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦)) ↔ ∃𝑠(𝑠Q ∧ (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦))))
5351, 52sylibr 132 . . . . . . . . . . . . . . . 16 ((((𝑥P𝑦P𝑧P) ∧ 𝑠 ∈ (1st𝑦)) ∧ 𝑠 ∈ (2nd𝑧)) → ∃𝑠Q (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦)))
54 ltdfpr 6966 . . . . . . . . . . . . . . . . . . . 20 ((𝑧P𝑦P) → (𝑧<P 𝑦 ↔ ∃𝑠Q (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦))))
5554biimprd 156 . . . . . . . . . . . . . . . . . . 19 ((𝑧P𝑦P) → (∃𝑠Q (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦)) → 𝑧<P 𝑦))
5655ancoms 264 . . . . . . . . . . . . . . . . . 18 ((𝑦P𝑧P) → (∃𝑠Q (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦)) → 𝑧<P 𝑦))
57563adant1 957 . . . . . . . . . . . . . . . . 17 ((𝑥P𝑦P𝑧P) → (∃𝑠Q (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦)) → 𝑧<P 𝑦))
5857ad2antrr 472 . . . . . . . . . . . . . . . 16 ((((𝑥P𝑦P𝑧P) ∧ 𝑠 ∈ (1st𝑦)) ∧ 𝑠 ∈ (2nd𝑧)) → (∃𝑠Q (𝑠 ∈ (2nd𝑧) ∧ 𝑠 ∈ (1st𝑦)) → 𝑧<P 𝑦))
5953, 58mpd 13 . . . . . . . . . . . . . . 15 ((((𝑥P𝑦P𝑧P) ∧ 𝑠 ∈ (1st𝑦)) ∧ 𝑠 ∈ (2nd𝑧)) → 𝑧<P 𝑦)
6059ex 113 . . . . . . . . . . . . . 14 (((𝑥P𝑦P𝑧P) ∧ 𝑠 ∈ (1st𝑦)) → (𝑠 ∈ (2nd𝑧) → 𝑧<P 𝑦))
6160adantrl 462 . . . . . . . . . . . . 13 (((𝑥P𝑦P𝑧P) ∧ (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (1st𝑦))) → (𝑠 ∈ (2nd𝑧) → 𝑧<P 𝑦))
6243, 61orim12d 733 . . . . . . . . . . . 12 (((𝑥P𝑦P𝑧P) ∧ (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (1st𝑦))) → ((𝑟 ∈ (1st𝑧) ∨ 𝑠 ∈ (2nd𝑧)) → (𝑥<P 𝑧𝑧<P 𝑦)))
6362adantlr 461 . . . . . . . . . . 11 ((((𝑥P𝑦P𝑧P) ∧ (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))) ∧ (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (1st𝑦))) → ((𝑟 ∈ (1st𝑧) ∨ 𝑠 ∈ (2nd𝑧)) → (𝑥<P 𝑧𝑧<P 𝑦)))
6463adantr 270 . . . . . . . . . 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 113 . . . . . . . 8 ((((𝑥P𝑦P𝑧P) ∧ (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))) ∧ (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (1st𝑦))) → ((𝑟 <Q 𝑞𝑞 <Q 𝑠) → (𝑥<P 𝑧𝑧<P 𝑦)))
6766rexlimdvva 2490 . . . . . . 7 (((𝑥P𝑦P𝑧P) ∧ (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))) → (∃𝑟 ∈ (2nd𝑥)∃𝑠 ∈ (1st𝑦)(𝑟 <Q 𝑞𝑞 <Q 𝑠) → (𝑥<P 𝑧𝑧<P 𝑦)))
6814, 67mpd 13 . . . . . 6 (((𝑥P𝑦P𝑧P) ∧ (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))) → (𝑥<P 𝑧𝑧<P 𝑦))
6968ex 113 . . . . 5 ((𝑥P𝑦P𝑧P) → ((𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦)) → (𝑥<P 𝑧𝑧<P 𝑦)))
7069rexlimdvw 2486 . . . 4 ((𝑥P𝑦P𝑧P) → (∃𝑞Q (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦)) → (𝑥<P 𝑧𝑧<P 𝑦)))
713, 70sylbid 148 . . 3 ((𝑥P𝑦P𝑧P) → (𝑥<P 𝑦 → (𝑥<P 𝑧𝑧<P 𝑦)))
7271rgen3 2454 . 2 𝑥P𝑦P𝑧P (𝑥<P 𝑦 → (𝑥<P 𝑧𝑧<P 𝑦))
73 df-iso 4087 . 2 (<P Or P ↔ (<P Po P ∧ ∀𝑥P𝑦P𝑧P (𝑥<P 𝑦 → (𝑥<P 𝑧𝑧<P 𝑦))))
741, 72, 73mpbir2an 884 1 <P Or P
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  wo 662  w3a 920  wex 1422  wcel 1434  wral 2353  wrex 2354  cop 3425   class class class wbr 3811   Po wpo 4084   Or wor 4085  cfv 4967  1st c1st 5842  2nd c2nd 5843  Qcnq 6740   <Q cltq 6745  Pcnp 6751  <P cltp 6755
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-coll 3919  ax-sep 3922  ax-nul 3930  ax-pow 3974  ax-pr 3999  ax-un 4223  ax-setind 4315  ax-iinf 4365
This theorem depends on definitions:  df-bi 115  df-dc 777  df-3or 921  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-ral 2358  df-rex 2359  df-reu 2360  df-rab 2362  df-v 2614  df-sbc 2827  df-csb 2920  df-dif 2986  df-un 2988  df-in 2990  df-ss 2997  df-nul 3270  df-pw 3408  df-sn 3428  df-pr 3429  df-op 3431  df-uni 3628  df-int 3663  df-iun 3706  df-br 3812  df-opab 3866  df-mpt 3867  df-tr 3902  df-eprel 4079  df-id 4083  df-po 4086  df-iso 4087  df-iord 4156  df-on 4158  df-suc 4161  df-iom 4368  df-xp 4405  df-rel 4406  df-cnv 4407  df-co 4408  df-dm 4409  df-rn 4410  df-res 4411  df-ima 4412  df-iota 4932  df-fun 4969  df-fn 4970  df-f 4971  df-f1 4972  df-fo 4973  df-f1o 4974  df-fv 4975  df-ov 5592  df-oprab 5593  df-mpt2 5594  df-1st 5844  df-2nd 5845  df-recs 6000  df-irdg 6065  df-oadd 6115  df-omul 6116  df-er 6220  df-ec 6222  df-qs 6226  df-ni 6764  df-mi 6766  df-lti 6767  df-enq 6807  df-nqqs 6808  df-ltnqqs 6813  df-inp 6926  df-iltp 6930
This theorem is referenced by:  prplnqu  7080  addextpr  7081  caucvgprprlemk  7143  caucvgprprlemnkltj  7149  caucvgprprlemnkeqj  7150  caucvgprprlemnjltk  7151  caucvgprprlemnbj  7153  caucvgprprlemml  7154  caucvgprprlemlol  7158  caucvgprprlemupu  7160  caucvgprprlemloc  7163  caucvgprprlemaddq  7168  lttrsr  7209  ltposr  7210  ltsosr  7211  archsr  7228
  Copyright terms: Public domain W3C validator