Metamath Proof Explorer

Theorem axlowdimlem10

Description: Lemma for axlowdim . Set up a family of points in Euclidean space. (Contributed by Scott Fenton, 21-Apr-2013)

Ref Expression
Hypothesis axlowdimlem10.1 ⊢ 𝑄 = ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) )
Assertion axlowdimlem10 ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 axlowdimlem10.1 ⊢ 𝑄 = ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) )
2 ovex ⊢ ( 𝐼 + 1 ) ∈ V
3 1ex ⊢ 1 ∈ V
4 2 3 f1osn ⊢ { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } : { ( 𝐼 + 1 ) } –1-1-onto→ { 1 }
5 f1of ⊢ ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } : { ( 𝐼 + 1 ) } –1-1-onto→ { 1 } → { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } : { ( 𝐼 + 1 ) } ⟶ { 1 } )
6 4 5 ax-mp ⊢ { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } : { ( 𝐼 + 1 ) } ⟶ { 1 }
7 c0ex ⊢ 0 ∈ V
8 7 fconst ⊢ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) : ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ⟶ { 0 }
9 6 8 pm3.2i ⊢ ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } : { ( 𝐼 + 1 ) } ⟶ { 1 } ∧ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) : ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ⟶ { 0 } )
10 disjdif ⊢ ( { ( 𝐼 + 1 ) } ∩ ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ) = ∅
11 fun ⊢ ( ( ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } : { ( 𝐼 + 1 ) } ⟶ { 1 } ∧ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) : ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ⟶ { 0 } ) ∧ ( { ( 𝐼 + 1 ) } ∩ ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ) = ∅ ) → ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) ) : ( { ( 𝐼 + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ) ⟶ ( { 1 } ∪ { 0 } ) )
12 9 10 11 mp2an ⊢ ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) ) : ( { ( 𝐼 + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ) ⟶ ( { 1 } ∪ { 0 } )
13 1 feq1i ⊢ ( 𝑄 : ( { ( 𝐼 + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ) ⟶ ( { 1 } ∪ { 0 } ) ↔ ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) ) : ( { ( 𝐼 + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ) ⟶ ( { 1 } ∪ { 0 } ) )
14 12 13 mpbir ⊢ 𝑄 : ( { ( 𝐼 + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ) ⟶ ( { 1 } ∪ { 0 } )
15 1re ⊢ 1 ∈ ℝ
16 snssi ⊢ ( 1 ∈ ℝ → { 1 } ⊆ ℝ )
17 15 16 ax-mp ⊢ { 1 } ⊆ ℝ
18 0re ⊢ 0 ∈ ℝ
19 snssi ⊢ ( 0 ∈ ℝ → { 0 } ⊆ ℝ )
20 18 19 ax-mp ⊢ { 0 } ⊆ ℝ
21 17 20 unssi ⊢ ( { 1 } ∪ { 0 } ) ⊆ ℝ
22 fss ⊢ ( ( 𝑄 : ( { ( 𝐼 + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ) ⟶ ( { 1 } ∪ { 0 } ) ∧ ( { 1 } ∪ { 0 } ) ⊆ ℝ ) → 𝑄 : ( { ( 𝐼 + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ) ⟶ ℝ )
23 14 21 22 mp2an ⊢ 𝑄 : ( { ( 𝐼 + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ) ⟶ ℝ
24 fznatpl1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝐼 + 1 ) ∈ ( 1 ... 𝑁 ) )
25 24 snssd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → { ( 𝐼 + 1 ) } ⊆ ( 1 ... 𝑁 ) )
26 undif ⊢ ( { ( 𝐼 + 1 ) } ⊆ ( 1 ... 𝑁 ) ↔ ( { ( 𝐼 + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ) = ( 1 ... 𝑁 ) )
27 25 26 sylib ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( { ( 𝐼 + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ) = ( 1 ... 𝑁 ) )
28 27 feq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑄 : ( { ( 𝐼 + 1 ) } ∪ ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ) ⟶ ℝ ↔ 𝑄 : ( 1 ... 𝑁 ) ⟶ ℝ ) )
29 23 28 mpbii ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑄 : ( 1 ... 𝑁 ) ⟶ ℝ )
30 elee ⊢ ( 𝑁 ∈ ℕ → ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ↔ 𝑄 : ( 1 ... 𝑁 ) ⟶ ℝ ) )
31 30 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ↔ 𝑄 : ( 1 ... 𝑁 ) ⟶ ℝ ) )
32 29 31 mpbird ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) )