Theorem axlowdimlem11

Description: Lemma for axlowdim . Calculate the value of Q at its distinguished point. (Contributed by Scott Fenton, 21-Apr-2013)

	Ref	Expression
Hypothesis	axlowdimlem10.1	|- Q = ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) )
Assertion	axlowdimlem11	|- ( Q ` ( I + 1 ) ) = 1

Proof

Step	Hyp	Ref	Expression
1		axlowdimlem10.1	|- Q = ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) )
2	1	fveq1i	|- ( Q ` ( I + 1 ) ) = ( ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) ` ( I + 1 ) )
3		ovex	|- ( I + 1 ) e. _V
4		1ex	|- 1 e. _V
5	3 4	fnsn	|- { <. ( I + 1 ) , 1 >. } Fn { ( I + 1 ) }
6		c0ex	|- 0 e. _V
7	6	fconst	|- ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) : ( ( 1 ... N ) \ { ( I + 1 ) } ) --> { 0 }
8		ffn	|- ( ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) : ( ( 1 ... N ) \ { ( I + 1 ) } ) --> { 0 } -> ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) Fn ( ( 1 ... N ) \ { ( I + 1 ) } ) )
9	7 8	ax-mp	|- ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) Fn ( ( 1 ... N ) \ { ( I + 1 ) } )
10		disjdif	|- ( { ( I + 1 ) } i^i ( ( 1 ... N ) \ { ( I + 1 ) } ) ) = (/)
11	3	snid	|- ( I + 1 ) e. { ( I + 1 ) }
12	10 11	pm3.2i	|- ( ( { ( I + 1 ) } i^i ( ( 1 ... N ) \ { ( I + 1 ) } ) ) = (/) /\ ( I + 1 ) e. { ( I + 1 ) } )
13		fvun1	|- ( ( { <. ( I + 1 ) , 1 >. } Fn { ( I + 1 ) } /\ ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) Fn ( ( 1 ... N ) \ { ( I + 1 ) } ) /\ ( ( { ( I + 1 ) } i^i ( ( 1 ... N ) \ { ( I + 1 ) } ) ) = (/) /\ ( I + 1 ) e. { ( I + 1 ) } ) ) -> ( ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) ` ( I + 1 ) ) = ( { <. ( I + 1 ) , 1 >. } ` ( I + 1 ) ) )
14	5 9 12 13	mp3an	|- ( ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) ` ( I + 1 ) ) = ( { <. ( I + 1 ) , 1 >. } ` ( I + 1 ) )
15	3 4	fvsn	|- ( { <. ( I + 1 ) , 1 >. } ` ( I + 1 ) ) = 1
16	2 14 15	3eqtri	|- ( Q ` ( I + 1 ) ) = 1