MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cgracol Structured version   Visualization version   GIF version

Theorem cgracol 28850
Description: Angle congruence preserves colinearity. (Contributed by Thierry Arnoux, 9-Aug-2020.)
Hypotheses
Ref Expression
cgracol.p 𝑃 = (Base‘𝐺)
cgracol.i 𝐼 = (Itv‘𝐺)
cgracol.m = (dist‘𝐺)
cgracol.g (𝜑𝐺 ∈ TarskiG)
cgracol.a (𝜑𝐴𝑃)
cgracol.b (𝜑𝐵𝑃)
cgracol.c (𝜑𝐶𝑃)
cgracol.d (𝜑𝐷𝑃)
cgracol.e (𝜑𝐸𝑃)
cgracol.f (𝜑𝐹𝑃)
cgracol.1 (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
cgracol.l 𝐿 = (LineG‘𝐺)
cgracol.2 (𝜑 → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
Assertion
Ref Expression
cgracol (𝜑 → (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))

Proof of Theorem cgracol
StepHypRef Expression
1 cgracol.p . . . . . . . . . 10 𝑃 = (Base‘𝐺)
2 cgracol.i . . . . . . . . . 10 𝐼 = (Itv‘𝐺)
3 cgracol.m . . . . . . . . . 10 = (dist‘𝐺)
4 cgracol.g . . . . . . . . . . 11 (𝜑𝐺 ∈ TarskiG)
54adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐺 ∈ TarskiG)
6 cgracol.a . . . . . . . . . . 11 (𝜑𝐴𝑃)
76adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐴𝑃)
8 cgracol.b . . . . . . . . . . 11 (𝜑𝐵𝑃)
98adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐵𝑃)
10 cgracol.c . . . . . . . . . . 11 (𝜑𝐶𝑃)
1110adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐶𝑃)
12 cgracol.d . . . . . . . . . . 11 (𝜑𝐷𝑃)
1312adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐷𝑃)
14 cgracol.e . . . . . . . . . . 11 (𝜑𝐸𝑃)
1514adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐸𝑃)
16 cgracol.f . . . . . . . . . . 11 (𝜑𝐹𝑃)
1716adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐹𝑃)
18 cgracol.1 . . . . . . . . . . 11 (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
1918adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
20 eqid 2734 . . . . . . . . . 10 (hlG‘𝐺) = (hlG‘𝐺)
211, 2, 20, 4, 6, 8, 10, 12, 14, 16, 18cgrane2 28835 . . . . . . . . . . . . . . . 16 (𝜑𝐵𝐶)
2221necomd 2993 . . . . . . . . . . . . . . 15 (𝜑𝐶𝐵)
2322adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝐶 ∈ (𝐴𝐼𝐵)) → 𝐶𝐵)
241, 2, 20, 4, 6, 8, 10, 12, 14, 16, 18cgrane1 28834 . . . . . . . . . . . . . . 15 (𝜑𝐴𝐵)
2524adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝐶 ∈ (𝐴𝐼𝐵)) → 𝐴𝐵)
264adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝐶 ∈ (𝐴𝐼𝐵)) → 𝐺 ∈ TarskiG)
276adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝐶 ∈ (𝐴𝐼𝐵)) → 𝐴𝑃)
2810adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝐶 ∈ (𝐴𝐼𝐵)) → 𝐶𝑃)
298adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝐶 ∈ (𝐴𝐼𝐵)) → 𝐵𝑃)
30 simpr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝐶 ∈ (𝐴𝐼𝐵)) → 𝐶 ∈ (𝐴𝐼𝐵))
311, 3, 2, 26, 27, 28, 29, 30tgbtwncom 28510 . . . . . . . . . . . . . . 15 ((𝜑𝐶 ∈ (𝐴𝐼𝐵)) → 𝐶 ∈ (𝐵𝐼𝐴))
3231orcd 873 . . . . . . . . . . . . . 14 ((𝜑𝐶 ∈ (𝐴𝐼𝐵)) → (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶)))
3323, 25, 323jca 1127 . . . . . . . . . . . . 13 ((𝜑𝐶 ∈ (𝐴𝐼𝐵)) → (𝐶𝐵𝐴𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶))))
3422adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝐴 ∈ (𝐶𝐼𝐵)) → 𝐶𝐵)
3524adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝐴 ∈ (𝐶𝐼𝐵)) → 𝐴𝐵)
364adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝐴 ∈ (𝐶𝐼𝐵)) → 𝐺 ∈ TarskiG)
3710adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝐴 ∈ (𝐶𝐼𝐵)) → 𝐶𝑃)
386adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝐴 ∈ (𝐶𝐼𝐵)) → 𝐴𝑃)
398adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝐴 ∈ (𝐶𝐼𝐵)) → 𝐵𝑃)
40 simpr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝐴 ∈ (𝐶𝐼𝐵)) → 𝐴 ∈ (𝐶𝐼𝐵))
411, 3, 2, 36, 37, 38, 39, 40tgbtwncom 28510 . . . . . . . . . . . . . . 15 ((𝜑𝐴 ∈ (𝐶𝐼𝐵)) → 𝐴 ∈ (𝐵𝐼𝐶))
4241olcd 874 . . . . . . . . . . . . . 14 ((𝜑𝐴 ∈ (𝐶𝐼𝐵)) → (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶)))
4334, 35, 423jca 1127 . . . . . . . . . . . . 13 ((𝜑𝐴 ∈ (𝐶𝐼𝐵)) → (𝐶𝐵𝐴𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶))))
4433, 43jaodan 959 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐶𝐵𝐴𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶))))
451, 2, 20, 10, 6, 8, 4ishlg 28624 . . . . . . . . . . . . 13 (𝜑 → (𝐶((hlG‘𝐺)‘𝐵)𝐴 ↔ (𝐶𝐵𝐴𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶)))))
4645adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐶((hlG‘𝐺)‘𝐵)𝐴 ↔ (𝐶𝐵𝐴𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶)))))
4744, 46mpbird 257 . . . . . . . . . . 11 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐶((hlG‘𝐺)‘𝐵)𝐴)
481, 2, 20, 11, 7, 9, 5, 47hlcomd 28626 . . . . . . . . . 10 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐴((hlG‘𝐺)‘𝐵)𝐶)
491, 2, 3, 5, 7, 9, 11, 13, 15, 17, 19, 20, 48cgrahl 28849 . . . . . . . . 9 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐷((hlG‘𝐺)‘𝐸)𝐹)
501, 2, 20, 13, 17, 15, 5ishlg 28624 . . . . . . . . 9 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐷((hlG‘𝐺)‘𝐸)𝐹 ↔ (𝐷𝐸𝐹𝐸 ∧ (𝐷 ∈ (𝐸𝐼𝐹) ∨ 𝐹 ∈ (𝐸𝐼𝐷)))))
5149, 50mpbid 232 . . . . . . . 8 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐷𝐸𝐹𝐸 ∧ (𝐷 ∈ (𝐸𝐼𝐹) ∨ 𝐹 ∈ (𝐸𝐼𝐷))))
5251simp3d 1143 . . . . . . 7 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐷 ∈ (𝐸𝐼𝐹) ∨ 𝐹 ∈ (𝐸𝐼𝐷)))
534adantr 480 . . . . . . . . . 10 ((𝜑𝐷 ∈ (𝐸𝐼𝐹)) → 𝐺 ∈ TarskiG)
5414adantr 480 . . . . . . . . . 10 ((𝜑𝐷 ∈ (𝐸𝐼𝐹)) → 𝐸𝑃)
5512adantr 480 . . . . . . . . . 10 ((𝜑𝐷 ∈ (𝐸𝐼𝐹)) → 𝐷𝑃)
5616adantr 480 . . . . . . . . . 10 ((𝜑𝐷 ∈ (𝐸𝐼𝐹)) → 𝐹𝑃)
57 simpr 484 . . . . . . . . . 10 ((𝜑𝐷 ∈ (𝐸𝐼𝐹)) → 𝐷 ∈ (𝐸𝐼𝐹))
581, 3, 2, 53, 54, 55, 56, 57tgbtwncom 28510 . . . . . . . . 9 ((𝜑𝐷 ∈ (𝐸𝐼𝐹)) → 𝐷 ∈ (𝐹𝐼𝐸))
5958olcd 874 . . . . . . . 8 ((𝜑𝐷 ∈ (𝐸𝐼𝐹)) → (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸)))
604adantr 480 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝐸𝐼𝐷)) → 𝐺 ∈ TarskiG)
6114adantr 480 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝐸𝐼𝐷)) → 𝐸𝑃)
6216adantr 480 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝐸𝐼𝐷)) → 𝐹𝑃)
6312adantr 480 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝐸𝐼𝐷)) → 𝐷𝑃)
64 simpr 484 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝐸𝐼𝐷)) → 𝐹 ∈ (𝐸𝐼𝐷))
651, 3, 2, 60, 61, 62, 63, 64tgbtwncom 28510 . . . . . . . . 9 ((𝜑𝐹 ∈ (𝐸𝐼𝐷)) → 𝐹 ∈ (𝐷𝐼𝐸))
6665orcd 873 . . . . . . . 8 ((𝜑𝐹 ∈ (𝐸𝐼𝐷)) → (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸)))
6759, 66jaodan 959 . . . . . . 7 ((𝜑 ∧ (𝐷 ∈ (𝐸𝐼𝐹) ∨ 𝐹 ∈ (𝐸𝐼𝐷))) → (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸)))
6852, 67syldan 591 . . . . . 6 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸)))
6968orcd 873 . . . . 5 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → ((𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸)) ∨ 𝐸 ∈ (𝐷𝐼𝐹)))
70 df-3or 1087 . . . . 5 ((𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸) ∨ 𝐸 ∈ (𝐷𝐼𝐹)) ↔ ((𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸)) ∨ 𝐸 ∈ (𝐷𝐼𝐹)))
7169, 70sylibr 234 . . . 4 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸) ∨ 𝐸 ∈ (𝐷𝐼𝐹)))
72 cgracol.l . . . . . 6 𝐿 = (LineG‘𝐺)
731, 2, 4, 20, 6, 8, 10, 12, 14, 16, 18cgracom 28844 . . . . . . 7 (𝜑 → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝐴𝐵𝐶”⟩)
741, 2, 20, 4, 12, 14, 16, 6, 8, 10, 73cgrane1 28834 . . . . . 6 (𝜑𝐷𝐸)
751, 72, 2, 4, 12, 14, 74, 16tgellng 28575 . . . . 5 (𝜑 → (𝐹 ∈ (𝐷𝐿𝐸) ↔ (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸) ∨ 𝐸 ∈ (𝐷𝐼𝐹))))
7675adantr 480 . . . 4 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐹 ∈ (𝐷𝐿𝐸) ↔ (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸) ∨ 𝐸 ∈ (𝐷𝐼𝐹))))
7771, 76mpbird 257 . . 3 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐹 ∈ (𝐷𝐿𝐸))
7877orcd 873 . 2 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
794adantr 480 . . 3 ((𝜑𝐵 ∈ (𝐴𝐼𝐶)) → 𝐺 ∈ TarskiG)
8012adantr 480 . . 3 ((𝜑𝐵 ∈ (𝐴𝐼𝐶)) → 𝐷𝑃)
8114adantr 480 . . 3 ((𝜑𝐵 ∈ (𝐴𝐼𝐶)) → 𝐸𝑃)
8216adantr 480 . . 3 ((𝜑𝐵 ∈ (𝐴𝐼𝐶)) → 𝐹𝑃)
836adantr 480 . . . 4 ((𝜑𝐵 ∈ (𝐴𝐼𝐶)) → 𝐴𝑃)
848adantr 480 . . . 4 ((𝜑𝐵 ∈ (𝐴𝐼𝐶)) → 𝐵𝑃)
8510adantr 480 . . . 4 ((𝜑𝐵 ∈ (𝐴𝐼𝐶)) → 𝐶𝑃)
8618adantr 480 . . . 4 ((𝜑𝐵 ∈ (𝐴𝐼𝐶)) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
87 simpr 484 . . . 4 ((𝜑𝐵 ∈ (𝐴𝐼𝐶)) → 𝐵 ∈ (𝐴𝐼𝐶))
881, 2, 3, 79, 83, 84, 85, 80, 81, 82, 86, 87cgrabtwn 28848 . . 3 ((𝜑𝐵 ∈ (𝐴𝐼𝐶)) → 𝐸 ∈ (𝐷𝐼𝐹))
891, 72, 2, 79, 80, 81, 82, 88btwncolg3 28579 . 2 ((𝜑𝐵 ∈ (𝐴𝐼𝐶)) → (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
9024neneqd 2942 . . . . 5 (𝜑 → ¬ 𝐴 = 𝐵)
91 cgracol.2 . . . . . . 7 (𝜑 → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
9291orcomd 871 . . . . . 6 (𝜑 → (𝐴 = 𝐵𝐶 ∈ (𝐴𝐿𝐵)))
9392ord 864 . . . . 5 (𝜑 → (¬ 𝐴 = 𝐵𝐶 ∈ (𝐴𝐿𝐵)))
9490, 93mpd 15 . . . 4 (𝜑𝐶 ∈ (𝐴𝐿𝐵))
951, 72, 2, 4, 6, 8, 24, 10tgellng 28575 . . . 4 (𝜑 → (𝐶 ∈ (𝐴𝐿𝐵) ↔ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐴𝐼𝐶))))
9694, 95mpbid 232 . . 3 (𝜑 → (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐴𝐼𝐶)))
97 df-3or 1087 . . 3 ((𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐴𝐼𝐶)) ↔ ((𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵)) ∨ 𝐵 ∈ (𝐴𝐼𝐶)))
9896, 97sylib 218 . 2 (𝜑 → ((𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵)) ∨ 𝐵 ∈ (𝐴𝐼𝐶)))
9978, 89, 98mpjaodan 960 1 (𝜑 → (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  w3o 1085  w3a 1086   = wceq 1536  wcel 2105  wne 2937   class class class wbr 5147  cfv 6562  (class class class)co 7430  ⟨“cs3 14877  Basecbs 17244  distcds 17306  TarskiGcstrkg 28449  Itvcitv 28455  LineGclng 28456  hlGchlg 28622  cgrAccgra 28829
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-oadd 8508  df-er 8743  df-map 8866  df-pm 8867  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-dju 9938  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-2 12326  df-3 12327  df-n0 12524  df-xnn0 12597  df-z 12611  df-uz 12876  df-fz 13544  df-fzo 13691  df-hash 14366  df-word 14549  df-concat 14605  df-s1 14630  df-s2 14883  df-s3 14884  df-trkgc 28470  df-trkgb 28471  df-trkgcb 28472  df-trkg 28475  df-cgrg 28533  df-leg 28605  df-hlg 28623  df-cgra 28830
This theorem is referenced by:  cgrancol  28851  tgasa1  28880
  Copyright terms: Public domain W3C validator