Metamath Proof Explorer

Theorem iscgra

Description: Property for two angles ABC and DEF to be congruent. This is a modified version of the definition 11.3 of Schwabhauser p. 95. where the number of constructed points has been reduced to two. We chose this version rather than the textbook version because it is shorter and therefore simpler to work with. Theorem dfcgra2 shows that those definitions are indeed equivalent. (Contributed by Thierry Arnoux, 31-Jul-2020)

Ref Expression
Hypotheses iscgra.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
iscgra.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
iscgra.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
iscgra.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
iscgra.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
iscgra.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
iscgra.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
iscgra.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
iscgra.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
iscgra.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
Assertion iscgra ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 iscgra.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 iscgra.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 iscgra.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
4 iscgra.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 iscgra.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6 iscgra.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7 iscgra.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8 iscgra.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9 iscgra.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
10 iscgra.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
11 simpl ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
12 eqidd ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝑥 = 𝑥 )
13 simpr ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
14 13 fveq1d ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( 𝑏 ‘ 1 ) = ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) )
15 eqidd ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝑦 = 𝑦 )
16 12 14 15 s3eqd ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ = ⟨“ 𝑥 ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) 𝑦 ”⟩ )
17 11 16 breq12d ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) 𝑦 ”⟩ ) )
18 14 fveq2d ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) = ( 𝐾 ‘ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ) )
19 13 fveq1d ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( 𝑏 ‘ 0 ) = ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) )
20 12 18 19 breq123d ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ↔ 𝑥 ( 𝐾 ‘ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ) )
21 13 fveq1d ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( 𝑏 ‘ 2 ) = ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 2 ) )
22 15 18 21 breq123d ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ↔ 𝑦 ( 𝐾 ‘ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 2 ) ) )
23 17 20 22 3anbi123d ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 2 ) ) ) )
24 23 2rexbidv ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 2 ) ) ) )
25 eqid ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) }
26 24 25 brab2a ⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) } ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 2 ) ) ) )
27 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → 𝑥 = 𝑥 )
28 s3fv1 ⊢ ( 𝐸 ∈ 𝑃 → ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) = 𝐸 )
29 9 28 syl ⊢ ( 𝜑 → ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) = 𝐸 )
30 29 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) = 𝐸 )
31 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → 𝑦 = 𝑦 )
32 27 30 31 s3eqd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ⟨“ 𝑥 ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) 𝑦 ”⟩ = ⟨“ 𝑥 𝐸 𝑦 ”⟩ )
33 32 breq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) 𝑦 ”⟩ ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ) )
34 30 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( 𝐾 ‘ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ) = ( 𝐾 ‘ 𝐸 ) )
35 s3fv0 ⊢ ( 𝐷 ∈ 𝑃 → ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) = 𝐷 )
36 8 35 syl ⊢ ( 𝜑 → ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) = 𝐷 )
37 36 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) = 𝐷 )
38 27 34 37 breq123d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( 𝑥 ( 𝐾 ‘ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ↔ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ) )
39 s3fv2 ⊢ ( 𝐹 ∈ 𝑃 → ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 2 ) = 𝐹 )
40 10 39 syl ⊢ ( 𝜑 → ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 2 ) = 𝐹 )
41 40 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 2 ) = 𝐹 )
42 31 34 41 breq123d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( 𝑦 ( 𝐾 ‘ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 2 ) ↔ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) )
43 33 38 42 3anbi123d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 2 ) ) ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) )
44 43 2rexbidva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 2 ) ) ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) )
45 44 anbi2d ⊢ ( 𝜑 → ( ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 2 ) ) ) ↔ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ) )
46 26 45 bitrid ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) } ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ) )
47 elex ⊢ ( 𝐺 ∈ TarskiG → 𝐺 ∈ V )
48 simpl ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑘 = 𝐾 ) → 𝑝 = 𝑃 )
49 48 oveq1d ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑘 = 𝐾 ) → ( 𝑝 ↑m ( 0 ..^ 3 ) ) = ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
50 49 eleq2d ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑘 = 𝐾 ) → ( 𝑎 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ↔ 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) )
51 49 eleq2d ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑘 = 𝐾 ) → ( 𝑏 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ↔ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) )
52 50 51 anbi12d ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑘 = 𝐾 ) → ( ( 𝑎 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ) ↔ ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ) )
53 simpr ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑘 = 𝐾 ) → 𝑘 = 𝐾 )
54 53 fveq1d ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑘 = 𝐾 ) → ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) = ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) )
55 54 breqd ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑘 = 𝐾 ) → ( 𝑥 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ↔ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ) )
56 54 breqd ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑘 = 𝐾 ) → ( 𝑦 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ↔ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) )
57 55 56 3anbi23d ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑘 = 𝐾 ) → ( ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ↔ ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) )
58 48 57 rexeqbidv ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑘 = 𝐾 ) → ( ∃ 𝑦 ∈ 𝑝 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ↔ ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) )
59 48 58 rexeqbidv ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑘 = 𝐾 ) → ( ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) )
60 52 59 anbi12d ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑘 = 𝐾 ) → ( ( ( 𝑎 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) ↔ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) ) )
61 1 3 60 sbcie2s ⊢ ( 𝑔 = 𝐺 → ( [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( hlG ‘ 𝑔 ) / 𝑘 ] ( ( 𝑎 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) ↔ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) ) )
62 61 opabbidv ⊢ ( 𝑔 = 𝐺 → { ⟨ 𝑎 , 𝑏 ⟩ ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( hlG ‘ 𝑔 ) / 𝑘 ] ( ( 𝑎 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) } )
63 fveq2 ⊢ ( 𝑔 = 𝐺 → ( cgrG ‘ 𝑔 ) = ( cgrG ‘ 𝐺 ) )
64 63 breqd ⊢ ( 𝑔 = 𝐺 → ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ↔ 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ) )
65 64 3anbi1d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ↔ ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) )
66 65 2rexbidv ⊢ ( 𝑔 = 𝐺 → ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) )
67 66 anbi2d ⊢ ( 𝑔 = 𝐺 → ( ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) ↔ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) ) )
68 67 opabbidv ⊢ ( 𝑔 = 𝐺 → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) } )
69 62 68 eqtrd ⊢ ( 𝑔 = 𝐺 → { ⟨ 𝑎 , 𝑏 ⟩ ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( hlG ‘ 𝑔 ) / 𝑘 ] ( ( 𝑎 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) } )
70 df-cgra ⊢ cgrA = ( 𝑔 ∈ V ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( hlG ‘ 𝑔 ) / 𝑘 ] ( ( 𝑎 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) } )
71 ovex ⊢ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∈ V
72 71 71 xpex ⊢ ( ( 𝑃 ↑m ( 0 ..^ 3 ) ) × ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∈ V
73 opabssxp ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) } ⊆ ( ( 𝑃 ↑m ( 0 ..^ 3 ) ) × ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
74 72 73 ssexi ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) } ∈ V
75 69 70 74 fvmpt ⊢ ( 𝐺 ∈ V → ( cgrA ‘ 𝐺 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) } )
76 4 47 75 3syl ⊢ ( 𝜑 → ( cgrA ‘ 𝐺 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) } )
77 76 breqd ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) } ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) )
78 5 6 7 s3cld ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑃 )
79 s3len ⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3
80 1 fvexi ⊢ 𝑃 ∈ V
81 3nn0 ⊢ 3 ∈ ℕ0
82 wrdmap ⊢ ( ( 𝑃 ∈ V ∧ 3 ∈ ℕ0 ) → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑃 ∧ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3 ) ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) )
83 80 81 82 mp2an ⊢ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑃 ∧ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3 ) ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
84 78 79 83 sylanblc ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
85 8 9 10 s3cld ⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ Word 𝑃 )
86 s3len ⊢ ( ♯ ‘ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) = 3
87 wrdmap ⊢ ( ( 𝑃 ∈ V ∧ 3 ∈ ℕ0 ) → ( ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ Word 𝑃 ∧ ( ♯ ‘ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) = 3 ) ↔ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) )
88 80 81 87 mp2an ⊢ ( ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ Word 𝑃 ∧ ( ♯ ‘ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) = 3 ) ↔ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
89 85 86 88 sylanblc ⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
90 84 89 jca ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) )
91 90 biantrurd ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ↔ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ) )
92 46 77 91 3bitr4d ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) )