Metamath Proof Explorer

Theorem axlowdimlem5

Description: Lemma for axlowdim . Show that a particular union is a point in Euclidean space. (Contributed by Scott Fenton, 29-Jun-2013)

Ref Expression
Hypotheses axlowdimlem4.1 
|- A e. RR
axlowdimlem4.2 
|- B e. RR
Assertion axlowdimlem5 
|- ( N e. ( ZZ>= ` 2 ) -> ( { <. 1 , A >. , <. 2 , B >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )

Proof

Step Hyp Ref Expression
1 axlowdimlem4.1 
 |-  A e. RR
2 axlowdimlem4.2 
 |-  B e. RR
3 1 2 axlowdimlem4 
 |-  { <. 1 , A >. , <. 2 , B >. } : ( 1 ... 2 ) --> RR
4 axlowdimlem1 
 |-  ( ( 3 ... N ) X. { 0 } ) : ( 3 ... N ) --> RR
5 3 4 pm3.2i 
 |-  ( { <. 1 , A >. , <. 2 , B >. } : ( 1 ... 2 ) --> RR /\ ( ( 3 ... N ) X. { 0 } ) : ( 3 ... N ) --> RR )
6 axlowdimlem2 
 |-  ( ( 1 ... 2 ) i^i ( 3 ... N ) ) = (/)
7 fun2 
 |-  ( ( ( { <. 1 , A >. , <. 2 , B >. } : ( 1 ... 2 ) --> RR /\ ( ( 3 ... N ) X. { 0 } ) : ( 3 ... N ) --> RR ) /\ ( ( 1 ... 2 ) i^i ( 3 ... N ) ) = (/) ) -> ( { <. 1 , A >. , <. 2 , B >. } u. ( ( 3 ... N ) X. { 0 } ) ) : ( ( 1 ... 2 ) u. ( 3 ... N ) ) --> RR )
8 5 6 7 mp2an 
 |-  ( { <. 1 , A >. , <. 2 , B >. } u. ( ( 3 ... N ) X. { 0 } ) ) : ( ( 1 ... 2 ) u. ( 3 ... N ) ) --> RR
9 axlowdimlem3 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 1 ... N ) = ( ( 1 ... 2 ) u. ( 3 ... N ) ) )
10 9 feq2d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( { <. 1 , A >. , <. 2 , B >. } u. ( ( 3 ... N ) X. { 0 } ) ) : ( 1 ... N ) --> RR <-> ( { <. 1 , A >. , <. 2 , B >. } u. ( ( 3 ... N ) X. { 0 } ) ) : ( ( 1 ... 2 ) u. ( 3 ... N ) ) --> RR ) )
11 8 10 mpbiri 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( { <. 1 , A >. , <. 2 , B >. } u. ( ( 3 ... N ) X. { 0 } ) ) : ( 1 ... N ) --> RR )
12 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
13 elee 
 |-  ( N e. NN -> ( ( { <. 1 , A >. , <. 2 , B >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) <-> ( { <. 1 , A >. , <. 2 , B >. } u. ( ( 3 ... N ) X. { 0 } ) ) : ( 1 ... N ) --> RR ) )
14 12 13 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( { <. 1 , A >. , <. 2 , B >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) <-> ( { <. 1 , A >. , <. 2 , B >. } u. ( ( 3 ... N ) X. { 0 } ) ) : ( 1 ... N ) --> RR ) )
15 11 14 mpbird 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( { <. 1 , A >. , <. 2 , B >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )