Metamath Proof Explorer

Theorem axlowdim2

Description: The lower two-dimensional axiom. In any space where the dimension is greater than one, there are three non-colinear points. Axiom A8 of Schwabhauser p. 12. (Contributed by Scott Fenton, 15-Apr-2013)

Ref Expression
Assertion axlowdim2 ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ¬ ( 𝑥 Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , 𝑥 ⟩ ∨ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) )

Proof

Step Hyp Ref Expression
1 0re ⊢ 0 ∈ ℝ
2 1 1 axlowdimlem5 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ∈ ( 𝔼 ‘ 𝑁 ) )
3 1re ⊢ 1 ∈ ℝ
4 3 1 axlowdimlem5 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ∈ ( 𝔼 ‘ 𝑁 ) )
5 1 3 axlowdimlem5 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ∈ ( 𝔼 ‘ 𝑁 ) )
6 eqid ⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) )
7 eqid ⊢ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) )
8 eqid ⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) )
9 6 7 8 axlowdimlem6 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ¬ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) )
10 opeq2 ⊢ ( 𝑧 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑧 ⟩ = ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ )
11 10 breq2d ⊢ ( 𝑧 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑧 ⟩ ↔ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) )
12 opeq1 ⊢ ( 𝑧 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ = ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ )
13 12 breq2d ⊢ ( 𝑧 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ↔ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) )
14 breq1 ⊢ ( 𝑧 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ↔ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) )
15 11 13 14 3orbi123d ⊢ ( 𝑧 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑧 ⟩ ∨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) ↔ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) ) )
16 15 notbid ⊢ ( 𝑧 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ¬ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑧 ⟩ ∨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) ↔ ¬ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) ) )
17 16 rspcev ⊢ ( ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ∈ ( 𝔼 ‘ 𝑁 ) ∧ ¬ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) ) → ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ¬ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑧 ⟩ ∨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) )
18 5 9 17 syl2anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ¬ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑧 ⟩ ∨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) )
19 breq1 ⊢ ( 𝑥 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( 𝑥 Btwn ⟨ 𝑦 , 𝑧 ⟩ ↔ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑦 , 𝑧 ⟩ ) )
20 opeq2 ⊢ ( 𝑥 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ⟨ 𝑧 , 𝑥 ⟩ = ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ )
21 20 breq2d ⊢ ( 𝑥 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( 𝑦 Btwn ⟨ 𝑧 , 𝑥 ⟩ ↔ 𝑦 Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) )
22 opeq1 ⊢ ( 𝑥 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑦 ⟩ )
23 22 breq2d ⊢ ( 𝑥 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑦 ⟩ ) )
24 19 21 23 3orbi123d ⊢ ( 𝑥 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ( 𝑥 Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , 𝑥 ⟩ ∨ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑦 ⟩ ) ) )
25 24 notbid ⊢ ( 𝑥 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ¬ ( 𝑥 Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , 𝑥 ⟩ ∨ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ¬ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑦 ⟩ ) ) )
26 25 rexbidv ⊢ ( 𝑥 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ¬ ( 𝑥 Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , 𝑥 ⟩ ∨ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ¬ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑦 ⟩ ) ) )
27 opeq1 ⊢ ( 𝑦 = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ⟨ 𝑦 , 𝑧 ⟩ = ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑧 ⟩ )
28 27 breq2d ⊢ ( 𝑦 = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑦 , 𝑧 ⟩ ↔ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑧 ⟩ ) )
29 breq1 ⊢ ( 𝑦 = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( 𝑦 Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ↔ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) )
30 opeq2 ⊢ ( 𝑦 = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑦 ⟩ = ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ )
31 30 breq2d ⊢ ( 𝑦 = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑦 ⟩ ↔ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) )
32 28 29 31 3orbi123d ⊢ ( 𝑦 = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑦 ⟩ ) ↔ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑧 ⟩ ∨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) ) )
33 32 notbid ⊢ ( 𝑦 = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ¬ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑦 ⟩ ) ↔ ¬ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑧 ⟩ ∨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) ) )
34 33 rexbidv ⊢ ( 𝑦 = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) → ( ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ¬ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑦 ⟩ ) ↔ ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ¬ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑧 ⟩ ∨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) ) )
35 26 34 rspc2ev ⊢ ( ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ¬ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , 𝑧 ⟩ ∨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ 𝑧 , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ∨ 𝑧 Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ¬ ( 𝑥 Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , 𝑥 ⟩ ∨ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) )
36 2 4 18 35 syl3anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ¬ ( 𝑥 Btwn ⟨ 𝑦 , 𝑧 ⟩ ∨ 𝑦 Btwn ⟨ 𝑧 , 𝑥 ⟩ ∨ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) )