Metamath Proof Explorer


Theorem dfcgra2

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 is indeed equivalent to the textbook's definition. (Contributed by Thierry Arnoux, 2-Aug-2020)

Ref Expression
Hypotheses 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 dfcgra2 ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ∧ ∃ 𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑎 𝑐 ) = ( 𝑑 𝑓 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dfcgra2.p 𝑃 = ( Base ‘ 𝐺 )
2 dfcgra2.i 𝐼 = ( Itv ‘ 𝐺 )
3 dfcgra2.m = ( dist ‘ 𝐺 )
4 dfcgra2.g ( 𝜑𝐺 ∈ TarskiG )
5 dfcgra2.a ( 𝜑𝐴𝑃 )
6 dfcgra2.b ( 𝜑𝐵𝑃 )
7 dfcgra2.c ( 𝜑𝐶𝑃 )
8 dfcgra2.d ( 𝜑𝐷𝑃 )
9 dfcgra2.e ( 𝜑𝐸𝑃 )
10 dfcgra2.f ( 𝜑𝐹𝑃 )
11 eqid ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
12 4 adantr ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐺 ∈ TarskiG )
13 5 adantr ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐴𝑃 )
14 6 adantr ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐵𝑃 )
15 7 adantr ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐶𝑃 )
16 8 adantr ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐷𝑃 )
17 9 adantr ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐸𝑃 )
18 10 adantr ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐹𝑃 )
19 simpr ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
20 1 2 11 12 13 14 15 16 17 18 19 cgrane1 ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐴𝐵 )
21 1 2 11 12 13 14 15 16 17 18 19 cgrane2 ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐵𝐶 )
22 21 necomd ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐶𝐵 )
23 20 22 jca ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( 𝐴𝐵𝐶𝐵 ) )
24 1 2 11 12 13 14 15 16 17 18 19 cgrane3 ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐸𝐷 )
25 24 necomd ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐷𝐸 )
26 1 2 11 12 13 14 15 16 17 18 19 cgrane4 ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐸𝐹 )
27 26 necomd ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐹𝐸 )
28 25 27 jca ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( 𝐷𝐸𝐹𝐸 ) )
29 simprl ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) )
30 simprr ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) )
31 4 ad6antr ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝐺 ∈ TarskiG )
32 simp-5r ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝑎𝑃 )
33 6 ad6antr ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝐵𝑃 )
34 simp-4r ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝑐𝑃 )
35 simpllr ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝑑𝑃 )
36 9 ad6antr ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝐸𝑃 )
37 simplr ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝑓𝑃 )
38 10 ad6antr ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝐹𝑃 )
39 8 ad6antr ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝐷𝑃 )
40 7 ad6antr ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝐶𝑃 )
41 5 ad6antr ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝐴𝑃 )
42 simp-6r ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
43 1 2 31 11 41 33 40 39 36 38 42 cgracom ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
44 29 simplld ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) )
45 20 ad5antr ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝐴𝐵 )
46 1 3 2 31 33 41 32 44 45 tgbtwnne ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝐵𝑎 )
47 1 2 11 33 32 41 31 41 44 46 45 btwnhl1 ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝐴 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝑎 )
48 1 2 11 41 32 33 31 47 hlcomd ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 )
49 1 2 11 31 39 36 38 41 33 40 43 32 48 cgrahl1 ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝐶 ”⟩ )
50 29 simprld ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) )
51 22 ad5antr ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝐶𝐵 )
52 1 3 2 31 33 40 34 50 51 tgbtwnne ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝐵𝑐 )
53 1 2 11 33 34 40 31 41 50 52 51 btwnhl1 ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝐶 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝑐 )
54 1 2 11 40 34 33 31 53 hlcomd ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 )
55 1 2 11 31 39 36 38 32 33 40 49 34 54 cgrahl2 ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ )
56 1 2 31 11 39 36 38 32 33 34 55 cgracom ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → ⟨“ 𝑎 𝐵 𝑐 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
57 30 simplld ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) )
58 25 ad5antr ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝐷𝐸 )
59 1 3 2 31 36 39 35 57 58 tgbtwnne ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝐸𝑑 )
60 1 2 11 36 35 39 31 41 57 59 58 btwnhl1 ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝐷 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝑑 )
61 1 2 11 39 35 36 31 60 hlcomd ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 )
62 1 2 11 31 32 33 34 39 36 38 56 35 61 cgrahl1 ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → ⟨“ 𝑎 𝐵 𝑐 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝐹 ”⟩ )
63 30 simprld ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) )
64 27 ad5antr ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝐹𝐸 )
65 1 3 2 31 36 38 37 63 64 tgbtwnne ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝐸𝑓 )
66 1 2 11 36 37 38 31 41 63 65 64 btwnhl1 ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝐹 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝑓 )
67 1 2 11 38 37 36 31 66 hlcomd ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 )
68 1 2 11 31 32 33 34 35 36 38 62 37 67 cgrahl2 ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → ⟨“ 𝑎 𝐵 𝑐 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑓 ”⟩ )
69 46 necomd ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝑎𝐵 )
70 1 2 11 32 41 33 31 69 hlid ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝑎 )
71 52 necomd ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝑐𝐵 )
72 1 2 11 34 41 33 31 71 hlid ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝑐 )
73 1 3 2 31 33 41 32 44 tgbtwncom ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝐴 ∈ ( 𝑎 𝐼 𝐵 ) )
74 29 simplrd ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) )
75 1 3 2 31 41 32 36 39 74 tgcgrcoml ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → ( 𝑎 𝐴 ) = ( 𝐸 𝐷 ) )
76 30 simplrd ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) )
77 76 eqcomd ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → ( 𝐵 𝐴 ) = ( 𝐷 𝑑 ) )
78 1 3 2 31 33 41 39 35 77 tgcgrcoml ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → ( 𝐴 𝐵 ) = ( 𝐷 𝑑 ) )
79 1 3 2 31 32 41 33 36 39 35 73 57 75 78 tgcgrextend ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → ( 𝑎 𝐵 ) = ( 𝐸 𝑑 ) )
80 1 3 2 31 32 33 36 35 79 tgcgrcoml ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → ( 𝐵 𝑎 ) = ( 𝐸 𝑑 ) )
81 1 3 2 31 33 40 34 50 tgbtwncom ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → 𝐶 ∈ ( 𝑐 𝐼 𝐵 ) )
82 29 simprrd ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) )
83 1 3 2 31 40 34 36 38 82 tgcgrcoml ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → ( 𝑐 𝐶 ) = ( 𝐸 𝐹 ) )
84 30 simprrd ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) )
85 84 eqcomd ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → ( 𝐵 𝐶 ) = ( 𝐹 𝑓 ) )
86 1 3 2 31 33 40 38 37 85 tgcgrcoml ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → ( 𝐶 𝐵 ) = ( 𝐹 𝑓 ) )
87 1 3 2 31 34 40 33 36 38 37 81 63 83 86 tgcgrextend ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → ( 𝑐 𝐵 ) = ( 𝐸 𝑓 ) )
88 1 3 2 31 34 33 36 37 87 tgcgrcoml ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → ( 𝐵 𝑐 ) = ( 𝐸 𝑓 ) )
89 1 2 11 31 32 33 34 35 36 37 68 32 3 34 70 72 80 88 cgracgr ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → ( 𝑎 𝑐 ) = ( 𝑑 𝑓 ) )
90 29 30 89 3jca ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑎 𝑐 ) = ( 𝑑 𝑓 ) ) )
91 90 ex ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) ∧ 𝑓𝑃 ) → ( ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) → ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑎 𝑐 ) = ( 𝑑 𝑓 ) ) ) )
92 91 reximdva ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ 𝑑𝑃 ) → ( ∃ 𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) → ∃ 𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑎 𝑐 ) = ( 𝑑 𝑓 ) ) ) )
93 92 reximdva ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) → ( ∃ 𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) → ∃ 𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑎 𝑐 ) = ( 𝑑 𝑓 ) ) ) )
94 93 imp ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎𝑃 ) ∧ 𝑐𝑃 ) ∧ ∃ 𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ) → ∃ 𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑎 𝑐 ) = ( 𝑑 𝑓 ) ) )
95 1 3 2 4 6 5 9 8 axtgsegcon ( 𝜑 → ∃ 𝑎𝑃 ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) )
96 1 3 2 4 6 7 9 10 axtgsegcon ( 𝜑 → ∃ 𝑐𝑃 ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) )
97 reeanv ( ∃ 𝑎𝑃𝑐𝑃 ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ↔ ( ∃ 𝑎𝑃 ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ∃ 𝑐𝑃 ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) )
98 95 96 97 sylanbrc ( 𝜑 → ∃ 𝑎𝑃𝑐𝑃 ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) )
99 1 3 2 4 9 8 6 5 axtgsegcon ( 𝜑 → ∃ 𝑑𝑃 ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) )
100 1 3 2 4 9 10 6 7 axtgsegcon ( 𝜑 → ∃ 𝑓𝑃 ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) )
101 reeanv ( ∃ 𝑑𝑃𝑓𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ↔ ( ∃ 𝑑𝑃 ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ∃ 𝑓𝑃 ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) )
102 99 100 101 sylanbrc ( 𝜑 → ∃ 𝑑𝑃𝑓𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) )
103 98 102 jca ( 𝜑 → ( ∃ 𝑎𝑃𝑐𝑃 ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ∃ 𝑑𝑃𝑓𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) )
104 r19.41vv ( ∃ 𝑑𝑃𝑓𝑃 ( ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ) ↔ ( ∃ 𝑑𝑃𝑓𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ) )
105 ancom ( ( ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ) ↔ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) )
106 105 2rexbii ( ∃ 𝑑𝑃𝑓𝑃 ( ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ) ↔ ∃ 𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) )
107 ancom ( ( ∃ 𝑑𝑃𝑓𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ) ↔ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ∃ 𝑑𝑃𝑓𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) )
108 104 106 107 3bitr3i ( ∃ 𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ↔ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ∃ 𝑑𝑃𝑓𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) )
109 108 2rexbii ( ∃ 𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ↔ ∃ 𝑎𝑃𝑐𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ∃ 𝑑𝑃𝑓𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) )
110 r19.41vv ( ∃ 𝑎𝑃𝑐𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ∃ 𝑑𝑃𝑓𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ↔ ( ∃ 𝑎𝑃𝑐𝑃 ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ∃ 𝑑𝑃𝑓𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) )
111 109 110 bitr2i ( ( ∃ 𝑎𝑃𝑐𝑃 ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ∃ 𝑑𝑃𝑓𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) ↔ ∃ 𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) )
112 103 111 sylib ( 𝜑 → ∃ 𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) )
113 112 adantr ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ∃ 𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) )
114 94 113 reximddv2 ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ∃ 𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑎 𝑐 ) = ( 𝑑 𝑓 ) ) )
115 23 28 114 3jca ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ∧ ∃ 𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑎 𝑐 ) = ( 𝑑 𝑓 ) ) ) )
116 df-3an ( ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ∧ ∃ 𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑎 𝑐 ) = ( 𝑑 𝑓 ) ) ) ↔ ( ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ∧ ∃ 𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑎 𝑐 ) = ( 𝑑 𝑓 ) ) ) )
117 4 ad6antr ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝐺 ∈ TarskiG )
118 8 ad6antr ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝐷𝑃 )
119 9 ad6antr ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝐸𝑃 )
120 10 ad6antr ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝐹𝑃 )
121 5 ad6antr ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝐴𝑃 )
122 6 ad6antr ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝐵𝑃 )
123 7 ad6antr ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝐶𝑃 )
124 simp-4r ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝑦𝑃 )
125 simp-5r ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝑥𝑃 )
126 simpllr ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝑧𝑃 )
127 simplr ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝑡𝑃 )
128 eqid ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
129 simpr1 ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) )
130 129 simplld ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) )
131 simpr2 ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) )
132 131 simplld ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) )
133 1 3 2 117 119 118 126 132 tgbtwncom ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝐷 ∈ ( 𝑧 𝐼 𝐸 ) )
134 131 simplrd ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) )
135 134 eqcomd ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → ( 𝐵 𝐴 ) = ( 𝐷 𝑧 ) )
136 1 3 2 117 122 121 118 126 135 tgcgrcomr ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → ( 𝐵 𝐴 ) = ( 𝑧 𝐷 ) )
137 129 simplrd ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) )
138 1 3 2 117 121 125 119 118 137 tgcgrcomr ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → ( 𝐴 𝑥 ) = ( 𝐷 𝐸 ) )
139 1 3 2 117 122 121 125 126 118 119 130 133 136 138 tgcgrextend ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → ( 𝐵 𝑥 ) = ( 𝑧 𝐸 ) )
140 1 3 2 117 122 125 126 119 139 tgcgrcoml ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → ( 𝑥 𝐵 ) = ( 𝑧 𝐸 ) )
141 129 simprld ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) )
142 1 3 2 117 122 123 124 141 tgbtwncom ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝐶 ∈ ( 𝑦 𝐼 𝐵 ) )
143 131 simprld ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) )
144 129 simprrd ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) )
145 1 3 2 117 123 124 119 120 144 tgcgrcoml ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → ( 𝑦 𝐶 ) = ( 𝐸 𝐹 ) )
146 131 simprrd ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) )
147 146 eqcomd ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → ( 𝐵 𝐶 ) = ( 𝐹 𝑡 ) )
148 1 3 2 117 122 123 120 127 147 tgcgrcoml ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → ( 𝐶 𝐵 ) = ( 𝐹 𝑡 ) )
149 1 3 2 117 124 123 122 119 120 127 142 143 145 148 tgcgrextend ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → ( 𝑦 𝐵 ) = ( 𝐸 𝑡 ) )
150 1 3 2 117 124 122 119 127 149 tgcgrcoml ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → ( 𝐵 𝑦 ) = ( 𝐸 𝑡 ) )
151 simpr3 ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) )
152 1 3 2 117 125 124 126 127 151 tgcgrcomlr ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → ( 𝑦 𝑥 ) = ( 𝑡 𝑧 ) )
153 1 3 128 117 125 122 124 126 119 127 140 150 152 trgcgr ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → ⟨“ 𝑥 𝐵 𝑦 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑧 𝐸 𝑡 ”⟩ )
154 simp-6r ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) )
155 154 simprld ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝐷𝐸 )
156 1 3 2 117 119 118 126 132 155 tgbtwnne ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝐸𝑧 )
157 1 2 11 119 126 118 117 122 132 156 155 btwnhl1 ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝐷 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝑧 )
158 1 2 11 118 126 119 117 157 hlcomd ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 )
159 154 simprrd ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝐹𝐸 )
160 1 3 2 117 119 120 127 143 159 tgbtwnne ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝐸𝑡 )
161 1 2 11 119 127 120 117 122 143 160 159 btwnhl1 ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝐹 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝑡 )
162 1 2 11 120 127 119 117 161 hlcomd ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 )
163 1 2 11 117 125 122 124 118 119 120 126 127 153 158 162 iscgrad ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → ⟨“ 𝑥 𝐵 𝑦 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
164 1 2 117 11 125 122 124 118 119 120 163 cgracom ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑥 𝐵 𝑦 ”⟩ )
165 154 simplld ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝐴𝐵 )
166 1 3 2 117 122 121 125 130 165 tgbtwnne ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝐵𝑥 )
167 1 2 11 122 125 121 117 121 130 166 165 btwnhl1 ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝐴 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝑥 )
168 1 2 11 117 118 119 120 125 122 124 164 121 167 cgrahl1 ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝑦 ”⟩ )
169 154 simplrd ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝐶𝐵 )
170 1 3 2 117 122 123 124 141 169 tgbtwnne ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝐵𝑦 )
171 1 2 11 122 124 123 117 121 141 170 169 btwnhl1 ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → 𝐶 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝑦 )
172 1 2 11 117 118 119 120 121 122 124 168 123 171 cgrahl2 ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
173 1 2 117 11 118 119 120 121 122 123 172 cgracom ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
174 173 adantl3r ( ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ∃ 𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑑 𝑓 ) ) ) ∧ 𝑧𝑃 ) ∧ 𝑡𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
175 simpr ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ∃ 𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑑 𝑓 ) ) ) → ∃ 𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑑 𝑓 ) ) )
176 oveq2 ( 𝑑 = 𝑧 → ( 𝐸 𝐼 𝑑 ) = ( 𝐸 𝐼 𝑧 ) )
177 176 eleq2d ( 𝑑 = 𝑧 → ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ↔ 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ) )
178 oveq2 ( 𝑑 = 𝑧 → ( 𝐷 𝑑 ) = ( 𝐷 𝑧 ) )
179 178 eqeq1d ( 𝑑 = 𝑧 → ( ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ↔ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) )
180 177 179 anbi12d ( 𝑑 = 𝑧 → ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ↔ ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ) )
181 180 anbi1d ( 𝑑 = 𝑧 → ( ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ↔ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ) )
182 oveq1 ( 𝑑 = 𝑧 → ( 𝑑 𝑓 ) = ( 𝑧 𝑓 ) )
183 182 eqeq2d ( 𝑑 = 𝑧 → ( ( 𝑥 𝑦 ) = ( 𝑑 𝑓 ) ↔ ( 𝑥 𝑦 ) = ( 𝑧 𝑓 ) ) )
184 181 183 3anbi23d ( 𝑑 = 𝑧 → ( ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑑 𝑓 ) ) ↔ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑓 ) ) ) )
185 oveq2 ( 𝑓 = 𝑡 → ( 𝐸 𝐼 𝑓 ) = ( 𝐸 𝐼 𝑡 ) )
186 185 eleq2d ( 𝑓 = 𝑡 → ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ↔ 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ) )
187 oveq2 ( 𝑓 = 𝑡 → ( 𝐹 𝑓 ) = ( 𝐹 𝑡 ) )
188 187 eqeq1d ( 𝑓 = 𝑡 → ( ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ↔ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) )
189 186 188 anbi12d ( 𝑓 = 𝑡 → ( ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ↔ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) )
190 189 anbi2d ( 𝑓 = 𝑡 → ( ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ↔ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ) )
191 oveq2 ( 𝑓 = 𝑡 → ( 𝑧 𝑓 ) = ( 𝑧 𝑡 ) )
192 191 eqeq2d ( 𝑓 = 𝑡 → ( ( 𝑥 𝑦 ) = ( 𝑧 𝑓 ) ↔ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) )
193 190 192 3anbi23d ( 𝑓 = 𝑡 → ( ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑓 ) ) ↔ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) ) )
194 184 193 cbvrex2vw ( ∃ 𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑑 𝑓 ) ) ↔ ∃ 𝑧𝑃𝑡𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) )
195 175 194 sylib ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ∃ 𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑑 𝑓 ) ) ) → ∃ 𝑧𝑃𝑡𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 𝑧 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 𝑡 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑧 𝑡 ) ) )
196 174 195 r19.29vva ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ∃ 𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑑 𝑓 ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
197 196 adantl3r ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ ∃ 𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑎 𝑐 ) = ( 𝑑 𝑓 ) ) ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ∃ 𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑑 𝑓 ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
198 simpr ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ ∃ 𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑎 𝑐 ) = ( 𝑑 𝑓 ) ) ) → ∃ 𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑎 𝑐 ) = ( 𝑑 𝑓 ) ) )
199 oveq2 ( 𝑎 = 𝑥 → ( 𝐵 𝐼 𝑎 ) = ( 𝐵 𝐼 𝑥 ) )
200 199 eleq2d ( 𝑎 = 𝑥 → ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ↔ 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ) )
201 oveq2 ( 𝑎 = 𝑥 → ( 𝐴 𝑎 ) = ( 𝐴 𝑥 ) )
202 201 eqeq1d ( 𝑎 = 𝑥 → ( ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ↔ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) )
203 200 202 anbi12d ( 𝑎 = 𝑥 → ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ↔ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ) )
204 203 anbi1d ( 𝑎 = 𝑥 → ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ↔ ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ) )
205 oveq1 ( 𝑎 = 𝑥 → ( 𝑎 𝑐 ) = ( 𝑥 𝑐 ) )
206 205 eqeq1d ( 𝑎 = 𝑥 → ( ( 𝑎 𝑐 ) = ( 𝑑 𝑓 ) ↔ ( 𝑥 𝑐 ) = ( 𝑑 𝑓 ) ) )
207 204 206 3anbi13d ( 𝑎 = 𝑥 → ( ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑎 𝑐 ) = ( 𝑑 𝑓 ) ) ↔ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑐 ) = ( 𝑑 𝑓 ) ) ) )
208 207 2rexbidv ( 𝑎 = 𝑥 → ( ∃ 𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑎 𝑐 ) = ( 𝑑 𝑓 ) ) ↔ ∃ 𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑐 ) = ( 𝑑 𝑓 ) ) ) )
209 oveq2 ( 𝑐 = 𝑦 → ( 𝐵 𝐼 𝑐 ) = ( 𝐵 𝐼 𝑦 ) )
210 209 eleq2d ( 𝑐 = 𝑦 → ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ↔ 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ) )
211 oveq2 ( 𝑐 = 𝑦 → ( 𝐶 𝑐 ) = ( 𝐶 𝑦 ) )
212 211 eqeq1d ( 𝑐 = 𝑦 → ( ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ↔ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) )
213 210 212 anbi12d ( 𝑐 = 𝑦 → ( ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ↔ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) )
214 213 anbi2d ( 𝑐 = 𝑦 → ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ↔ ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ) )
215 oveq2 ( 𝑐 = 𝑦 → ( 𝑥 𝑐 ) = ( 𝑥 𝑦 ) )
216 215 eqeq1d ( 𝑐 = 𝑦 → ( ( 𝑥 𝑐 ) = ( 𝑑 𝑓 ) ↔ ( 𝑥 𝑦 ) = ( 𝑑 𝑓 ) ) )
217 214 216 3anbi13d ( 𝑐 = 𝑦 → ( ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑐 ) = ( 𝑑 𝑓 ) ) ↔ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑑 𝑓 ) ) ) )
218 217 2rexbidv ( 𝑐 = 𝑦 → ( ∃ 𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑐 ) = ( 𝑑 𝑓 ) ) ↔ ∃ 𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑑 𝑓 ) ) ) )
219 208 218 cbvrex2vw ( ∃ 𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑎 𝑐 ) = ( 𝑑 𝑓 ) ) ↔ ∃ 𝑥𝑃𝑦𝑃𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑑 𝑓 ) ) )
220 198 219 sylib ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ ∃ 𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑎 𝑐 ) = ( 𝑑 𝑓 ) ) ) → ∃ 𝑥𝑃𝑦𝑃𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 𝑦 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑥 𝑦 ) = ( 𝑑 𝑓 ) ) )
221 197 220 r19.29vva ( ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ) ∧ ∃ 𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑎 𝑐 ) = ( 𝑑 𝑓 ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
222 221 anasss ( ( 𝜑 ∧ ( ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ) ∧ ∃ 𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑎 𝑐 ) = ( 𝑑 𝑓 ) ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
223 116 222 sylan2b ( ( 𝜑 ∧ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ∧ ∃ 𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑎 𝑐 ) = ( 𝑑 𝑓 ) ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
224 115 223 impbida ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ( ( 𝐴𝐵𝐶𝐵 ) ∧ ( 𝐷𝐸𝐹𝐸 ) ∧ ∃ 𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 𝑎 ) = ( 𝐸 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 𝑐 ) = ( 𝐸 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 𝑑 ) = ( 𝐵 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 𝑓 ) = ( 𝐵 𝐶 ) ) ) ∧ ( 𝑎 𝑐 ) = ( 𝑑 𝑓 ) ) ) ) )