Metamath Proof Explorer

Theorem axlowdim1

Description: The lower dimension axiom for one dimension. In any dimension, there are at least two distinct points. Theorem 3.13 of Schwabhauser p. 32, where it is derived from axlowdim2 . (Contributed by Scott Fenton, 22-Apr-2013)

Ref Expression
Assertion axlowdim1 ( 𝑁 ∈ ℕ → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) 𝑥 ≠ 𝑦 )

Proof

Step Hyp Ref Expression
1 1re ⊢ 1 ∈ ℝ
2 1 fconst6 ⊢ ( ( 1 ... 𝑁 ) × { 1 } ) : ( 1 ... 𝑁 ) ⟶ ℝ
3 elee ⊢ ( 𝑁 ∈ ℕ → ( ( ( 1 ... 𝑁 ) × { 1 } ) ∈ ( 𝔼 ‘ 𝑁 ) ↔ ( ( 1 ... 𝑁 ) × { 1 } ) : ( 1 ... 𝑁 ) ⟶ ℝ ) )
4 2 3 mpbiri ⊢ ( 𝑁 ∈ ℕ → ( ( 1 ... 𝑁 ) × { 1 } ) ∈ ( 𝔼 ‘ 𝑁 ) )
5 0re ⊢ 0 ∈ ℝ
6 5 fconst6 ⊢ ( ( 1 ... 𝑁 ) × { 0 } ) : ( 1 ... 𝑁 ) ⟶ ℝ
7 elee ⊢ ( 𝑁 ∈ ℕ → ( ( ( 1 ... 𝑁 ) × { 0 } ) ∈ ( 𝔼 ‘ 𝑁 ) ↔ ( ( 1 ... 𝑁 ) × { 0 } ) : ( 1 ... 𝑁 ) ⟶ ℝ ) )
8 6 7 mpbiri ⊢ ( 𝑁 ∈ ℕ → ( ( 1 ... 𝑁 ) × { 0 } ) ∈ ( 𝔼 ‘ 𝑁 ) )
9 ax-1ne0 ⊢ 1 ≠ 0
10 9 neii ⊢ ¬ 1 = 0
11 1ex ⊢ 1 ∈ V
12 11 sneqr ⊢ ( { 1 } = { 0 } → 1 = 0 )
13 10 12 mto ⊢ ¬ { 1 } = { 0 }
14 elnnuz ⊢ ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
15 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... 𝑁 ) )
16 14 15 sylbi ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ( 1 ... 𝑁 ) )
17 16 ne0d ⊢ ( 𝑁 ∈ ℕ → ( 1 ... 𝑁 ) ≠ ∅ )
18 rnxp ⊢ ( ( 1 ... 𝑁 ) ≠ ∅ → ran ( ( 1 ... 𝑁 ) × { 1 } ) = { 1 } )
19 17 18 syl ⊢ ( 𝑁 ∈ ℕ → ran ( ( 1 ... 𝑁 ) × { 1 } ) = { 1 } )
20 rnxp ⊢ ( ( 1 ... 𝑁 ) ≠ ∅ → ran ( ( 1 ... 𝑁 ) × { 0 } ) = { 0 } )
21 17 20 syl ⊢ ( 𝑁 ∈ ℕ → ran ( ( 1 ... 𝑁 ) × { 0 } ) = { 0 } )
22 19 21 eqeq12d ⊢ ( 𝑁 ∈ ℕ → ( ran ( ( 1 ... 𝑁 ) × { 1 } ) = ran ( ( 1 ... 𝑁 ) × { 0 } ) ↔ { 1 } = { 0 } ) )
23 13 22 mtbiri ⊢ ( 𝑁 ∈ ℕ → ¬ ran ( ( 1 ... 𝑁 ) × { 1 } ) = ran ( ( 1 ... 𝑁 ) × { 0 } ) )
24 rneq ⊢ ( ( ( 1 ... 𝑁 ) × { 1 } ) = ( ( 1 ... 𝑁 ) × { 0 } ) → ran ( ( 1 ... 𝑁 ) × { 1 } ) = ran ( ( 1 ... 𝑁 ) × { 0 } ) )
25 23 24 nsyl ⊢ ( 𝑁 ∈ ℕ → ¬ ( ( 1 ... 𝑁 ) × { 1 } ) = ( ( 1 ... 𝑁 ) × { 0 } ) )
26 25 neqned ⊢ ( 𝑁 ∈ ℕ → ( ( 1 ... 𝑁 ) × { 1 } ) ≠ ( ( 1 ... 𝑁 ) × { 0 } ) )
27 neeq1 ⊢ ( 𝑥 = ( ( 1 ... 𝑁 ) × { 1 } ) → ( 𝑥 ≠ 𝑦 ↔ ( ( 1 ... 𝑁 ) × { 1 } ) ≠ 𝑦 ) )
28 neeq2 ⊢ ( 𝑦 = ( ( 1 ... 𝑁 ) × { 0 } ) → ( ( ( 1 ... 𝑁 ) × { 1 } ) ≠ 𝑦 ↔ ( ( 1 ... 𝑁 ) × { 1 } ) ≠ ( ( 1 ... 𝑁 ) × { 0 } ) ) )
29 27 28 rspc2ev ⊢ ( ( ( ( 1 ... 𝑁 ) × { 1 } ) ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( ( 1 ... 𝑁 ) × { 0 } ) ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( ( 1 ... 𝑁 ) × { 1 } ) ≠ ( ( 1 ... 𝑁 ) × { 0 } ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) 𝑥 ≠ 𝑦 )
30 4 8 26 29 syl3anc ⊢ ( 𝑁 ∈ ℕ → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) 𝑥 ≠ 𝑦 )