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 syl5bb ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑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 eqcomd ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑘 = 𝐾 ) → 𝑃 = 𝑝 )
50 49 oveq1d ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑘 = 𝐾 ) → ( 𝑃 ↑m ( 0 ..^ 3 ) ) = ( 𝑝 ↑m ( 0 ..^ 3 ) ) )
51 50 eleq2d ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑘 = 𝐾 ) → ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ↔ 𝑎 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ) )
52 50 eleq2d ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑘 = 𝐾 ) → ( 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ↔ 𝑏 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ) )
53 51 52 anbi12d ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑘 = 𝐾 ) → ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ↔ ( 𝑎 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ) ) )
54 simpr ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑘 = 𝐾 ) → 𝑘 = 𝐾 )
55 54 fveq1d ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑘 = 𝐾 ) → ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) = ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) )
56 55 breqd ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑘 = 𝐾 ) → ( 𝑥 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ↔ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ) )
57 55 breqd ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑘 = 𝐾 ) → ( 𝑦 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ↔ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) )
58 56 57 3anbi23d ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑘 = 𝐾 ) → ( ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ↔ ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) )
59 58 bicomd ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑘 = 𝐾 ) → ( ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ↔ ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) )
60 49 59 rexeqbidv ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑘 = 𝐾 ) → ( ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ↔ ∃ 𝑦 ∈ 𝑝 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) )
61 49 60 rexeqbidv ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑘 = 𝐾 ) → ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ↔ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) )
62 53 61 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 ) ) ) ) )
63 1 3 62 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 ) ) ) ) )
64 63 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 ) ) ) } )
65 fveq2 ⊢ ( 𝑔 = 𝐺 → ( cgrG ‘ 𝑔 ) = ( cgrG ‘ 𝐺 ) )
66 65 breqd ⊢ ( 𝑔 = 𝐺 → ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ↔ 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ) )
67 66 3anbi1d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ↔ ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) )
68 67 2rexbidv ⊢ ( 𝑔 = 𝐺 → ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) )
69 68 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 ) ) ) ) )
70 69 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 ) ) ) } )
71 64 70 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 ) ) ) } )
72 df-cgra ⊢ cgrA = ( 𝑔 ∈ V ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( hlG ‘ 𝑔 ) / 𝑘 ] ( ( 𝑎 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) } )
73 ovex ⊢ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∈ V
74 73 73 xpex ⊢ ( ( 𝑃 ↑m ( 0 ..^ 3 ) ) × ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∈ V
75 opabssxp ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) } ⊆ ( ( 𝑃 ↑m ( 0 ..^ 3 ) ) × ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
76 74 75 ssexi ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) } ∈ V
77 71 72 76 fvmpt ⊢ ( 𝐺 ∈ V → ( cgrA ‘ 𝐺 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) } )
78 4 47 77 3syl ⊢ ( 𝜑 → ( cgrA ‘ 𝐺 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) } )
79 78 breqd ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝐾 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) } ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) )
80 5 6 7 s3cld ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑃 )
81 s3len ⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3
82 1 fvexi ⊢ 𝑃 ∈ V
83 3nn0 ⊢ 3 ∈ ℕ0
84 wrdmap ⊢ ( ( 𝑃 ∈ V ∧ 3 ∈ ℕ0 ) → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑃 ∧ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3 ) ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) )
85 82 83 84 mp2an ⊢ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑃 ∧ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3 ) ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
86 80 81 85 sylanblc ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
87 8 9 10 s3cld ⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ Word 𝑃 )
88 s3len ⊢ ( ♯ ‘ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) = 3
89 wrdmap ⊢ ( ( 𝑃 ∈ V ∧ 3 ∈ ℕ0 ) → ( ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ Word 𝑃 ∧ ( ♯ ‘ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) = 3 ) ↔ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) )
90 82 83 89 mp2an ⊢ ( ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ Word 𝑃 ∧ ( ♯ ‘ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) = 3 ) ↔ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
91 87 88 90 sylanblc ⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
92 86 91 jca ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) )
93 92 biantrurd ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ↔ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ) )
94 46 79 93 3bitr4d ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) )