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

Theorem dfcgra2 26178
Description: This is the full statement of definition 11.2 of [Schwabhauser] p. 95. This proof serves to confirm that the definition we have chosen, df-cgra 26156 is indeed equivalent to the textbook's definition. (Contributed by Thierry Arnoux, 2-Aug-2020.)
Hypotheses
Ref Expression
dfcgra2.p 𝑃 = (Base‘𝐺)
dfcgra2.i 𝐼 = (Itv‘𝐺)
dfcgra2.m = (dist‘𝐺)
dfcgra2.g (𝜑𝐺 ∈ TarskiG)
dfcgra2.a (𝜑𝐴𝑃)
dfcgra2.b (𝜑𝐵𝑃)
dfcgra2.c (𝜑𝐶𝑃)
dfcgra2.d (𝜑𝐷𝑃)
dfcgra2.e (𝜑𝐸𝑃)
dfcgra2.f (𝜑𝐹𝑃)
Assertion
Ref Expression
dfcgra2 (𝜑 → (⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ↔ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))))
Distinct variable groups:   ,𝑎,𝑐,𝑑,𝑓   𝐴,𝑎,𝑐,𝑑,𝑓   𝐵,𝑎,𝑐,𝑑,𝑓   𝐶,𝑎,𝑐,𝑑,𝑓   𝐷,𝑎,𝑐,𝑑,𝑓   𝐸,𝑎,𝑐,𝑑,𝑓   𝐹,𝑎,𝑐,𝑑,𝑓   𝐺,𝑎,𝑐,𝑑,𝑓   𝐼,𝑎,𝑐,𝑑,𝑓   𝑃,𝑎,𝑐,𝑑,𝑓   𝜑,𝑎,𝑐,𝑑,𝑓

