Metamath Proof Explorer

Theorem cgrabasimass

Description: The angle congruence relation is hereditary. (Contributed by Thierry Arnoux, 31-Aug-2026)

Ref Expression
Hypotheses cgraer.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
cgraer.a ⊢ 𝐴 = { 𝑑 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) }
cgraer.c ⊢ ∼ = ( cgrA ‘ 𝐺 )
cgraer.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
Assertion cgrabasimass ( 𝜑 → ( ∼ “ 𝐴 ) ⊆ 𝐴 )

Proof

Step Hyp Ref Expression
1 cgraer.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 cgraer.a ⊢ 𝐴 = { 𝑑 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) }
3 cgraer.c ⊢ ∼ = ( cgrA ‘ 𝐺 )
4 cgraer.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 fveq1 ⊢ ( 𝑑 = 𝑒 → ( 𝑑 ‘ 0 ) = ( 𝑒 ‘ 0 ) )
6 fveq1 ⊢ ( 𝑑 = 𝑒 → ( 𝑑 ‘ 1 ) = ( 𝑒 ‘ 1 ) )
7 5 6 neeq12d ⊢ ( 𝑑 = 𝑒 → ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ↔ ( 𝑒 ‘ 0 ) ≠ ( 𝑒 ‘ 1 ) ) )
8 fveq1 ⊢ ( 𝑑 = 𝑒 → ( 𝑑 ‘ 2 ) = ( 𝑒 ‘ 2 ) )
9 6 8 neeq12d ⊢ ( 𝑑 = 𝑒 → ( ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ↔ ( 𝑒 ‘ 1 ) ≠ ( 𝑒 ‘ 2 ) ) )
10 7 9 anbi12d ⊢ ( 𝑑 = 𝑒 → ( ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) ↔ ( ( 𝑒 ‘ 0 ) ≠ ( 𝑒 ‘ 1 ) ∧ ( 𝑒 ‘ 1 ) ≠ ( 𝑒 ‘ 2 ) ) ) )
11 imassrn ⊢ ( ∼ “ 𝐴 ) ⊆ ran ∼
12 df-cgra ⊢ cgrA = ( 𝑔 ∈ V ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( hlG ‘ 𝑔 ) / 𝑘 ] ( ( 𝑎 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) } )
13 fvexd ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) ∈ V )
14 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
15 14 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = 𝑃 )
16 fvexd ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) → ( hlG ‘ 𝑔 ) ∈ V )
17 fveq2 ⊢ ( 𝑔 = 𝐺 → ( hlG ‘ 𝑔 ) = ( hlG ‘ 𝐺 ) )
18 17 adantr ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) → ( hlG ‘ 𝑔 ) = ( hlG ‘ 𝐺 ) )
19 oveq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ↑m ( 0 ..^ 3 ) ) = ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
20 19 ad2antlr ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑘 = ( hlG ‘ 𝐺 ) ) → ( 𝑝 ↑m ( 0 ..^ 3 ) ) = ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
21 20 eleq2d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑘 = ( hlG ‘ 𝐺 ) ) → ( 𝑎 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ↔ 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) )
22 20 eleq2d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑘 = ( hlG ‘ 𝐺 ) ) → ( 𝑏 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ↔ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) )
23 21 22 anbi12d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑘 = ( hlG ‘ 𝐺 ) ) → ( ( 𝑎 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ) ↔ ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ) )
24 simplr ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑘 = ( hlG ‘ 𝐺 ) ) → 𝑝 = 𝑃 )
25 fveq2 ⊢ ( 𝑔 = 𝐺 → ( cgrG ‘ 𝑔 ) = ( cgrG ‘ 𝐺 ) )
26 25 ad2antrr ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑘 = ( hlG ‘ 𝐺 ) ) → ( cgrG ‘ 𝑔 ) = ( cgrG ‘ 𝐺 ) )
27 26 breqd ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑘 = ( hlG ‘ 𝐺 ) ) → ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ↔ 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ) )
28 fveq1 ⊢ ( 𝑘 = ( hlG ‘ 𝐺 ) → ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) = ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) )
29 28 adantl ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑘 = ( hlG ‘ 𝐺 ) ) → ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) = ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) )
30 29 breqd ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑘 = ( hlG ‘ 𝐺 ) ) → ( 𝑥 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ↔ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ) )
31 29 breqd ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑘 = ( hlG ‘ 𝐺 ) ) → ( 𝑦 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ↔ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) )
32 27 30 31 3anbi123d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑘 = ( hlG ‘ 𝐺 ) ) → ( ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ↔ ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) )
33 24 32 rexeqbidv ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑘 = ( hlG ‘ 𝐺 ) ) → ( ∃ 𝑦 ∈ 𝑝 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ↔ ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) )
34 24 33 rexeqbidv ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑘 = ( hlG ‘ 𝐺 ) ) → ( ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) )
35 23 34 anbi12d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑘 = ( hlG ‘ 𝐺 ) ) → ( ( ( 𝑎 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) ↔ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) ) )
36 16 18 35 sbcied2 ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) → ( [ ( hlG ‘ 𝑔 ) / 𝑘 ] ( ( 𝑎 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) ↔ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) ) )
37 13 15 36 sbcied2 ⊢ ( 𝑔 = 𝐺 → ( [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( hlG ‘ 𝑔 ) / 𝑘 ] ( ( 𝑎 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) ↔ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) ) )
38 an21 ⊢ ( ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) ↔ ( 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) ) )
39 37 38 bitrdi ⊢ ( 𝑔 = 𝐺 → ( [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( hlG ‘ 𝑔 ) / 𝑘 ] ( ( 𝑎 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) ↔ ( 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) ) ) )
40 39 opabbidv ⊢ ( 𝑔 = 𝐺 → { ⟨ 𝑎 , 𝑏 ⟩ ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( hlG ‘ 𝑔 ) / 𝑘 ] ( ( 𝑎 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) ) } )
41 4 elexd ⊢ ( 𝜑 → 𝐺 ∈ V )
42 ovexd ⊢ ( 𝜑 → ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∈ V )
43 simprrl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) ) ) → 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
44 simprl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) ) ) → 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
45 42 42 43 44 opabex2 ⊢ ( 𝜑 → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) ) } ∈ V )
46 12 40 41 45 fvmptd3 ⊢ ( 𝜑 → ( cgrA ‘ 𝐺 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) ) } )
47 3 46 eqtrid ⊢ ( 𝜑 → ∼ = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) ) } )
48 47 rneqd ⊢ ( 𝜑 → ran ∼ = ran { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) ) } )
49 rnopabss ⊢ ran { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑎 ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) ) } ⊆ ( 𝑃 ↑m ( 0 ..^ 3 ) )
50 48 49 eqsstrdi ⊢ ( 𝜑 → ran ∼ ⊆ ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
51 11 50 sstrid ⊢ ( 𝜑 → ( ∼ “ 𝐴 ) ⊆ ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
52 51 sselda ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) → 𝑒 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
53 52 ad10antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → 𝑒 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
54 eqid ⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
55 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
56 4 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) → 𝐺 ∈ TarskiG )
57 56 ad4antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → 𝐺 ∈ TarskiG )
58 simp-4r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → 𝑢 ∈ 𝑃 )
59 simpllr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → 𝑣 ∈ 𝑃 )
60 simplr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → 𝑤 ∈ 𝑃 )
61 simp-8r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → 𝑥 ∈ 𝑃 )
62 simp-7r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → 𝑦 ∈ 𝑃 )
63 simp-6r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → 𝑧 ∈ 𝑃 )
64 3 a1i ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → ∼ = ( cgrA ‘ 𝐺 ) )
65 simp-9r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → 𝑓 ∼ 𝑒 )
66 64 65 breqdi ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → 𝑓 ( cgrA ‘ 𝐺 ) 𝑒 )
67 simpr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
68 simp-5r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ )
69 66 67 68 3brtr3d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → ⟨“ 𝑢 𝑣 𝑤 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑥 𝑦 𝑧 ”⟩ )
70 1 54 55 57 58 59 60 61 62 63 69 cgrane3 ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → 𝑦 ≠ 𝑥 )
71 70 necomd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → 𝑥 ≠ 𝑦 )
72 68 fveq1d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → ( 𝑒 ‘ 0 ) = ( ⟨“ 𝑥 𝑦 𝑧 ”⟩ ‘ 0 ) )
73 s3fv0 ⊢ ( 𝑥 ∈ 𝑃 → ( ⟨“ 𝑥 𝑦 𝑧 ”⟩ ‘ 0 ) = 𝑥 )
74 61 73 syl ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → ( ⟨“ 𝑥 𝑦 𝑧 ”⟩ ‘ 0 ) = 𝑥 )
75 72 74 eqtrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → ( 𝑒 ‘ 0 ) = 𝑥 )
76 68 fveq1d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → ( 𝑒 ‘ 1 ) = ( ⟨“ 𝑥 𝑦 𝑧 ”⟩ ‘ 1 ) )
77 s3fv1 ⊢ ( 𝑦 ∈ 𝑃 → ( ⟨“ 𝑥 𝑦 𝑧 ”⟩ ‘ 1 ) = 𝑦 )
78 77 ad7antlr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → ( ⟨“ 𝑥 𝑦 𝑧 ”⟩ ‘ 1 ) = 𝑦 )
79 76 78 eqtrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → ( 𝑒 ‘ 1 ) = 𝑦 )
80 71 75 79 3netr4d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → ( 𝑒 ‘ 0 ) ≠ ( 𝑒 ‘ 1 ) )
81 1 54 55 57 58 59 60 61 62 63 69 cgrane4 ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → 𝑦 ≠ 𝑧 )
82 68 fveq1d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → ( 𝑒 ‘ 2 ) = ( ⟨“ 𝑥 𝑦 𝑧 ”⟩ ‘ 2 ) )
83 s3fv2 ⊢ ( 𝑧 ∈ 𝑃 → ( ⟨“ 𝑥 𝑦 𝑧 ”⟩ ‘ 2 ) = 𝑧 )
84 63 83 syl ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → ( ⟨“ 𝑥 𝑦 𝑧 ”⟩ ‘ 2 ) = 𝑧 )
85 82 84 eqtrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → ( 𝑒 ‘ 2 ) = 𝑧 )
86 81 79 85 3netr4d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → ( 𝑒 ‘ 1 ) ≠ ( 𝑒 ‘ 2 ) )
87 80 86 jca ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → ( ( 𝑒 ‘ 0 ) ≠ ( 𝑒 ‘ 1 ) ∧ ( 𝑒 ‘ 1 ) ≠ ( 𝑒 ‘ 2 ) ) )
88 10 53 87 elrabd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → 𝑒 ∈ { 𝑑 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) } )
89 88 2 eleqtrrdi ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → 𝑒 ∈ 𝐴 )
90 89 r19.29an ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ∃ 𝑤 ∈ 𝑃 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) → 𝑒 ∈ 𝐴 )
91 1 fvexi ⊢ 𝑃 ∈ V
92 simp-6r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) → 𝑓 ∈ 𝐴 )
93 91 2 92 elcgrabasi ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) → ∃ 𝑢 ∈ 𝑃 ∃ 𝑣 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤 ) ) )
94 simpl ⊢ ( ( 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤 ) ) → 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
95 94 reximi ⊢ ( ∃ 𝑤 ∈ 𝑃 ( 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤 ) ) → ∃ 𝑤 ∈ 𝑃 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
96 95 reximi ⊢ ( ∃ 𝑣 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤 ) ) → ∃ 𝑣 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
97 96 reximi ⊢ ( ∃ 𝑢 ∈ 𝑃 ∃ 𝑣 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤 ) ) → ∃ 𝑢 ∈ 𝑃 ∃ 𝑣 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
98 93 97 syl ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) → ∃ 𝑢 ∈ 𝑃 ∃ 𝑣 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
99 90 98 r19.29vva ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) → 𝑒 ∈ 𝐴 )
100 99 r19.29an ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ∃ 𝑧 ∈ 𝑃 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) → 𝑒 ∈ 𝐴 )
101 52 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) → 𝑒 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
102 91 s3rex ⊢ ( 𝑒 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ )
103 101 102 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ )
104 100 103 r19.29vva ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) → 𝑒 ∈ 𝐴 )
105 vex ⊢ 𝑒 ∈ V
106 105 elima ⊢ ( 𝑒 ∈ ( ∼ “ 𝐴 ) ↔ ∃ 𝑓 ∈ 𝐴 𝑓 ∼ 𝑒 )
107 106 bilani ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) → ∃ 𝑓 ∈ 𝐴 𝑓 ∼ 𝑒 )
108 104 107 r19.29a ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ∼ “ 𝐴 ) ) → 𝑒 ∈ 𝐴 )
109 108 ex ⊢ ( 𝜑 → ( 𝑒 ∈ ( ∼ “ 𝐴 ) → 𝑒 ∈ 𝐴 ) )
110 109 ssrdv ⊢ ( 𝜑 → ( ∼ “ 𝐴 ) ⊆ 𝐴 )