Theorem axlowdimlem8

Description: Lemma for axlowdim . Calculate the value of P at three. (Contributed by Scott Fenton, 21-Apr-2013)

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

Proof

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