Proof of Theorem dfcgra2
Dummy variables 𝑡 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfcgra2.p . . . . 5 𝑃 = (Base‘𝐺)
2 dfcgra2.i . . . . 5 𝐼 = (Itv‘𝐺)
3 eqid 2778 . . . . 5 (hlG‘𝐺) = (hlG‘𝐺)
4 dfcgra2.g . . . . . 6 (𝜑𝐺 ∈ TarskiG)
54adantr 474 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐺 ∈ TarskiG)
6 dfcgra2.a . . . . . 6 (𝜑𝐴𝑃)
76adantr 474 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐴𝑃)
8 dfcgra2.b . . . . . 6 (𝜑𝐵𝑃)
98adantr 474 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐵𝑃)
10 dfcgra2.c . . . . . 6 (𝜑𝐶𝑃)
1110adantr 474 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐶𝑃)
12 dfcgra2.d . . . . . 6 (𝜑𝐷𝑃)
1312adantr 474 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐷𝑃)
14 dfcgra2.e . . . . . 6 (𝜑𝐸𝑃)
1514adantr 474 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐸𝑃)
16 dfcgra2.f . . . . . 6 (𝜑𝐹𝑃)
1716adantr 474 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐹𝑃)
18 simpr 479 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
191, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane1 26160 . . . 4 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐴𝐵)
201, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane2 26161 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐵𝐶)
2120necomd 3024 . . . 4 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐶𝐵)
2219, 21jca 507 . . 3 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → (𝐴𝐵𝐶𝐵))
231, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane3 26162 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐸𝐷)
2423necomd 3024 . . . 4 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐷𝐸)
251, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane4 26163 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐸𝐹)
2625necomd 3024 . . . 4 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐹𝐸)
2724, 26jca 507 . . 3 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → (𝐷𝐸𝐹𝐸))
28 simprl 761 . . . . . . . . 9 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))))
29 simprr 763 . . . . . . . . 9 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))
305ad5antr 724 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐺 ∈ TarskiG)
31 simp-5r 776 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑎𝑃)
329ad5antr 724 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐵𝑃)
33 simp-4r 774 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑐𝑃)
34 simpllr 766 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑑𝑃)
3515ad5antr 724 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐸𝑃)
36 simplr 759 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑓𝑃)
3717ad5antr 724 . . . . . . . . . . 11 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐹𝑃)
3813ad5antr 724 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐷𝑃)
3911ad5antr 724 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐶𝑃)
407ad5antr 724 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐴𝑃)
4118ad5antr 724 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
421, 2, 30, 3, 40, 32, 39, 38, 35, 37, 41cgracom 26170 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝐴𝐵𝐶”⟩)
4328simplld 758 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐴 ∈ (𝐵𝐼𝑎))
44 dfcgra2.m . . . . . . . . . . . . . . . . . 18 = (dist‘𝐺)
4519ad5antr 724 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐴𝐵)
461, 44, 2, 30, 32, 40, 31, 43, 45tgbtwnne 25841 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐵𝑎)
471, 2, 3, 32, 31, 40, 30, 40, 43, 46, 45btwnhl1 25963 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐴((hlG‘𝐺)‘𝐵)𝑎)
481, 2, 3, 40, 31, 32, 30, 47hlcomd 25955 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑎((hlG‘𝐺)‘𝐵)𝐴)
491, 2, 3, 30, 38, 35, 37, 40, 32, 39, 42, 31, 48cgrahl1 26164 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝑎𝐵𝐶”⟩)
5028simprld 762 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐶 ∈ (𝐵𝐼𝑐))
5121ad5antr 724 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐶𝐵)
521, 44, 2, 30, 32, 39, 33, 50, 51tgbtwnne 25841 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐵𝑐)
531, 2, 3, 32, 33, 39, 30, 40, 50, 52, 51btwnhl1 25963 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐶((hlG‘𝐺)‘𝐵)𝑐)
541, 2, 3, 39, 33, 32, 30, 53hlcomd 25955 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑐((hlG‘𝐺)‘𝐵)𝐶)
551, 2, 3, 30, 38, 35, 37, 31, 32, 39, 49, 33, 54cgrahl2 26165 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝑎𝐵𝑐”⟩)
561, 2, 30, 3, 38, 35, 37, 31, 32, 33, 55cgracom 26170 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ⟨“𝑎𝐵𝑐”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
5729simplld 758 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐷 ∈ (𝐸𝐼𝑑))
5824ad5antr 724 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐷𝐸)
591, 44, 2, 30, 35, 38, 34, 57, 58tgbtwnne 25841 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐸𝑑)
601, 2, 3, 35, 34, 38, 30, 40, 57, 59, 58btwnhl1 25963 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐷((hlG‘𝐺)‘𝐸)𝑑)
611, 2, 3, 38, 34, 35, 30, 60hlcomd 25955 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑑((hlG‘𝐺)‘𝐸)𝐷)
621, 2, 3, 30, 31, 32, 33, 38, 35, 37, 56, 34, 61cgrahl1 26164 . . . . . . . . . . 11 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ⟨“𝑎𝐵𝑐”⟩(cgrA‘𝐺)⟨“𝑑𝐸𝐹”⟩)
6329simprld 762 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐹 ∈ (𝐸𝐼𝑓))
6426ad5antr 724 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐹𝐸)
651, 44, 2, 30, 35, 37, 36, 63, 64tgbtwnne 25841 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐸𝑓)
661, 2, 3, 35, 36, 37, 30, 40, 63, 65, 64btwnhl1 25963 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐹((hlG‘𝐺)‘𝐸)𝑓)
671, 2, 3, 37, 36, 35, 30, 66hlcomd 25955 . . . . . . . . . . 11 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑓((hlG‘𝐺)‘𝐸)𝐹)
681, 2, 3, 30, 31, 32, 33, 34, 35, 37, 62, 36, 67cgrahl2 26165 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ⟨“𝑎𝐵𝑐”⟩(cgrA‘𝐺)⟨“𝑑𝐸𝑓”⟩)
691, 2, 3, 30, 31, 32, 33, 34, 35, 36, 68cgrane1 26160 . . . . . . . . . . 11 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑎𝐵)
701, 2, 3, 31, 40, 32, 30, 69hlid 25960 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑎((hlG‘𝐺)‘𝐵)𝑎)
711, 2, 3, 30, 31, 32, 33, 34, 35, 36, 68cgrane2 26161 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐵𝑐)
7271necomd 3024 . . . . . . . . . . 11 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑐𝐵)
731, 2, 3, 33, 40, 32, 30, 72hlid 25960 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑐((hlG‘𝐺)‘𝐵)𝑐)
741, 44, 2, 30, 32, 40, 31, 43tgbtwncom 25839 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐴 ∈ (𝑎𝐼𝐵))
7528simplrd 760 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐴 𝑎) = (𝐸 𝐷))
761, 44, 2, 30, 40, 31, 35, 38, 75tgcgrcoml 25830 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝑎 𝐴) = (𝐸 𝐷))
7729simplrd 760 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐷 𝑑) = (𝐵 𝐴))
7877eqcomd 2784 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐵 𝐴) = (𝐷 𝑑))
791, 44, 2, 30, 32, 40, 38, 34, 78tgcgrcoml 25830 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐴 𝐵) = (𝐷 𝑑))
801, 44, 2, 30, 31, 40, 32, 35, 38, 34, 74, 57, 76, 79tgcgrextend 25836 . . . . . . . . . . 11 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝑎 𝐵) = (𝐸 𝑑))
811, 44, 2, 30, 31, 32, 35, 34, 80tgcgrcoml 25830 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐵 𝑎) = (𝐸 𝑑))
821, 44, 2, 30, 32, 39, 33, 50tgbtwncom 25839 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐶 ∈ (𝑐𝐼𝐵))
8328simprrd 764 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐶 𝑐) = (𝐸 𝐹))
841, 44, 2, 30, 39, 33, 35, 37, 83tgcgrcoml 25830 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝑐 𝐶) = (𝐸 𝐹))
8529simprrd 764 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐹 𝑓) = (𝐵 𝐶))
8685eqcomd 2784 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐵 𝐶) = (𝐹 𝑓))
871, 44, 2, 30, 32, 39, 37, 36, 86tgcgrcoml 25830 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐶 𝐵) = (𝐹 𝑓))
881, 44, 2, 30, 33, 39, 32, 35, 37, 36, 82, 63, 84, 87tgcgrextend 25836 . . . . . . . . . . 11 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝑐 𝐵) = (𝐸 𝑓))
891, 44, 2, 30, 33, 32, 35, 36, 88tgcgrcoml 25830 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐵 𝑐) = (𝐸 𝑓))
901, 2, 3, 30, 31, 32, 33, 34, 35, 36, 68, 31, 44, 33, 70, 73, 81, 89cgracgr 26166 . . . . . . . . 9 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝑎 𝑐) = (𝑑 𝑓))
9128, 29, 903jca 1119 . . . . . . . 8 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))
9291ex 403 . . . . . . 7 ((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) → ((((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))) → (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))))
9392reximdva 3198 . . . . . 6 (((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) → (∃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))) → ∃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))))
9493reximdva 3198 . . . . 5 ((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) → (∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))) → ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))))
9594imp 397 . . . 4 (((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))
961, 44, 2, 4, 8, 6, 14, 12axtgsegcon 25815 . . . . . . . 8 (𝜑 → ∃𝑎𝑃 (𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)))
971, 44, 2, 4, 8, 10, 14, 16axtgsegcon 25815 . . . . . . . 8 (𝜑 → ∃𝑐𝑃 (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)))
98 reeanv 3293 . . . . . . . 8 (∃𝑎𝑃𝑐𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ↔ (∃𝑎𝑃 (𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ ∃𝑐𝑃 (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))))
9996, 97, 98sylanbrc 578 . . . . . . 7 (𝜑 → ∃𝑎𝑃𝑐𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))))
1001, 44, 2, 4, 14, 12, 8, 6axtgsegcon 25815 . . . . . . . 8 (𝜑 → ∃𝑑𝑃 (𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)))
1011, 44, 2, 4, 14, 16, 8, 10axtgsegcon 25815 . . . . . . . 8 (𝜑 → ∃𝑓𝑃 (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))
102 reeanv 3293 . . . . . . . 8 (∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ↔ (∃𝑑𝑃 (𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ ∃𝑓𝑃 (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))
103100, 101, 102sylanbrc 578 . . . . . . 7 (𝜑 → ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))
10499, 103jca 507 . . . . . 6 (𝜑 → (∃𝑎𝑃𝑐𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
105 r19.41vv 3277 . . . . . . . . 9 (∃𝑑𝑃𝑓𝑃 (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)))) ↔ (∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)))))
106 ancom 454 . . . . . . . . . 10 ((((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)))) ↔ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
1071062rexbii 3225 . . . . . . . . 9 (∃𝑑𝑃𝑓𝑃 (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)))) ↔ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
108 ancom 454 . . . . . . . . 9 ((∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)))) ↔ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
109105, 107, 1083bitr3i 293 . . . . . . . 8 (∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))) ↔ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
1101092rexbii 3225 . . . . . . 7 (∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))) ↔ ∃𝑎𝑃𝑐𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
111 r19.41vv 3277 . . . . . . 7 (∃𝑎𝑃𝑐𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))) ↔ (∃𝑎𝑃𝑐𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
112110, 111bitr2i 268 . . . . . 6 ((∃𝑎𝑃𝑐𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))) ↔ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
113104, 112sylib 210 . . . . 5 (𝜑 → ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
114113adantr 474 . . . 4 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
11595, 114reximddv2 3202 . . 3 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))
11622, 27, 1153jca 1119 . 2 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))))
117 df-3an 1073 . . 3 (((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))) ↔ (((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸)) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))))
1184ad6antr 726 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐺 ∈ TarskiG)
11912ad6antr 726 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐷𝑃)
12014ad6antr 726 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐸𝑃)
12116ad6antr 726 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐹𝑃)
1226ad6antr 726 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐴𝑃)
1238ad6antr 726 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐵𝑃)
12410ad6antr 726 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐶𝑃)
125 simp-4r 774 . . . . . . . . . 10 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝑦𝑃)
126 simp-5r 776 . . . . . . . . . . 11 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝑥𝑃)
127 simpllr 766 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝑧𝑃)
128 simplr 759 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝑡𝑃)
129 eqid 2778 . . . . . . . . . . . . . 14 (cgrG‘𝐺) = (cgrG‘𝐺)
130 simpr1 1205 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))))
131130simplld 758 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐴 ∈ (𝐵𝐼𝑥))
132 simpr2 1207 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))))
133132simplld 758 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐷 ∈ (𝐸𝐼𝑧))
1341, 44, 2, 118, 120, 119, 127, 133tgbtwncom 25839 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐷 ∈ (𝑧𝐼𝐸))
135132simplrd 760 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐷 𝑧) = (𝐵 𝐴))
136135eqcomd 2784 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐵 𝐴) = (𝐷 𝑧))
1371, 44, 2, 118, 123, 122, 119, 127, 136tgcgrcomr 25829 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐵 𝐴) = (𝑧 𝐷))
138130simplrd 760 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐴 𝑥) = (𝐸 𝐷))
1391, 44, 2, 118, 122, 126, 120, 119, 138tgcgrcomr 25829 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐴 𝑥) = (𝐷 𝐸))
1401, 44, 2, 118, 123, 122, 126, 127, 119, 120, 131, 134, 137, 139tgcgrextend 25836 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐵 𝑥) = (𝑧 𝐸))
1411, 44, 2, 118, 123, 126, 127, 120, 140tgcgrcoml 25830 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝑥 𝐵) = (𝑧 𝐸))
142130simprld 762 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐶 ∈ (𝐵𝐼𝑦))
1431, 44, 2, 118, 123, 124, 125, 142tgbtwncom 25839 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐶 ∈ (𝑦𝐼𝐵))
144132simprld 762 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐹 ∈ (𝐸𝐼𝑡))
145130simprrd 764 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐶 𝑦) = (𝐸 𝐹))
1461, 44, 2, 118, 124, 125, 120, 121, 145tgcgrcoml 25830 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝑦 𝐶) = (𝐸 𝐹))
147132simprrd 764 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐹 𝑡) = (𝐵 𝐶))
148147eqcomd 2784 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐵 𝐶) = (𝐹 𝑡))
1491, 44, 2, 118, 123, 124, 121, 128, 148tgcgrcoml 25830 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐶 𝐵) = (𝐹 𝑡))
1501, 44, 2, 118, 125, 124, 123, 120, 121, 128, 143, 144, 146, 149tgcgrextend 25836 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝑦 𝐵) = (𝐸 𝑡))
1511, 44, 2, 118, 125, 123, 120, 128, 150tgcgrcoml 25830 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐵 𝑦) = (𝐸 𝑡))
152 simpr3 1209 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝑥 𝑦) = (𝑧 𝑡))
1531, 44, 2, 118, 126, 125, 127, 128, 152tgcgrcomlr 25831 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝑦 𝑥) = (𝑡 𝑧))
1541, 44, 129, 118, 126, 123, 125, 127, 120, 128, 141, 151, 153trgcgr 25867 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ⟨“𝑥𝐵𝑦”⟩(cgrG‘𝐺)⟨“𝑧𝐸𝑡”⟩)
155 simp-6r 778 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸)))
156155simprld 762 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐷𝐸)
1571, 44, 2, 118, 120, 119, 127, 133, 156tgbtwnne 25841 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐸𝑧)
1581, 2, 3, 120, 127, 119, 118, 123, 133, 157, 156btwnhl1 25963 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐷((hlG‘𝐺)‘𝐸)𝑧)
1591, 2, 3, 119, 127, 120, 118, 158hlcomd 25955 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝑧((hlG‘𝐺)‘𝐸)𝐷)
160155simprrd 764 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐹𝐸)
1611, 44, 2, 118, 120, 121, 128, 144, 160tgbtwnne 25841 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐸𝑡)
1621, 2, 3, 120, 128, 121, 118, 123, 144, 161, 160btwnhl1 25963 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐹((hlG‘𝐺)‘𝐸)𝑡)
1631, 2, 3, 121, 128, 120, 118, 162hlcomd 25955 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝑡((hlG‘𝐺)‘𝐸)𝐹)
1641, 2, 3, 118, 126, 123, 125, 119, 120, 121, 127, 128, 154, 159, 163iscgrad 26159 . . . . . . . . . . . 12 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ⟨“𝑥𝐵𝑦”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
1651, 2, 118, 3, 126, 123, 125, 119, 120, 121, 164cgracom 26170 . . . . . . . . . . 11 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝑥𝐵𝑦”⟩)
166155simplld 758 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐴𝐵)
1671, 44, 2, 118, 123, 122, 126, 131, 166tgbtwnne 25841 . . . . . . . . . . . 12 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐵𝑥)
1681, 2, 3, 123, 126, 122, 118, 122, 131, 167, 166btwnhl1 25963 . . . . . . . . . . 11 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐴((hlG‘𝐺)‘𝐵)𝑥)
1691, 2, 3, 118, 119, 120, 121, 126, 123, 125, 165, 122, 168cgrahl1 26164 . . . . . . . . . 10 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝐴𝐵𝑦”⟩)
170155simplrd 760 . . . . . . . . . . . 12 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐶𝐵)
1711, 44, 2, 118, 123, 124, 125, 142, 170tgbtwnne 25841 . . . . . . . . . . 11 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐵𝑦)
1721, 2, 3, 123, 125, 124, 118, 122, 142, 171, 170btwnhl1 25963 . . . . . . . . . 10 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐶((hlG‘𝐺)‘𝐵)𝑦)
1731, 2, 3, 118, 119, 120, 121, 122, 123, 125, 169, 124, 172cgrahl2 26165 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝐴𝐵𝐶”⟩)
1741, 2, 118, 3, 119, 120, 121, 122, 123, 124, 173cgracom 26170 . . . . . . . 8 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
175174adantl3r 740 . . . . . . 7 ((((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓))) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
176 simpr 479 . . . . . . . 8 (((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓))) → ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓)))
177 eqidd 2779 . . . . . . . . . . . . 13 (𝑑 = 𝑧𝐷 = 𝐷)
178 oveq2 6930 . . . . . . . . . . . . 13 (𝑑 = 𝑧 → (𝐸𝐼𝑑) = (𝐸𝐼𝑧))
179177, 178eleq12d 2853 . . . . . . . . . . . 12 (𝑑 = 𝑧 → (𝐷 ∈ (𝐸𝐼𝑑) ↔ 𝐷 ∈ (𝐸𝐼𝑧)))
180 oveq2 6930 . . . . . . . . . . . . 13 (𝑑 = 𝑧 → (𝐷 𝑑) = (𝐷 𝑧))
181 eqidd 2779 . . . . . . . . . . . . 13 (𝑑 = 𝑧 → (𝐵 𝐴) = (𝐵 𝐴))
182180, 181eqeq12d 2793 . . . . . . . . . . . 12 (𝑑 = 𝑧 → ((𝐷 𝑑) = (𝐵 𝐴) ↔ (𝐷 𝑧) = (𝐵 𝐴)))
183179, 182anbi12d 624 . . . . . . . . . . 11 (𝑑 = 𝑧 → ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ↔ (𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴))))
184 biidd 254 . . . . . . . . . . 11 (𝑑 = 𝑧 → ((𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)) ↔ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))
185183, 184anbi12d 624 . . . . . . . . . 10 (𝑑 = 𝑧 → (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ↔ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
186 eqidd 2779 . . . . . . . . . . 11 (𝑑 = 𝑧 → (𝑥 𝑦) = (𝑥 𝑦))
187 oveq1 6929 . . . . . . . . . . 11 (𝑑 = 𝑧 → (𝑑 𝑓) = (𝑧 𝑓))
188186, 187eqeq12d 2793 . . . . . . . . . 10 (𝑑 = 𝑧 → ((𝑥 𝑦) = (𝑑 𝑓) ↔ (𝑥 𝑦) = (𝑧 𝑓)))
189185, 1883anbi23d 1512 . . . . . . . . 9 (𝑑 = 𝑧 → ((((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓)) ↔ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑓))))
190 biidd 254 . . . . . . . . . . 11 (𝑓 = 𝑡 → ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ↔ (𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴))))
191 eqidd 2779 . . . . . . . . . . . . 13 (𝑓 = 𝑡𝐹 = 𝐹)
192 oveq2 6930 . . . . . . . . . . . . 13 (𝑓 = 𝑡 → (𝐸𝐼𝑓) = (𝐸𝐼𝑡))
193191, 192eleq12d 2853 . . . . . . . . . . . 12 (𝑓 = 𝑡 → (𝐹 ∈ (𝐸𝐼𝑓) ↔ 𝐹 ∈ (𝐸𝐼𝑡)))
194 oveq2 6930 . . . . . . . . . . . . 13 (𝑓 = 𝑡 → (𝐹 𝑓) = (𝐹 𝑡))
195 eqidd 2779 . . . . . . . . . . . . 13 (𝑓 = 𝑡 → (𝐵 𝐶) = (𝐵 𝐶))
196194, 195eqeq12d 2793 . . . . . . . . . . . 12 (𝑓 = 𝑡 → ((𝐹 𝑓) = (𝐵 𝐶) ↔ (𝐹 𝑡) = (𝐵 𝐶)))
197193, 196anbi12d 624 . . . . . . . . . . 11 (𝑓 = 𝑡 → ((𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)) ↔ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))))
198190, 197anbi12d 624 . . . . . . . . . 10 (𝑓 = 𝑡 → (((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ↔ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶)))))
199 eqidd 2779 . . . . . . . . . . 11 (𝑓 = 𝑡 → (𝑥 𝑦) = (𝑥 𝑦))
200 oveq2 6930 . . . . . . . . . . 11 (𝑓 = 𝑡 → (𝑧 𝑓) = (𝑧 𝑡))
201199, 200eqeq12d 2793 . . . . . . . . . 10 (𝑓 = 𝑡 → ((𝑥 𝑦) = (𝑧 𝑓) ↔ (𝑥 𝑦) = (𝑧 𝑡)))
202198, 2013anbi23d 1512 . . . . . . . . 9 (𝑓 = 𝑡 → ((((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑓)) ↔ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))))
203189, 202cbvrex2v 3376 . . . . . . . 8 (∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓)) ↔ ∃𝑧𝑃𝑡𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡)))
204176, 203sylib 210 . . . . . . 7 (((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓))) → ∃𝑧𝑃𝑡𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡)))
205175, 204r19.29vva 3267 . . . . . 6 (((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
206205adantl3r 740 . . . . 5 ((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
207 simpr 479 . . . . . 6 (((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))) → ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))
208 eqidd 2779 . . . . . . . . . . . 12 (𝑎 = 𝑥𝐴 = 𝐴)
209 oveq2 6930 . . . . . . . . . . . 12 (𝑎 = 𝑥 → (𝐵𝐼𝑎) = (𝐵𝐼𝑥))
210208, 209eleq12d 2853 . . . . . . . . . . 11 (𝑎 = 𝑥 → (𝐴 ∈ (𝐵𝐼𝑎) ↔ 𝐴 ∈ (𝐵𝐼𝑥)))
211 oveq2 6930 . . . . . . . . . . . 12 (𝑎 = 𝑥 → (𝐴 𝑎) = (𝐴 𝑥))
212 eqidd 2779 . . . . . . . . . . . 12 (𝑎 = 𝑥 → (𝐸 𝐷) = (𝐸 𝐷))
213211, 212eqeq12d 2793 . . . . . . . . . . 11 (𝑎 = 𝑥 → ((𝐴 𝑎) = (𝐸 𝐷) ↔ (𝐴 𝑥) = (𝐸 𝐷)))
214210, 213anbi12d 624 . . . . . . . . . 10 (𝑎 = 𝑥 → ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ↔ (𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷))))
215 biidd 254 . . . . . . . . . 10 (𝑎 = 𝑥 → ((𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)) ↔ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))))
216214, 215anbi12d 624 . . . . . . . . 9 (𝑎 = 𝑥 → (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ↔ ((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)))))
217 oveq1 6929 . . . . . . . . . 10 (𝑎 = 𝑥 → (𝑎 𝑐) = (𝑥 𝑐))
218 eqidd 2779 . . . . . . . . . 10 (𝑎 = 𝑥 → (𝑑 𝑓) = (𝑑 𝑓))
219217, 218eqeq12d 2793 . . . . . . . . 9 (𝑎 = 𝑥 → ((𝑎 𝑐) = (𝑑 𝑓) ↔ (𝑥 𝑐) = (𝑑 𝑓)))
220216, 2193anbi13d 1511 . . . . . . . 8 (𝑎 = 𝑥 → ((((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)) ↔ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑐) = (𝑑 𝑓))))
2212202rexbidv 3242 . . . . . . 7 (𝑎 = 𝑥 → (∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)) ↔ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑐) = (𝑑 𝑓))))
222 biidd 254 . . . . . . . . . 10 (𝑐 = 𝑦 → ((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ↔ (𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷))))
223 eqidd 2779 . . . . . . . . . . . 12 (𝑐 = 𝑦𝐶 = 𝐶)
224 oveq2 6930 . . . . . . . . . . . 12 (𝑐 = 𝑦 → (𝐵𝐼𝑐) = (𝐵𝐼𝑦))
225223, 224eleq12d 2853 . . . . . . . . . . 11 (𝑐 = 𝑦 → (𝐶 ∈ (𝐵𝐼𝑐) ↔ 𝐶 ∈ (𝐵𝐼𝑦)))
226 oveq2 6930 . . . . . . . . . . . 12 (𝑐 = 𝑦 → (𝐶 𝑐) = (𝐶 𝑦))
227 eqidd 2779 . . . . . . . . . . . 12 (𝑐 = 𝑦 → (𝐸 𝐹) = (𝐸 𝐹))
228226, 227eqeq12d 2793 . . . . . . . . . . 11 (𝑐 = 𝑦 → ((𝐶 𝑐) = (𝐸 𝐹) ↔ (𝐶 𝑦) = (𝐸 𝐹)))
229225, 228anbi12d 624 . . . . . . . . . 10 (𝑐 = 𝑦 → ((𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)) ↔ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))))
230222, 229anbi12d 624 . . . . . . . . 9 (𝑐 = 𝑦 → (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ↔ ((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹)))))
231 oveq2 6930 . . . . . . . . . 10 (𝑐 = 𝑦 → (𝑥 𝑐) = (𝑥 𝑦))
232 eqidd 2779 . . . . . . . . . 10 (𝑐 = 𝑦 → (𝑑 𝑓) = (𝑑 𝑓))
233231, 232eqeq12d 2793 . . . . . . . . 9 (𝑐 = 𝑦 → ((𝑥 𝑐) = (𝑑 𝑓) ↔ (𝑥 𝑦) = (𝑑 𝑓)))
234230, 2333anbi13d 1511 . . . . . . . 8 (𝑐 = 𝑦 → ((((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑐) = (𝑑 𝑓)) ↔ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓))))
2352342rexbidv 3242 . . . . . . 7 (𝑐 = 𝑦 → (∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑐) = (𝑑 𝑓)) ↔ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓))))
236221, 235cbvrex2v 3376 . . . . . 6 (∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)) ↔ ∃𝑥𝑃𝑦𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓)))
237207, 236sylib 210 . . . . 5 (((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))) → ∃𝑥𝑃𝑦𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓)))
238206, 237r19.29vva 3267 . . . 4 (((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
239238anasss 460 . . 3 ((𝜑 ∧ (((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸)) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
240117, 239sylan2b 587 . 2 ((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
241116, 240impbida 791 1 (𝜑 → (⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ↔ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386  w3a 1071   = wceq 1601  wcel 2107  wne 2969  wrex 3091   class class class wbr 4886  cfv 6135  (class class class)co 6922  ⟨“cs3 13993  Basecbs 16255  distcds 16347  TarskiGcstrkg 25781  Itvcitv 25787  cgrGccgrg 25861  hlGchlg 25951  cgrAccgra 26155
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-int 4711  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-om 7344  df-1st 7445  df-2nd 7446  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-oadd 7847  df-er 8026  df-map 8142  df-pm 8143  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-card 9098  df-cda 9325  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-nn 11375  df-2 11438  df-3 11439  df-n0 11643  df-xnn0 11715  df-z 11729  df-uz 11993  df-fz 12644  df-fzo 12785  df-hash 13436  df-word 13600  df-concat 13661  df-s1 13686  df-s2 13999  df-s3 14000  df-trkgc 25799  df-trkgb 25800  df-trkgcb 25801  df-trkg 25804  df-cgrg 25862  df-leg 25934  df-hlg 25952  df-cgra 26156
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator