Metamath Proof Explorer

Theorem axlowdimlem7

Description: Lemma for axlowdim . Set up a point in Euclidean space. (Contributed by Scott Fenton, 29-Jun-2013)

Ref Expression
Hypothesis axlowdimlem7.1 ⊢ 𝑃 = ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) )
Assertion axlowdimlem7 ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 axlowdimlem7.1 ⊢ 𝑃 = ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) )
2 eqid ⊢ { ⟨ 3 , - 1 ⟩ } = { ⟨ 3 , - 1 ⟩ }
3 3ex ⊢ 3 ∈ V
4 negex ⊢ - 1 ∈ V
5 3 4 fsn ⊢ ( { ⟨ 3 , - 1 ⟩ } : { 3 } ⟶ { - 1 } ↔ { ⟨ 3 , - 1 ⟩ } = { ⟨ 3 , - 1 ⟩ } )
6 2 5 mpbir ⊢ { ⟨ 3 , - 1 ⟩ } : { 3 } ⟶ { - 1 }
7 neg1rr ⊢ - 1 ∈ ℝ
8 snssi ⊢ ( - 1 ∈ ℝ → { - 1 } ⊆ ℝ )
9 7 8 ax-mp ⊢ { - 1 } ⊆ ℝ
10 fss ⊢ ( ( { ⟨ 3 , - 1 ⟩ } : { 3 } ⟶ { - 1 } ∧ { - 1 } ⊆ ℝ ) → { ⟨ 3 , - 1 ⟩ } : { 3 } ⟶ ℝ )
11 6 9 10 mp2an ⊢ { ⟨ 3 , - 1 ⟩ } : { 3 } ⟶ ℝ
12 0re ⊢ 0 ∈ ℝ
13 12 fconst6 ⊢ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) : ( ( 1 ... 𝑁 ) ∖ { 3 } ) ⟶ ℝ
14 11 13 pm3.2i ⊢ ( { ⟨ 3 , - 1 ⟩ } : { 3 } ⟶ ℝ ∧ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) : ( ( 1 ... 𝑁 ) ∖ { 3 } ) ⟶ ℝ )
15 disjdif ⊢ ( { 3 } ∩ ( ( 1 ... 𝑁 ) ∖ { 3 } ) ) = ∅
16 fun2 ⊢ ( ( ( { ⟨ 3 , - 1 ⟩ } : { 3 } ⟶ ℝ ∧ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) : ( ( 1 ... 𝑁 ) ∖ { 3 } ) ⟶ ℝ ) ∧ ( { 3 } ∩ ( ( 1 ... 𝑁 ) ∖ { 3 } ) ) = ∅ ) → ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) : ( { 3 } ∪ ( ( 1 ... 𝑁 ) ∖ { 3 } ) ) ⟶ ℝ )
17 14 15 16 mp2an ⊢ ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) : ( { 3 } ∪ ( ( 1 ... 𝑁 ) ∖ { 3 } ) ) ⟶ ℝ
18 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 3 ≤ 𝑁 )
19 1le3 ⊢ 1 ≤ 3
20 18 19 jctil ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 1 ≤ 3 ∧ 3 ≤ 𝑁 ) )
21 3z ⊢ 3 ∈ ℤ
22 1z ⊢ 1 ∈ ℤ
23 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℤ )
24 elfz ⊢ ( ( 3 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 3 ∈ ( 1 ... 𝑁 ) ↔ ( 1 ≤ 3 ∧ 3 ≤ 𝑁 ) ) )
25 21 22 23 24 mp3an12i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 3 ∈ ( 1 ... 𝑁 ) ↔ ( 1 ≤ 3 ∧ 3 ≤ 𝑁 ) ) )
26 20 25 mpbird ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 3 ∈ ( 1 ... 𝑁 ) )
27 26 snssd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → { 3 } ⊆ ( 1 ... 𝑁 ) )
28 undif ⊢ ( { 3 } ⊆ ( 1 ... 𝑁 ) ↔ ( { 3 } ∪ ( ( 1 ... 𝑁 ) ∖ { 3 } ) ) = ( 1 ... 𝑁 ) )
29 27 28 sylib ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( { 3 } ∪ ( ( 1 ... 𝑁 ) ∖ { 3 } ) ) = ( 1 ... 𝑁 ) )
30 29 feq2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) : ( { 3 } ∪ ( ( 1 ... 𝑁 ) ∖ { 3 } ) ) ⟶ ℝ ↔ ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) : ( 1 ... 𝑁 ) ⟶ ℝ ) )
31 17 30 mpbii ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) : ( 1 ... 𝑁 ) ⟶ ℝ )
32 eluzge3nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ )
33 elee ⊢ ( 𝑁 ∈ ℕ → ( ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) ∈ ( 𝔼 ‘ 𝑁 ) ↔ ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) : ( 1 ... 𝑁 ) ⟶ ℝ ) )
34 32 33 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) ∈ ( 𝔼 ‘ 𝑁 ) ↔ ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) : ( 1 ... 𝑁 ) ⟶ ℝ ) )
35 31 34 mpbird ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) ∈ ( 𝔼 ‘ 𝑁 ) )
36 1 35 eqeltrid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )