Metamath Proof Explorer

Theorem cgraer

Description: The angle congruence relation is an equivalence relation. (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 cgraer ( 𝜑 → ( ∼ ∩ ( 𝐴 × 𝐴 ) ) Er 𝐴 )

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 relinxp ⊢ Rel ( ∼ ∩ ( 𝐴 × 𝐴 ) )
6 5 a1i ⊢ ( 𝜑 → Rel ( ∼ ∩ ( 𝐴 × 𝐴 ) ) )
7 brinxp2 ⊢ ( 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ↔ ( ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑒 ∼ 𝑓 ) )
8 7 bilani ⊢ ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) → ( ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑒 ∼ 𝑓 ) )
9 8 simplrd ⊢ ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) → 𝑓 ∈ 𝐴 )
10 8 simplld ⊢ ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) → 𝑒 ∈ 𝐴 )
11 3 a1i ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → ∼ = ( cgrA ‘ 𝐺 ) )
12 11 eqcomd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → ( cgrA ‘ 𝐺 ) = ∼ )
13 eqid ⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
14 4 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → 𝐺 ∈ TarskiG )
15 14 ad6antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝐺 ∈ TarskiG )
16 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
17 simp-6r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → 𝑥 ∈ 𝑃 )
18 17 ad6antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝑥 ∈ 𝑃 )
19 simp-11r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝑦 ∈ 𝑃 )
20 simp-10r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝑧 ∈ 𝑃 )
21 simp-6r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝑢 ∈ 𝑃 )
22 simp-5r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝑣 ∈ 𝑃 )
23 simp-4r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝑤 ∈ 𝑃 )
24 8 simprd ⊢ ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) → 𝑒 ∼ 𝑓 )
25 24 ad6antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → 𝑒 ∼ 𝑓 )
26 25 ad6antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝑒 ∼ 𝑓 )
27 11 26 breqdi ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝑒 ( cgrA ‘ 𝐺 ) 𝑓 )
28 simp-9r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ )
29 simpllr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
30 27 28 29 3brtr3d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → ⟨“ 𝑥 𝑦 𝑧 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
31 1 13 15 16 18 19 20 21 22 23 30 cgracom ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → ⟨“ 𝑢 𝑣 𝑤 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑥 𝑦 𝑧 ”⟩ )
32 12 31 breqdi ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ )
33 32 29 28 3brtr4d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝑓 ∼ 𝑒 )
34 33 anasss ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ ( 𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤 ) ) → 𝑓 ∼ 𝑒 )
35 34 anasss ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤 ) ) ) → 𝑓 ∼ 𝑒 )
36 35 r19.29an ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ∃ 𝑤 ∈ 𝑃 ( 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤 ) ) ) → 𝑓 ∼ 𝑒 )
37 1 fvexi ⊢ 𝑃 ∈ V
38 9 ad6antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → 𝑓 ∈ 𝐴 )
39 37 2 38 elcgrabasi ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → ∃ 𝑢 ∈ 𝑃 ∃ 𝑣 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤 ) ) )
40 36 39 r19.29vva ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → 𝑓 ∼ 𝑒 )
41 40 anasss ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ) ) → 𝑓 ∼ 𝑒 )
42 41 anasss ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ) ) ) → 𝑓 ∼ 𝑒 )
43 42 r19.29an ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ) ) ) → 𝑓 ∼ 𝑒 )
44 37 2 10 elcgrabasi ⊢ ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ) ) )
45 43 44 r19.29vva ⊢ ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) → 𝑓 ∼ 𝑒 )
46 brinxp2 ⊢ ( 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑒 ↔ ( ( 𝑓 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑒 ) )
47 9 10 45 46 syl21anbrc ⊢ ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) → 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑒 )
48 10 adantr ⊢ ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) → 𝑒 ∈ 𝐴 )
49 48 ad6antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → 𝑒 ∈ 𝐴 )
50 49 ad6antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝑒 ∈ 𝐴 )
51 50 ad6antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑗 ≠ 𝑘 ) → 𝑒 ∈ 𝐴 )
52 brinxp2 ⊢ ( 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ↔ ( ( 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑔 ) )
53 52 biimpi ⊢ ( 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 → ( ( 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) ∧ 𝑓 ∼ 𝑔 ) )
54 53 simplrd ⊢ ( 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 → 𝑔 ∈ 𝐴 )
55 54 ad7antlr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → 𝑔 ∈ 𝐴 )
56 55 ad6antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝑔 ∈ 𝐴 )
57 56 ad6antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑗 ≠ 𝑘 ) → 𝑔 ∈ 𝐴 )
58 3 eqcomi ⊢ ( cgrA ‘ 𝐺 ) = ∼
59 58 a1i ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑗 ≠ 𝑘 ) → ( cgrA ‘ 𝐺 ) = ∼ )
60 4 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → 𝐺 ∈ TarskiG )
61 60 ad6antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝐺 ∈ TarskiG )
62 61 ad6antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑗 ≠ 𝑘 ) → 𝐺 ∈ TarskiG )
63 simp-6r ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → 𝑥 ∈ 𝑃 )
64 63 ad6antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝑥 ∈ 𝑃 )
65 64 ad6antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑗 ≠ 𝑘 ) → 𝑥 ∈ 𝑃 )
66 simp-11r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝑦 ∈ 𝑃 )
67 66 ad6antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑗 ≠ 𝑘 ) → 𝑦 ∈ 𝑃 )
68 simp-10r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝑧 ∈ 𝑃 )
69 68 ad6antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑗 ≠ 𝑘 ) → 𝑧 ∈ 𝑃 )
70 simp-6r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝑢 ∈ 𝑃 )
71 70 ad6antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑗 ≠ 𝑘 ) → 𝑢 ∈ 𝑃 )
72 simp-11r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑗 ≠ 𝑘 ) → 𝑣 ∈ 𝑃 )
73 simp-10r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑗 ≠ 𝑘 ) → 𝑤 ∈ 𝑃 )
74 3 a1i ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑗 ≠ 𝑘 ) → ∼ = ( cgrA ‘ 𝐺 ) )
75 24 ad7antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → 𝑒 ∼ 𝑓 )
76 75 ad6antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝑒 ∼ 𝑓 )
77 76 ad6antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑗 ≠ 𝑘 ) → 𝑒 ∼ 𝑓 )
78 74 77 breqdi ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑗 ≠ 𝑘 ) → 𝑒 ( cgrA ‘ 𝐺 ) 𝑓 )
79 simp-9r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ )
80 79 ad6antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑗 ≠ 𝑘 ) → 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ )
81 simp-9r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑗 ≠ 𝑘 ) → 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
82 78 80 81 3brtr3d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑗 ≠ 𝑘 ) → ⟨“ 𝑥 𝑦 𝑧 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
83 simp-6r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑗 ≠ 𝑘 ) → 𝑖 ∈ 𝑃 )
84 simp-5r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑗 ≠ 𝑘 ) → 𝑗 ∈ 𝑃 )
85 simp-4r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑗 ≠ 𝑘 ) → 𝑘 ∈ 𝑃 )
86 53 simprd ⊢ ( 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 → 𝑓 ∼ 𝑔 )
87 86 ad7antlr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → 𝑓 ∼ 𝑔 )
88 87 ad6antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝑓 ∼ 𝑔 )
89 88 ad6antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑗 ≠ 𝑘 ) → 𝑓 ∼ 𝑔 )
90 74 89 breqdi ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑗 ≠ 𝑘 ) → 𝑓 ( cgrA ‘ 𝐺 ) 𝑔 )
91 simpllr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑗 ≠ 𝑘 ) → 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ )
92 90 81 91 3brtr3d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑗 ≠ 𝑘 ) → ⟨“ 𝑢 𝑣 𝑤 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑖 𝑗 𝑘 ”⟩ )
93 1 13 62 16 65 67 69 71 72 73 82 83 84 85 92 cgratr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑗 ≠ 𝑘 ) → ⟨“ 𝑥 𝑦 𝑧 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑖 𝑗 𝑘 ”⟩ )
94 59 93 breqdi ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑗 ≠ 𝑘 ) → ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∼ ⟨“ 𝑖 𝑗 𝑘 ”⟩ )
95 94 80 91 3brtr4d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑗 ≠ 𝑘 ) → 𝑒 ∼ 𝑔 )
96 brinxp2 ⊢ ( 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ↔ ( ( 𝑒 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) ∧ 𝑒 ∼ 𝑔 ) )
97 51 57 95 96 syl21anbrc ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑗 ≠ 𝑘 ) → 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 )
98 97 anasss ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) ∧ ( 𝑖 ≠ 𝑗 ∧ 𝑗 ≠ 𝑘 ) ) → 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 )
99 98 anasss ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ ( 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ∧ ( 𝑖 ≠ 𝑗 ∧ 𝑗 ≠ 𝑘 ) ) ) → 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 )
100 99 r19.29an ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑖 ∈ 𝑃 ) ∧ 𝑗 ∈ 𝑃 ) ∧ ∃ 𝑘 ∈ 𝑃 ( 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ∧ ( 𝑖 ≠ 𝑗 ∧ 𝑗 ≠ 𝑘 ) ) ) → 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 )
101 37 2 56 elcgrabasi ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → ∃ 𝑖 ∈ 𝑃 ∃ 𝑗 ∈ 𝑃 ∃ 𝑘 ∈ 𝑃 ( 𝑔 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ∧ ( 𝑖 ≠ 𝑗 ∧ 𝑗 ≠ 𝑘 ) ) )
102 100 101 r19.29vva ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 )
103 102 anasss ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ ( 𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤 ) ) → 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 )
104 103 anasss ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤 ) ) ) → 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 )
105 104 r19.29an ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ∃ 𝑤 ∈ 𝑃 ( 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤 ) ) ) → 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 )
106 39 adantl6r ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → ∃ 𝑢 ∈ 𝑃 ∃ 𝑣 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝑓 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤 ) ) )
107 105 106 r19.29vva ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 )
108 107 anasss ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ) ) → 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 )
109 108 anasss ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ) ) ) → 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 )
110 109 r19.29an ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ) ) ) → 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 )
111 37 2 48 elcgrabasi ⊢ ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ) ) )
112 110 111 r19.29vva ⊢ ( ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ) ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) → 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 )
113 112 anasss ⊢ ( ( 𝜑 ∧ ( 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑓 ∧ 𝑓 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 ) ) → 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑔 )
114 simpr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐴 ) → 𝑒 ∈ 𝐴 )
115 58 a1i ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → ( cgrA ‘ 𝐺 ) = ∼ )
116 4 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → 𝐺 ∈ TarskiG )
117 simp-6r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → 𝑥 ∈ 𝑃 )
118 simp-5r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → 𝑦 ∈ 𝑃 )
119 simp-4r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → 𝑧 ∈ 𝑃 )
120 simplr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → 𝑥 ≠ 𝑦 )
121 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → 𝑦 ≠ 𝑧 )
122 1 13 116 16 117 118 119 120 121 cgraid ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → ⟨“ 𝑥 𝑦 𝑧 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑥 𝑦 𝑧 ”⟩ )
123 115 122 breqdi ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ )
124 simpllr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ )
125 123 124 124 3brtr4d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → 𝑒 ∼ 𝑒 )
126 125 anasss ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ) ) → 𝑒 ∼ 𝑒 )
127 126 anasss ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ) ) ) → 𝑒 ∼ 𝑒 )
128 127 r19.29an ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ) ) ) → 𝑒 ∼ 𝑒 )
129 37 2 114 elcgrabasi ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( 𝑒 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ) ) )
130 128 129 r19.29vva ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐴 ) → 𝑒 ∼ 𝑒 )
131 brinxp2 ⊢ ( 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑒 ↔ ( ( 𝑒 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ 𝑒 ∼ 𝑒 ) )
132 114 114 130 131 syl21anbrc ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐴 ) → 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑒 )
133 131 bilani ⊢ ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑒 ) → ( ( 𝑒 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ 𝑒 ∼ 𝑒 ) )
134 133 simplld ⊢ ( ( 𝜑 ∧ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑒 ) → 𝑒 ∈ 𝐴 )
135 132 134 impbida ⊢ ( 𝜑 → ( 𝑒 ∈ 𝐴 ↔ 𝑒 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑒 ) )
136 6 47 113 135 iserd ⊢ ( 𝜑 → ( ∼ ∩ ( 𝐴 × 𝐴 ) ) Er 𝐴 )