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	⊢ 𝑄 = ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) )
Assertion	axlowdimlem11	⊢ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = 1

Proof

Step	Hyp	Ref	Expression
1		axlowdimlem10.1	⊢ 𝑄 = ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) )
2	1	fveq1i	⊢ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) ) ‘ ( 𝐼 + 1 ) )
3		ovex	⊢ ( 𝐼 + 1 ) ∈ V
4		1ex	⊢ 1 ∈ V
5	3 4	fnsn	⊢ { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } Fn { ( 𝐼 + 1 ) }
6		c0ex	⊢ 0 ∈ V
7	6	fconst	⊢ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) : ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ⟶ { 0 }
8		ffn	⊢ ( ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) : ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ⟶ { 0 } → ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) Fn ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) )
9	7 8	ax-mp	⊢ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) Fn ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } )
10		disjdif	⊢ ( { ( 𝐼 + 1 ) } ∩ ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ) = ∅
11	3	snid	⊢ ( 𝐼 + 1 ) ∈ { ( 𝐼 + 1 ) }
12	10 11	pm3.2i	⊢ ( ( { ( 𝐼 + 1 ) } ∩ ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ) = ∅ ∧ ( 𝐼 + 1 ) ∈ { ( 𝐼 + 1 ) } )
13		fvun1	⊢ ( ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } Fn { ( 𝐼 + 1 ) } ∧ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) Fn ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ∧ ( ( { ( 𝐼 + 1 ) } ∩ ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) ) = ∅ ∧ ( 𝐼 + 1 ) ∈ { ( 𝐼 + 1 ) } ) ) → ( ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) ) ‘ ( 𝐼 + 1 ) ) = ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ‘ ( 𝐼 + 1 ) ) )
14	5 9 12 13	mp3an	⊢ ( ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) ) ‘ ( 𝐼 + 1 ) ) = ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ‘ ( 𝐼 + 1 ) )
15	3 4	fvsn	⊢ ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ‘ ( 𝐼 + 1 ) ) = 1
16	2 14 15	3eqtri	⊢ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = 1