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

Theorem cgracol 25713
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 481 . . . . . . . . . 10 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐺 ∈ TarskiG)
6 cgracol.a . . . . . . . . . . 11 (𝜑𝐴𝑃)
76adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐴𝑃)
8 cgracol.b . . . . . . . . . . 11 (𝜑𝐵𝑃)
98adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐵𝑃)
10 cgracol.c . . . . . . . . . . 11 (𝜑𝐶𝑃)
1110adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐶𝑃)
12 cgracol.d . . . . . . . . . . 11 (𝜑𝐷𝑃)
1312adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐷𝑃)
14 cgracol.e . . . . . . . . . . 11 (𝜑𝐸𝑃)
1514adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐸𝑃)
16 cgracol.f . . . . . . . . . . 11 (𝜑𝐹𝑃)
1716adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐹𝑃)
18 cgracol.1 . . . . . . . . . . 11 (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
1918adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
20 eqid 2621 . . . . . . . . . 10 (hlG‘𝐺) = (hlG‘𝐺)
211, 2, 20, 4, 6, 8, 10, 12, 14, 16, 18cgrane2 25699 . . . . . . . . . . . . . . . 16 (𝜑𝐵𝐶)
2221necomd 2848 . . . . . . . . . . . . . . 15 (𝜑𝐶𝐵)
2322adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝐶 ∈ (𝐴𝐼𝐵)) → 𝐶𝐵)
241, 2, 20, 4, 6, 8, 10, 12, 14, 16, 18cgrane1 25698 . . . . . . . . . . . . . . 15 (𝜑𝐴𝐵)
2524adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝐶 ∈ (𝐴𝐼𝐵)) → 𝐴𝐵)
264adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝐶 ∈ (𝐴𝐼𝐵)) → 𝐺 ∈ TarskiG)
276adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝐶 ∈ (𝐴𝐼𝐵)) → 𝐴𝑃)
2810adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝐶 ∈ (𝐴𝐼𝐵)) → 𝐶𝑃)
298adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝐶 ∈ (𝐴𝐼𝐵)) → 𝐵𝑃)
30 simpr 477 . . . . . . . . . . . . . . . 16 ((𝜑𝐶 ∈ (𝐴𝐼𝐵)) → 𝐶 ∈ (𝐴𝐼𝐵))
311, 3, 2, 26, 27, 28, 29, 30tgbtwncom 25377 . . . . . . . . . . . . . . 15 ((𝜑𝐶 ∈ (𝐴𝐼𝐵)) → 𝐶 ∈ (𝐵𝐼𝐴))
3231orcd 407 . . . . . . . . . . . . . 14 ((𝜑𝐶 ∈ (𝐴𝐼𝐵)) → (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶)))
3323, 25, 323jca 1241 . . . . . . . . . . . . 13 ((𝜑𝐶 ∈ (𝐴𝐼𝐵)) → (𝐶𝐵𝐴𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶))))
3422adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝐴 ∈ (𝐶𝐼𝐵)) → 𝐶𝐵)
3524adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝐴 ∈ (𝐶𝐼𝐵)) → 𝐴𝐵)
364adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝐴 ∈ (𝐶𝐼𝐵)) → 𝐺 ∈ TarskiG)
3710adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝐴 ∈ (𝐶𝐼𝐵)) → 𝐶𝑃)
386adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝐴 ∈ (𝐶𝐼𝐵)) → 𝐴𝑃)
398adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝐴 ∈ (𝐶𝐼𝐵)) → 𝐵𝑃)
40 simpr 477 . . . . . . . . . . . . . . . 16 ((𝜑𝐴 ∈ (𝐶𝐼𝐵)) → 𝐴 ∈ (𝐶𝐼𝐵))
411, 3, 2, 36, 37, 38, 39, 40tgbtwncom 25377 . . . . . . . . . . . . . . 15 ((𝜑𝐴 ∈ (𝐶𝐼𝐵)) → 𝐴 ∈ (𝐵𝐼𝐶))
4241olcd 408 . . . . . . . . . . . . . 14 ((𝜑𝐴 ∈ (𝐶𝐼𝐵)) → (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶)))
4334, 35, 423jca 1241 . . . . . . . . . . . . 13 ((𝜑𝐴 ∈ (𝐶𝐼𝐵)) → (𝐶𝐵𝐴𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶))))
4433, 43jaodan 826 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐶𝐵𝐴𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶))))
451, 2, 20, 10, 6, 8, 4ishlg 25491 . . . . . . . . . . . . 13 (𝜑 → (𝐶((hlG‘𝐺)‘𝐵)𝐴 ↔ (𝐶𝐵𝐴𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶)))))
4645adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐶((hlG‘𝐺)‘𝐵)𝐴 ↔ (𝐶𝐵𝐴𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶)))))
4744, 46mpbird 247 . . . . . . . . . . 11 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐶((hlG‘𝐺)‘𝐵)𝐴)
481, 2, 20, 11, 7, 9, 5, 47hlcomd 25493 . . . . . . . . . 10 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐴((hlG‘𝐺)‘𝐵)𝐶)
491, 2, 3, 5, 7, 9, 11, 13, 15, 17, 19, 20, 48cgrahl 25712 . . . . . . . . 9 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐷((hlG‘𝐺)‘𝐸)𝐹)
501, 2, 20, 13, 17, 15, 5ishlg 25491 . . . . . . . . 9 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐷((hlG‘𝐺)‘𝐸)𝐹 ↔ (𝐷𝐸𝐹𝐸 ∧ (𝐷 ∈ (𝐸𝐼𝐹) ∨ 𝐹 ∈ (𝐸𝐼𝐷)))))
5149, 50mpbid 222 . . . . . . . 8 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐷𝐸𝐹𝐸 ∧ (𝐷 ∈ (𝐸𝐼𝐹) ∨ 𝐹 ∈ (𝐸𝐼𝐷))))
5251simp3d 1074 . . . . . . 7 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐷 ∈ (𝐸𝐼𝐹) ∨ 𝐹 ∈ (𝐸𝐼𝐷)))
534adantr 481 . . . . . . . . . 10 ((𝜑𝐷 ∈ (𝐸𝐼𝐹)) → 𝐺 ∈ TarskiG)
5414adantr 481 . . . . . . . . . 10 ((𝜑𝐷 ∈ (𝐸𝐼𝐹)) → 𝐸𝑃)
5512adantr 481 . . . . . . . . . 10 ((𝜑𝐷 ∈ (𝐸𝐼𝐹)) → 𝐷𝑃)
5616adantr 481 . . . . . . . . . 10 ((𝜑𝐷 ∈ (𝐸𝐼𝐹)) → 𝐹𝑃)
57 simpr 477 . . . . . . . . . 10 ((𝜑𝐷 ∈ (𝐸𝐼𝐹)) → 𝐷 ∈ (𝐸𝐼𝐹))
581, 3, 2, 53, 54, 55, 56, 57tgbtwncom 25377 . . . . . . . . 9 ((𝜑𝐷 ∈ (𝐸𝐼𝐹)) → 𝐷 ∈ (𝐹𝐼𝐸))
5958olcd 408 . . . . . . . 8 ((𝜑𝐷 ∈ (𝐸𝐼𝐹)) → (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸)))
604adantr 481 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝐸𝐼𝐷)) → 𝐺 ∈ TarskiG)
6114adantr 481 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝐸𝐼𝐷)) → 𝐸𝑃)
6216adantr 481 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝐸𝐼𝐷)) → 𝐹𝑃)
6312adantr 481 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝐸𝐼𝐷)) → 𝐷𝑃)
64 simpr 477 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝐸𝐼𝐷)) → 𝐹 ∈ (𝐸𝐼𝐷))
651, 3, 2, 60, 61, 62, 63, 64tgbtwncom 25377 . . . . . . . . 9 ((𝜑𝐹 ∈ (𝐸𝐼𝐷)) → 𝐹 ∈ (𝐷𝐼𝐸))
6665orcd 407 . . . . . . . 8 ((𝜑𝐹 ∈ (𝐸𝐼𝐷)) → (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸)))
6759, 66jaodan 826 . . . . . . 7 ((𝜑 ∧ (𝐷 ∈ (𝐸𝐼𝐹) ∨ 𝐹 ∈ (𝐸𝐼𝐷))) → (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸)))
6852, 67syldan 487 . . . . . 6 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸)))
6968orcd 407 . . . . 5 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → ((𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸)) ∨ 𝐸 ∈ (𝐷𝐼𝐹)))
70 df-3or 1038 . . . . 5 ((𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸) ∨ 𝐸 ∈ (𝐷𝐼𝐹)) ↔ ((𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸)) ∨ 𝐸 ∈ (𝐷𝐼𝐹)))
7169, 70sylibr 224 . . . 4 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸) ∨ 𝐸 ∈ (𝐷𝐼𝐹)))
72 cgracol.l . . . . . 6 𝐿 = (LineG‘𝐺)
731, 2, 4, 20, 6, 8, 10, 12, 14, 16, 18cgracom 25708 . . . . . . 7 (𝜑 → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝐴𝐵𝐶”⟩)
741, 2, 20, 4, 12, 14, 16, 6, 8, 10, 73cgrane1 25698 . . . . . 6 (𝜑𝐷𝐸)
751, 72, 2, 4, 12, 14, 74, 16tgellng 25442 . . . . 5 (𝜑 → (𝐹 ∈ (𝐷𝐿𝐸) ↔ (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸) ∨ 𝐸 ∈ (𝐷𝐼𝐹))))
7675adantr 481 . . . 4 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐹 ∈ (𝐷𝐿𝐸) ↔ (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸) ∨ 𝐸 ∈ (𝐷𝐼𝐹))))
7771, 76mpbird 247 . . 3 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐹 ∈ (𝐷𝐿𝐸))
7877orcd 407 . 2 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
794adantr 481 . . 3 ((𝜑𝐵 ∈ (𝐴𝐼𝐶)) → 𝐺 ∈ TarskiG)
8012adantr 481 . . 3 ((𝜑𝐵 ∈ (𝐴𝐼𝐶)) → 𝐷𝑃)
8114adantr 481 . . 3 ((𝜑𝐵 ∈ (𝐴𝐼𝐶)) → 𝐸𝑃)
8216adantr 481 . . 3 ((𝜑𝐵 ∈ (𝐴𝐼𝐶)) → 𝐹𝑃)
836adantr 481 . . . 4 ((𝜑𝐵 ∈ (𝐴𝐼𝐶)) → 𝐴𝑃)
848adantr 481 . . . 4 ((𝜑𝐵 ∈ (𝐴𝐼𝐶)) → 𝐵𝑃)
8510adantr 481 . . . 4 ((𝜑𝐵 ∈ (𝐴𝐼𝐶)) → 𝐶𝑃)
8618adantr 481 . . . 4 ((𝜑𝐵 ∈ (𝐴𝐼𝐶)) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
87 simpr 477 . . . 4 ((𝜑𝐵 ∈ (𝐴𝐼𝐶)) → 𝐵 ∈ (𝐴𝐼𝐶))
881, 2, 3, 79, 83, 84, 85, 80, 81, 82, 86, 87cgrabtwn 25711 . . 3 ((𝜑𝐵 ∈ (𝐴𝐼𝐶)) → 𝐸 ∈ (𝐷𝐼𝐹))
891, 72, 2, 79, 80, 81, 82, 88btwncolg3 25446 . 2 ((𝜑𝐵 ∈ (𝐴𝐼𝐶)) → (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
9024neneqd 2798 . . . . 5 (𝜑 → ¬ 𝐴 = 𝐵)
91 cgracol.2 . . . . . . 7 (𝜑 → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
9291orcomd 403 . . . . . 6 (𝜑 → (𝐴 = 𝐵𝐶 ∈ (𝐴𝐿𝐵)))
9392ord 392 . . . . 5 (𝜑 → (¬ 𝐴 = 𝐵𝐶 ∈ (𝐴𝐿𝐵)))
9490, 93mpd 15 . . . 4 (𝜑𝐶 ∈ (𝐴𝐿𝐵))
951, 72, 2, 4, 6, 8, 24, 10tgellng 25442 . . . 4 (𝜑 → (𝐶 ∈ (𝐴𝐿𝐵) ↔ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐴𝐼𝐶))))
9694, 95mpbid 222 . . 3 (𝜑 → (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐴𝐼𝐶)))
97 df-3or 1038 . . 3 ((𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐴𝐼𝐶)) ↔ ((𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵)) ∨ 𝐵 ∈ (𝐴𝐼𝐶)))
9896, 97sylib 208 . 2 (𝜑 → ((𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵)) ∨ 𝐵 ∈ (𝐴𝐼𝐶)))
9978, 89, 98mpjaodan 827 1 (𝜑 → (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3o 1036  w3a 1037   = wceq 1482  wcel 1989  wne 2793   class class class wbr 4651  cfv 5886  (class class class)co 6647  ⟨“cs3 13581  Basecbs 15851  distcds 15944  TarskiGcstrkg 25323  Itvcitv 25329  LineGclng 25330  hlGchlg 25489  cgrAccgra 25693
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-rep 4769  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946  ax-cnex 9989  ax-resscn 9990  ax-1cn 9991  ax-icn 9992  ax-addcl 9993  ax-addrcl 9994  ax-mulcl 9995  ax-mulrcl 9996  ax-mulcom 9997  ax-addass 9998  ax-mulass 9999  ax-distr 10000  ax-i2m1 10001  ax-1ne0 10002  ax-1rid 10003  ax-rnegex 10004  ax-rrecex 10005  ax-cnre 10006  ax-pre-lttri 10007  ax-pre-lttrn 10008  ax-pre-ltadd 10009  ax-pre-mulgt0 10010
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-nel 2897  df-ral 2916  df-rex 2917  df-reu 2918  df-rmo 2919  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-pss 3588  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-tp 4180  df-op 4182  df-uni 4435  df-int 4474  df-iun 4520  df-br 4652  df-opab 4711  df-mpt 4728  df-tr 4751  df-id 5022  df-eprel 5027  df-po 5033  df-so 5034  df-fr 5071  df-we 5073  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-pred 5678  df-ord 5724  df-on 5725  df-lim 5726  df-suc 5727  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-f1 5891  df-fo 5892  df-f1o 5893  df-fv 5894  df-riota 6608  df-ov 6650  df-oprab 6651  df-mpt2 6652  df-om 7063  df-1st 7165  df-2nd 7166  df-wrecs 7404  df-recs 7465  df-rdg 7503  df-1o 7557  df-oadd 7561  df-er 7739  df-map 7856  df-pm 7857  df-en 7953  df-dom 7954  df-sdom 7955  df-fin 7956  df-card 8762  df-cda 8987  df-pnf 10073  df-mnf 10074  df-xr 10075  df-ltxr 10076  df-le 10077  df-sub 10265  df-neg 10266  df-nn 11018  df-2 11076  df-3 11077  df-n0 11290  df-xnn0 11361  df-z 11375  df-uz 11685  df-fz 12324  df-fzo 12462  df-hash 13113  df-word 13294  df-concat 13296  df-s1 13297  df-s2 13587  df-s3 13588  df-trkgc 25341  df-trkgb 25342  df-trkgcb 25343  df-trkg 25346  df-cgrg 25400  df-leg 25472  df-hlg 25490  df-cgra 25694
This theorem is referenced by:  cgrancol  25714  tgasa1  25733
  Copyright terms: Public domain W3C validator