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

Theorem dfcgra2 25935
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 25914 is indeed equivalent with 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 2771 . . . . 5 (hlG‘𝐺) = (hlG‘𝐺)
4 dfcgra2.g . . . . . 6 (𝜑𝐺 ∈ TarskiG)
54adantr 466 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐺 ∈ TarskiG)
6 dfcgra2.a . . . . . 6 (𝜑𝐴𝑃)
76adantr 466 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐴𝑃)
8 dfcgra2.b . . . . . 6 (𝜑𝐵𝑃)
98adantr 466 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐵𝑃)
10 dfcgra2.c . . . . . 6 (𝜑𝐶𝑃)
1110adantr 466 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐶𝑃)
12 dfcgra2.d . . . . . 6 (𝜑𝐷𝑃)
1312adantr 466 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐷𝑃)
14 dfcgra2.e . . . . . 6 (𝜑𝐸𝑃)
1514adantr 466 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐸𝑃)
16 dfcgra2.f . . . . . 6 (𝜑𝐹𝑃)
1716adantr 466 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐹𝑃)
18 simpr 471 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
191, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane1 25918 . . . 4 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐴𝐵)
201, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane2 25919 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐵𝐶)
2120necomd 2998 . . . 4 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐶𝐵)
2219, 21jca 501 . . 3 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → (𝐴𝐵𝐶𝐵))
231, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane3 25920 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐸𝐷)
2423necomd 2998 . . . 4 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐷𝐸)
251, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane4 25921 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐸𝐹)
2625necomd 2998 . . . 4 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐹𝐸)
2724, 26jca 501 . . 3 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → (𝐷𝐸𝐹𝐸))
28 simprl 754 . . . . . . . . 9 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))))
29 simprr 756 . . . . . . . . 9 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))
305ad5antr 716 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐺 ∈ TarskiG)
31 simp-5r 774 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑎𝑃)
329ad5antr 716 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐵𝑃)
33 simp-4r 770 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑐𝑃)
34 simpllr 760 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑑𝑃)
3515ad5antr 716 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐸𝑃)
36 simplr 752 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑓𝑃)
3717ad5antr 716 . . . . . . . . . . 11 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐹𝑃)
3813ad5antr 716 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐷𝑃)
3911ad5antr 716 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐶𝑃)
407ad5antr 716 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐴𝑃)
4118ad5antr 716 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
421, 2, 30, 3, 40, 32, 39, 38, 35, 37, 41cgracom 25928 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝐴𝐵𝐶”⟩)
4328simplld 751 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐴 ∈ (𝐵𝐼𝑎))
44 dfcgra2.m . . . . . . . . . . . . . . . . . 18 = (dist‘𝐺)
4519ad5antr 716 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐴𝐵)
461, 44, 2, 30, 32, 40, 31, 43, 45tgbtwnne 25599 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐵𝑎)
471, 2, 3, 32, 31, 40, 30, 40, 43, 46, 45btwnhl1 25721 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐴((hlG‘𝐺)‘𝐵)𝑎)
481, 2, 3, 40, 31, 32, 30, 47hlcomd 25713 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑎((hlG‘𝐺)‘𝐵)𝐴)
491, 2, 3, 30, 38, 35, 37, 40, 32, 39, 42, 31, 48cgrahl1 25922 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝑎𝐵𝐶”⟩)
5028simprld 755 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐶 ∈ (𝐵𝐼𝑐))
5121ad5antr 716 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐶𝐵)
521, 44, 2, 30, 32, 39, 33, 50, 51tgbtwnne 25599 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐵𝑐)
531, 2, 3, 32, 33, 39, 30, 40, 50, 52, 51btwnhl1 25721 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐶((hlG‘𝐺)‘𝐵)𝑐)
541, 2, 3, 39, 33, 32, 30, 53hlcomd 25713 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑐((hlG‘𝐺)‘𝐵)𝐶)
551, 2, 3, 30, 38, 35, 37, 31, 32, 39, 49, 33, 54cgrahl2 25923 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝑎𝐵𝑐”⟩)
561, 2, 30, 3, 38, 35, 37, 31, 32, 33, 55cgracom 25928 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ⟨“𝑎𝐵𝑐”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
5729simplld 751 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐷 ∈ (𝐸𝐼𝑑))
5824ad5antr 716 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐷𝐸)
591, 44, 2, 30, 35, 38, 34, 57, 58tgbtwnne 25599 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐸𝑑)
601, 2, 3, 35, 34, 38, 30, 40, 57, 59, 58btwnhl1 25721 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐷((hlG‘𝐺)‘𝐸)𝑑)
611, 2, 3, 38, 34, 35, 30, 60hlcomd 25713 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑑((hlG‘𝐺)‘𝐸)𝐷)
621, 2, 3, 30, 31, 32, 33, 38, 35, 37, 56, 34, 61cgrahl1 25922 . . . . . . . . . . 11 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ⟨“𝑎𝐵𝑐”⟩(cgrA‘𝐺)⟨“𝑑𝐸𝐹”⟩)
6329simprld 755 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐹 ∈ (𝐸𝐼𝑓))
6426ad5antr 716 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐹𝐸)
651, 44, 2, 30, 35, 37, 36, 63, 64tgbtwnne 25599 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐸𝑓)
661, 2, 3, 35, 36, 37, 30, 40, 63, 65, 64btwnhl1 25721 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐹((hlG‘𝐺)‘𝐸)𝑓)
671, 2, 3, 37, 36, 35, 30, 66hlcomd 25713 . . . . . . . . . . 11 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑓((hlG‘𝐺)‘𝐸)𝐹)
681, 2, 3, 30, 31, 32, 33, 34, 35, 37, 62, 36, 67cgrahl2 25923 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ⟨“𝑎𝐵𝑐”⟩(cgrA‘𝐺)⟨“𝑑𝐸𝑓”⟩)
691, 2, 3, 30, 31, 32, 33, 34, 35, 36, 68cgrane1 25918 . . . . . . . . . . 11 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑎𝐵)
701, 2, 3, 31, 40, 32, 30, 69hlid 25718 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑎((hlG‘𝐺)‘𝐵)𝑎)
711, 2, 3, 30, 31, 32, 33, 34, 35, 36, 68cgrane2 25919 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐵𝑐)
7271necomd 2998 . . . . . . . . . . 11 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑐𝐵)
731, 2, 3, 33, 40, 32, 30, 72hlid 25718 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑐((hlG‘𝐺)‘𝐵)𝑐)
741, 44, 2, 30, 32, 40, 31, 43tgbtwncom 25597 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐴 ∈ (𝑎𝐼𝐵))
7528simplrd 753 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐴 𝑎) = (𝐸 𝐷))
761, 44, 2, 30, 40, 31, 35, 38, 75tgcgrcoml 25588 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝑎 𝐴) = (𝐸 𝐷))
7729simplrd 753 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐷 𝑑) = (𝐵 𝐴))
7877eqcomd 2777 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐵 𝐴) = (𝐷 𝑑))
791, 44, 2, 30, 32, 40, 38, 34, 78tgcgrcoml 25588 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐴 𝐵) = (𝐷 𝑑))
801, 44, 2, 30, 31, 40, 32, 35, 38, 34, 74, 57, 76, 79tgcgrextend 25594 . . . . . . . . . . 11 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝑎 𝐵) = (𝐸 𝑑))
811, 44, 2, 30, 31, 32, 35, 34, 80tgcgrcoml 25588 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐵 𝑎) = (𝐸 𝑑))
821, 44, 2, 30, 32, 39, 33, 50tgbtwncom 25597 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐶 ∈ (𝑐𝐼𝐵))
8328simprrd 757 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐶 𝑐) = (𝐸 𝐹))
841, 44, 2, 30, 39, 33, 35, 37, 83tgcgrcoml 25588 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝑐 𝐶) = (𝐸 𝐹))
8529simprrd 757 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐹 𝑓) = (𝐵 𝐶))
8685eqcomd 2777 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐵 𝐶) = (𝐹 𝑓))
871, 44, 2, 30, 32, 39, 37, 36, 86tgcgrcoml 25588 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐶 𝐵) = (𝐹 𝑓))
881, 44, 2, 30, 33, 39, 32, 35, 37, 36, 82, 63, 84, 87tgcgrextend 25594 . . . . . . . . . . 11 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝑐 𝐵) = (𝐸 𝑓))
891, 44, 2, 30, 33, 32, 35, 36, 88tgcgrcoml 25588 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐵 𝑐) = (𝐸 𝑓))
901, 2, 3, 30, 31, 32, 33, 34, 35, 36, 68, 31, 44, 33, 70, 73, 81, 89cgracgr 25924 . . . . . . . . 9 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝑎 𝑐) = (𝑑 𝑓))
9128, 29, 903jca 1122 . . . . . . . 8 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))
9291ex 397 . . . . . . 7 ((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) → ((((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))) → (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))))
9392reximdva 3165 . . . . . 6 (((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) → (∃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))) → ∃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))))
9493reximdva 3165 . . . . 5 ((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) → (∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))) → ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))))
9594imp 393 . . . 4 (((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))
961, 44, 2, 4, 8, 6, 14, 12axtgsegcon 25577 . . . . . . . 8 (𝜑 → ∃𝑎𝑃 (𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)))
971, 44, 2, 4, 8, 10, 14, 16axtgsegcon 25577 . . . . . . . 8 (𝜑 → ∃𝑐𝑃 (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)))
98 reeanv 3255 . . . . . . . 8 (∃𝑎𝑃𝑐𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ↔ (∃𝑎𝑃 (𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ ∃𝑐𝑃 (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))))
9996, 97, 98sylanbrc 572 . . . . . . 7 (𝜑 → ∃𝑎𝑃𝑐𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))))
1001, 44, 2, 4, 14, 12, 8, 6axtgsegcon 25577 . . . . . . . 8 (𝜑 → ∃𝑑𝑃 (𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)))
1011, 44, 2, 4, 14, 16, 8, 10axtgsegcon 25577 . . . . . . . 8 (𝜑 → ∃𝑓𝑃 (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))
102 reeanv 3255 . . . . . . . 8 (∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ↔ (∃𝑑𝑃 (𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ ∃𝑓𝑃 (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))
103100, 101, 102sylanbrc 572 . . . . . . 7 (𝜑 → ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))
10499, 103jca 501 . . . . . 6 (𝜑 → (∃𝑎𝑃𝑐𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
105 r19.41vv 3239 . . . . . . . . 9 (∃𝑑𝑃𝑓𝑃 (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)))) ↔ (∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)))))
106 ancom 448 . . . . . . . . . 10 ((((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)))) ↔ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
1071062rexbii 3190 . . . . . . . . 9 (∃𝑑𝑃𝑓𝑃 (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)))) ↔ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
108 ancom 448 . . . . . . . . 9 ((∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)))) ↔ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
109105, 107, 1083bitr3i 290 . . . . . . . 8 (∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))) ↔ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
1101092rexbii 3190 . . . . . . 7 (∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))) ↔ ∃𝑎𝑃𝑐𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
111 r19.41vv 3239 . . . . . . 7 (∃𝑎𝑃𝑐𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))) ↔ (∃𝑎𝑃𝑐𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
112110, 111bitr2i 265 . . . . . 6 ((∃𝑎𝑃𝑐𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))) ↔ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
113104, 112sylib 208 . . . . 5 (𝜑 → ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
114113adantr 466 . . . 4 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
11595, 114reximddv2 3168 . . 3 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))
11622, 27, 1153jca 1122 . 2 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))))
117 df-3an 1073 . . 3 (((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))) ↔ (((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸)) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))))
1184ad6antr 720 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐺 ∈ TarskiG)
11912ad6antr 720 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐷𝑃)
12014ad6antr 720 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐸𝑃)
12116ad6antr 720 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐹𝑃)
1226ad6antr 720 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐴𝑃)
1238ad6antr 720 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐵𝑃)
12410ad6antr 720 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐶𝑃)
125 simp-4r 770 . . . . . . . . . 10 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝑦𝑃)
126 simp-5r 774 . . . . . . . . . . 11 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝑥𝑃)
127 simpllr 760 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝑧𝑃)
128 simplr 752 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝑡𝑃)
129 eqid 2771 . . . . . . . . . . . . . 14 (cgrG‘𝐺) = (cgrG‘𝐺)
130 simpr1 1233 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))))
131130simplld 751 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐴 ∈ (𝐵𝐼𝑥))
132 simpr2 1235 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))))
133132simplld 751 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐷 ∈ (𝐸𝐼𝑧))
1341, 44, 2, 118, 120, 119, 127, 133tgbtwncom 25597 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐷 ∈ (𝑧𝐼𝐸))
135132simplrd 753 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐷 𝑧) = (𝐵 𝐴))
136135eqcomd 2777 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐵 𝐴) = (𝐷 𝑧))
1371, 44, 2, 118, 123, 122, 119, 127, 136tgcgrcomr 25587 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐵 𝐴) = (𝑧 𝐷))
138130simplrd 753 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐴 𝑥) = (𝐸 𝐷))
1391, 44, 2, 118, 122, 126, 120, 119, 138tgcgrcomr 25587 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐴 𝑥) = (𝐷 𝐸))
1401, 44, 2, 118, 123, 122, 126, 127, 119, 120, 131, 134, 137, 139tgcgrextend 25594 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐵 𝑥) = (𝑧 𝐸))
1411, 44, 2, 118, 123, 126, 127, 120, 140tgcgrcoml 25588 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝑥 𝐵) = (𝑧 𝐸))
142130simprld 755 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐶 ∈ (𝐵𝐼𝑦))
1431, 44, 2, 118, 123, 124, 125, 142tgbtwncom 25597 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐶 ∈ (𝑦𝐼𝐵))
144132simprld 755 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐹 ∈ (𝐸𝐼𝑡))
145130simprrd 757 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐶 𝑦) = (𝐸 𝐹))
1461, 44, 2, 118, 124, 125, 120, 121, 145tgcgrcoml 25588 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝑦 𝐶) = (𝐸 𝐹))
147132simprrd 757 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐹 𝑡) = (𝐵 𝐶))
148147eqcomd 2777 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐵 𝐶) = (𝐹 𝑡))
1491, 44, 2, 118, 123, 124, 121, 128, 148tgcgrcoml 25588 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐶 𝐵) = (𝐹 𝑡))
1501, 44, 2, 118, 125, 124, 123, 120, 121, 128, 143, 144, 146, 149tgcgrextend 25594 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝑦 𝐵) = (𝐸 𝑡))
1511, 44, 2, 118, 125, 123, 120, 128, 150tgcgrcoml 25588 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐵 𝑦) = (𝐸 𝑡))
152 simpr3 1237 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝑥 𝑦) = (𝑧 𝑡))
1531, 44, 2, 118, 126, 125, 127, 128, 152tgcgrcomlr 25589 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝑦 𝑥) = (𝑡 𝑧))
1541, 44, 129, 118, 126, 123, 125, 127, 120, 128, 141, 151, 153trgcgr 25625 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ⟨“𝑥𝐵𝑦”⟩(cgrG‘𝐺)⟨“𝑧𝐸𝑡”⟩)
155 simp-6r 778 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸)))
156155simprld 755 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐷𝐸)
1571, 44, 2, 118, 120, 119, 127, 133, 156tgbtwnne 25599 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐸𝑧)
1581, 2, 3, 120, 127, 119, 118, 123, 133, 157, 156btwnhl1 25721 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐷((hlG‘𝐺)‘𝐸)𝑧)
1591, 2, 3, 119, 127, 120, 118, 158hlcomd 25713 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝑧((hlG‘𝐺)‘𝐸)𝐷)
160155simprrd 757 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐹𝐸)
1611, 44, 2, 118, 120, 121, 128, 144, 160tgbtwnne 25599 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐸𝑡)
1621, 2, 3, 120, 128, 121, 118, 123, 144, 161, 160btwnhl1 25721 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐹((hlG‘𝐺)‘𝐸)𝑡)
1631, 2, 3, 121, 128, 120, 118, 162hlcomd 25713 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝑡((hlG‘𝐺)‘𝐸)𝐹)
1641, 2, 3, 118, 126, 123, 125, 119, 120, 121, 127, 128, 154, 159, 163iscgrad 25917 . . . . . . . . . . . 12 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ⟨“𝑥𝐵𝑦”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
1651, 2, 118, 3, 126, 123, 125, 119, 120, 121, 164cgracom 25928 . . . . . . . . . . 11 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝑥𝐵𝑦”⟩)
166155simplld 751 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐴𝐵)
1671, 44, 2, 118, 123, 122, 126, 131, 166tgbtwnne 25599 . . . . . . . . . . . 12 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐵𝑥)
1681, 2, 3, 123, 126, 122, 118, 122, 131, 167, 166btwnhl1 25721 . . . . . . . . . . 11 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐴((hlG‘𝐺)‘𝐵)𝑥)
1691, 2, 3, 118, 119, 120, 121, 126, 123, 125, 165, 122, 168cgrahl1 25922 . . . . . . . . . 10 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝐴𝐵𝑦”⟩)
170155simplrd 753 . . . . . . . . . . . 12 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐶𝐵)
1711, 44, 2, 118, 123, 124, 125, 142, 170tgbtwnne 25599 . . . . . . . . . . 11 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐵𝑦)
1721, 2, 3, 123, 125, 124, 118, 122, 142, 171, 170btwnhl1 25721 . . . . . . . . . 10 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐶((hlG‘𝐺)‘𝐵)𝑦)
1731, 2, 3, 118, 119, 120, 121, 122, 123, 125, 169, 124, 172cgrahl2 25923 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝐴𝐵𝐶”⟩)
1741, 2, 118, 3, 119, 120, 121, 122, 123, 124, 173cgracom 25928 . . . . . . . 8 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
175174adantl3r 744 . . . . . . 7 ((((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓))) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
176 simpr 471 . . . . . . . 8 (((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓))) → ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓)))
177 eqidd 2772 . . . . . . . . . . . . 13 (𝑑 = 𝑧𝐷 = 𝐷)
178 oveq2 6799 . . . . . . . . . . . . 13 (𝑑 = 𝑧 → (𝐸𝐼𝑑) = (𝐸𝐼𝑧))
179177, 178eleq12d 2844 . . . . . . . . . . . 12 (𝑑 = 𝑧 → (𝐷 ∈ (𝐸𝐼𝑑) ↔ 𝐷 ∈ (𝐸𝐼𝑧)))
180 oveq2 6799 . . . . . . . . . . . . 13 (𝑑 = 𝑧 → (𝐷 𝑑) = (𝐷 𝑧))
181 eqidd 2772 . . . . . . . . . . . . 13 (𝑑 = 𝑧 → (𝐵 𝐴) = (𝐵 𝐴))
182180, 181eqeq12d 2786 . . . . . . . . . . . 12 (𝑑 = 𝑧 → ((𝐷 𝑑) = (𝐵 𝐴) ↔ (𝐷 𝑧) = (𝐵 𝐴)))
183179, 182anbi12d 616 . . . . . . . . . . 11 (𝑑 = 𝑧 → ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ↔ (𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴))))
184 biidd 252 . . . . . . . . . . 11 (𝑑 = 𝑧 → ((𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)) ↔ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))
185183, 184anbi12d 616 . . . . . . . . . 10 (𝑑 = 𝑧 → (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ↔ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
186 eqidd 2772 . . . . . . . . . . 11 (𝑑 = 𝑧 → (𝑥 𝑦) = (𝑥 𝑦))
187 oveq1 6798 . . . . . . . . . . 11 (𝑑 = 𝑧 → (𝑑 𝑓) = (𝑧 𝑓))
188186, 187eqeq12d 2786 . . . . . . . . . 10 (𝑑 = 𝑧 → ((𝑥 𝑦) = (𝑑 𝑓) ↔ (𝑥 𝑦) = (𝑧 𝑓)))
189185, 1883anbi23d 1550 . . . . . . . . 9 (𝑑 = 𝑧 → ((((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓)) ↔ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑓))))
190 biidd 252 . . . . . . . . . . 11 (𝑓 = 𝑡 → ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ↔ (𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴))))
191 eqidd 2772 . . . . . . . . . . . . 13 (𝑓 = 𝑡𝐹 = 𝐹)
192 oveq2 6799 . . . . . . . . . . . . 13 (𝑓 = 𝑡 → (𝐸𝐼𝑓) = (𝐸𝐼𝑡))
193191, 192eleq12d 2844 . . . . . . . . . . . 12 (𝑓 = 𝑡 → (𝐹 ∈ (𝐸𝐼𝑓) ↔ 𝐹 ∈ (𝐸𝐼𝑡)))
194 oveq2 6799 . . . . . . . . . . . . 13 (𝑓 = 𝑡 → (𝐹 𝑓) = (𝐹 𝑡))
195 eqidd 2772 . . . . . . . . . . . . 13 (𝑓 = 𝑡 → (𝐵 𝐶) = (𝐵 𝐶))
196194, 195eqeq12d 2786 . . . . . . . . . . . 12 (𝑓 = 𝑡 → ((𝐹 𝑓) = (𝐵 𝐶) ↔ (𝐹 𝑡) = (𝐵 𝐶)))
197193, 196anbi12d 616 . . . . . . . . . . 11 (𝑓 = 𝑡 → ((𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)) ↔ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))))
198190, 197anbi12d 616 . . . . . . . . . 10 (𝑓 = 𝑡 → (((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ↔ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶)))))
199 eqidd 2772 . . . . . . . . . . 11 (𝑓 = 𝑡 → (𝑥 𝑦) = (𝑥 𝑦))
200 oveq2 6799 . . . . . . . . . . 11 (𝑓 = 𝑡 → (𝑧 𝑓) = (𝑧 𝑡))
201199, 200eqeq12d 2786 . . . . . . . . . 10 (𝑓 = 𝑡 → ((𝑥 𝑦) = (𝑧 𝑓) ↔ (𝑥 𝑦) = (𝑧 𝑡)))
202198, 2013anbi23d 1550 . . . . . . . . 9 (𝑓 = 𝑡 → ((((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑓)) ↔ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))))
203189, 202cbvrex2v 3329 . . . . . . . 8 (∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓)) ↔ ∃𝑧𝑃𝑡𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡)))
204176, 203sylib 208 . . . . . . 7 (((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓))) → ∃𝑧𝑃𝑡𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡)))
205175, 204r19.29vva 3229 . . . . . 6 (((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
206205adantl3r 744 . . . . 5 ((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
207 simpr 471 . . . . . 6 (((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))) → ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))
208 eqidd 2772 . . . . . . . . . . . 12 (𝑎 = 𝑥𝐴 = 𝐴)
209 oveq2 6799 . . . . . . . . . . . 12 (𝑎 = 𝑥 → (𝐵𝐼𝑎) = (𝐵𝐼𝑥))
210208, 209eleq12d 2844 . . . . . . . . . . 11 (𝑎 = 𝑥 → (𝐴 ∈ (𝐵𝐼𝑎) ↔ 𝐴 ∈ (𝐵𝐼𝑥)))
211 oveq2 6799 . . . . . . . . . . . 12 (𝑎 = 𝑥 → (𝐴 𝑎) = (𝐴 𝑥))
212 eqidd 2772 . . . . . . . . . . . 12 (𝑎 = 𝑥 → (𝐸 𝐷) = (𝐸 𝐷))
213211, 212eqeq12d 2786 . . . . . . . . . . 11 (𝑎 = 𝑥 → ((𝐴 𝑎) = (𝐸 𝐷) ↔ (𝐴 𝑥) = (𝐸 𝐷)))
214210, 213anbi12d 616 . . . . . . . . . 10 (𝑎 = 𝑥 → ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ↔ (𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷))))
215 biidd 252 . . . . . . . . . 10 (𝑎 = 𝑥 → ((𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)) ↔ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))))
216214, 215anbi12d 616 . . . . . . . . 9 (𝑎 = 𝑥 → (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ↔ ((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)))))
217 oveq1 6798 . . . . . . . . . 10 (𝑎 = 𝑥 → (𝑎 𝑐) = (𝑥 𝑐))
218 eqidd 2772 . . . . . . . . . 10 (𝑎 = 𝑥 → (𝑑 𝑓) = (𝑑 𝑓))
219217, 218eqeq12d 2786 . . . . . . . . 9 (𝑎 = 𝑥 → ((𝑎 𝑐) = (𝑑 𝑓) ↔ (𝑥 𝑐) = (𝑑 𝑓)))
220216, 2193anbi13d 1549 . . . . . . . 8 (𝑎 = 𝑥 → ((((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)) ↔ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑐) = (𝑑 𝑓))))
2212202rexbidv 3205 . . . . . . 7 (𝑎 = 𝑥 → (∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)) ↔ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑐) = (𝑑 𝑓))))
222 biidd 252 . . . . . . . . . 10 (𝑐 = 𝑦 → ((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ↔ (𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷))))
223 eqidd 2772 . . . . . . . . . . . 12 (𝑐 = 𝑦𝐶 = 𝐶)
224 oveq2 6799 . . . . . . . . . . . 12 (𝑐 = 𝑦 → (𝐵𝐼𝑐) = (𝐵𝐼𝑦))
225223, 224eleq12d 2844 . . . . . . . . . . 11 (𝑐 = 𝑦 → (𝐶 ∈ (𝐵𝐼𝑐) ↔ 𝐶 ∈ (𝐵𝐼𝑦)))
226 oveq2 6799 . . . . . . . . . . . 12 (𝑐 = 𝑦 → (𝐶 𝑐) = (𝐶 𝑦))
227 eqidd 2772 . . . . . . . . . . . 12 (𝑐 = 𝑦 → (𝐸 𝐹) = (𝐸 𝐹))
228226, 227eqeq12d 2786 . . . . . . . . . . 11 (𝑐 = 𝑦 → ((𝐶 𝑐) = (𝐸 𝐹) ↔ (𝐶 𝑦) = (𝐸 𝐹)))
229225, 228anbi12d 616 . . . . . . . . . 10 (𝑐 = 𝑦 → ((𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)) ↔ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))))
230222, 229anbi12d 616 . . . . . . . . 9 (𝑐 = 𝑦 → (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ↔ ((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹)))))
231 oveq2 6799 . . . . . . . . . 10 (𝑐 = 𝑦 → (𝑥 𝑐) = (𝑥 𝑦))
232 eqidd 2772 . . . . . . . . . 10 (𝑐 = 𝑦 → (𝑑 𝑓) = (𝑑 𝑓))
233231, 232eqeq12d 2786 . . . . . . . . 9 (𝑐 = 𝑦 → ((𝑥 𝑐) = (𝑑 𝑓) ↔ (𝑥 𝑦) = (𝑑 𝑓)))
234230, 2333anbi13d 1549 . . . . . . . 8 (𝑐 = 𝑦 → ((((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑐) = (𝑑 𝑓)) ↔ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓))))
2352342rexbidv 3205 . . . . . . 7 (𝑐 = 𝑦 → (∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑐) = (𝑑 𝑓)) ↔ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓))))
236221, 235cbvrex2v 3329 . . . . . 6 (∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)) ↔ ∃𝑥𝑃𝑦𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓)))
237207, 236sylib 208 . . . . 5 (((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))) → ∃𝑥𝑃𝑦𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓)))
238206, 237r19.29vva 3229 . . . 4 (((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
239238anasss 452 . . 3 ((𝜑 ∧ (((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸)) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
240117, 239sylan2b 581 . 2 ((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
241116, 240impbida 802 1 (𝜑 → (⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ↔ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wcel 2145  wne 2943  wrex 3062   class class class wbr 4786  cfv 6029  (class class class)co 6791  ⟨“cs3 13789  Basecbs 16057  distcds 16151  TarskiGcstrkg 25543  Itvcitv 25549  cgrGccgrg 25619  hlGchlg 25709  cgrAccgra 25913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7094  ax-cnex 10192  ax-resscn 10193  ax-1cn 10194  ax-icn 10195  ax-addcl 10196  ax-addrcl 10197  ax-mulcl 10198  ax-mulrcl 10199  ax-mulcom 10200  ax-addass 10201  ax-mulass 10202  ax-distr 10203  ax-i2m1 10204  ax-1ne0 10205  ax-1rid 10206  ax-rnegex 10207  ax-rrecex 10208  ax-cnre 10209  ax-pre-lttri 10210  ax-pre-lttrn 10211  ax-pre-ltadd 10212  ax-pre-mulgt0 10213
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5821  df-ord 5867  df-on 5868  df-lim 5869  df-suc 5870  df-iota 5992  df-fun 6031  df-fn 6032  df-f 6033  df-f1 6034  df-fo 6035  df-f1o 6036  df-fv 6037  df-riota 6752  df-ov 6794  df-oprab 6795  df-mpt2 6796  df-om 7211  df-1st 7313  df-2nd 7314  df-wrecs 7557  df-recs 7619  df-rdg 7657  df-1o 7711  df-oadd 7715  df-er 7894  df-map 8009  df-pm 8010  df-en 8108  df-dom 8109  df-sdom 8110  df-fin 8111  df-card 8963  df-cda 9190  df-pnf 10276  df-mnf 10277  df-xr 10278  df-ltxr 10279  df-le 10280  df-sub 10468  df-neg 10469  df-nn 11221  df-2 11279  df-3 11280  df-n0 11493  df-xnn0 11564  df-z 11578  df-uz 11887  df-fz 12527  df-fzo 12667  df-hash 13315  df-word 13488  df-concat 13490  df-s1 13491  df-s2 13795  df-s3 13796  df-trkgc 25561  df-trkgb 25562  df-trkgcb 25563  df-trkg 25566  df-cgrg 25620  df-leg 25692  df-hlg 25710  df-cgra 25914
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator