Metamath Proof Explorer

Theorem segconeq

Description: Two points that satisfy the conclusion of axsegcon are identical. Uniqueness portion of Theorem 2.12 of Schwabhauser p. 29. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion segconeq ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → 𝑋 = 𝑌 ) )

Proof

Step Hyp Ref Expression
1 simpr2l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ )
2 1 1 jca ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ) )
3 simpl1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → 𝑁 ∈ ℕ )
4 simpl31 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) )
5 simpl21 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
6 3 4 5 cgrrflxd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ⟨ 𝑄 , 𝐴 ⟩ Cgr ⟨ 𝑄 , 𝐴 ⟩ )
7 simpl32 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) )
8 3 5 7 cgrrflxd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑋 ⟩ )
9 6 8 jca ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ( ⟨ 𝑄 , 𝐴 ⟩ Cgr ⟨ 𝑄 , 𝐴 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑋 ⟩ ) )
10 simpl33 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) )
11 4 5 10 3jca ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) )
12 4 5 7 3jca ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ) )
13 3 11 12 3jca ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ) ) )
14 simpr3l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ )
15 14 1 jca ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ) )
16 simpl22 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
17 simpl23 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
18 simpr3r ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ )
19 cgrcom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) )
20 3 5 10 16 17 19 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ( ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ ) )
21 18 20 mpbid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝑌 ⟩ )
22 simpr2r ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ )
23 cgrcom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝑋 ⟩ ) )
24 3 5 7 16 17 23 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ( ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝑋 ⟩ ) )
25 22 24 mpbid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝑋 ⟩ )
26 3 16 17 5 10 5 7 21 25 cgrtr4d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐴 , 𝑋 ⟩ )
27 15 6 26 jca32 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ( ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ) ∧ ( ⟨ 𝑄 , 𝐴 ⟩ Cgr ⟨ 𝑄 , 𝐴 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐴 , 𝑋 ⟩ ) ) )
28 cgrextend ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ) ∧ ( ⟨ 𝑄 , 𝐴 ⟩ Cgr ⟨ 𝑄 , 𝐴 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐴 , 𝑋 ⟩ ) ) → ⟨ 𝑄 , 𝑌 ⟩ Cgr ⟨ 𝑄 , 𝑋 ⟩ ) )
29 13 27 28 sylc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ⟨ 𝑄 , 𝑌 ⟩ Cgr ⟨ 𝑄 , 𝑋 ⟩ )
30 29 26 jca ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ( ⟨ 𝑄 , 𝑌 ⟩ Cgr ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐴 , 𝑋 ⟩ ) )
31 2 9 30 3jca ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) ) → ( ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ) ∧ ( ⟨ 𝑄 , 𝐴 ⟩ Cgr ⟨ 𝑄 , 𝐴 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑋 ⟩ ) ∧ ( ⟨ 𝑄 , 𝑌 ⟩ Cgr ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐴 , 𝑋 ⟩ ) ) )
32 31 ex ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → ( ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ) ∧ ( ⟨ 𝑄 , 𝐴 ⟩ Cgr ⟨ 𝑄 , 𝐴 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑋 ⟩ ) ∧ ( ⟨ 𝑄 , 𝑌 ⟩ Cgr ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐴 , 𝑋 ⟩ ) ) ) )
33 simp1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
34 simp31 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) )
35 simp21 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
36 simp32 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) )
37 simp33 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) )
38 brofs ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ ⟨ 𝑄 , 𝐴 ⟩ , ⟨ 𝑋 , 𝑌 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝑄 , 𝐴 ⟩ , ⟨ 𝑋 , 𝑋 ⟩ ⟩ ↔ ( ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ) ∧ ( ⟨ 𝑄 , 𝐴 ⟩ Cgr ⟨ 𝑄 , 𝐴 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑋 ⟩ ) ∧ ( ⟨ 𝑄 , 𝑌 ⟩ Cgr ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐴 , 𝑋 ⟩ ) ) ) )
39 33 34 35 36 37 34 35 36 36 38 syl333anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ ⟨ 𝑄 , 𝐴 ⟩ , ⟨ 𝑋 , 𝑌 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝑄 , 𝐴 ⟩ , ⟨ 𝑋 , 𝑋 ⟩ ⟩ ↔ ( ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ) ∧ ( ⟨ 𝑄 , 𝐴 ⟩ Cgr ⟨ 𝑄 , 𝐴 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐴 , 𝑋 ⟩ ) ∧ ( ⟨ 𝑄 , 𝑌 ⟩ Cgr ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐴 , 𝑋 ⟩ ) ) ) )
40 32 39 sylibrd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → ⟨ ⟨ 𝑄 , 𝐴 ⟩ , ⟨ 𝑋 , 𝑌 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝑄 , 𝐴 ⟩ , ⟨ 𝑋 , 𝑋 ⟩ ⟩ ) )
41 simp1 ⊢ ( ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → 𝑄 ≠ 𝐴 )
42 41 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → 𝑄 ≠ 𝐴 ) )
43 40 42 jcad ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → ( ⟨ ⟨ 𝑄 , 𝐴 ⟩ , ⟨ 𝑋 , 𝑌 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝑄 , 𝐴 ⟩ , ⟨ 𝑋 , 𝑋 ⟩ ⟩ ∧ 𝑄 ≠ 𝐴 ) ) )
44 5segofs ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ ⟨ 𝑄 , 𝐴 ⟩ , ⟨ 𝑋 , 𝑌 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝑄 , 𝐴 ⟩ , ⟨ 𝑋 , 𝑋 ⟩ ⟩ ∧ 𝑄 ≠ 𝐴 ) → ⟨ 𝑋 , 𝑌 ⟩ Cgr ⟨ 𝑋 , 𝑋 ⟩ ) )
45 33 34 35 36 37 34 35 36 36 44 syl333anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ ⟨ 𝑄 , 𝐴 ⟩ , ⟨ 𝑋 , 𝑌 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝑄 , 𝐴 ⟩ , ⟨ 𝑋 , 𝑋 ⟩ ⟩ ∧ 𝑄 ≠ 𝐴 ) → ⟨ 𝑋 , 𝑌 ⟩ Cgr ⟨ 𝑋 , 𝑋 ⟩ ) )
46 axcgrid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑋 , 𝑌 ⟩ Cgr ⟨ 𝑋 , 𝑋 ⟩ → 𝑋 = 𝑌 ) )
47 33 36 37 36 46 syl13anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑋 , 𝑌 ⟩ Cgr ⟨ 𝑋 , 𝑋 ⟩ → 𝑋 = 𝑌 ) )
48 43 45 47 3syld ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑄 ≠ 𝐴 ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑋 ⟩ ∧ ⟨ 𝐴 , 𝑋 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( 𝐴 Btwn ⟨ 𝑄 , 𝑌 ⟩ ∧ ⟨ 𝐴 , 𝑌 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) → 𝑋 = 𝑌 ) )