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	$$⊢P=\left\{⟨3,-1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)$$
Assertion	axlowdimlem8	$$⊢P\left(3\right)=-1$$

Proof

Step	Hyp	Ref	Expression
1		axlowdimlem7.1	$$⊢P=\left\{⟨3,-1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)$$
2	1	fveq1i	$$⊢P\left(3\right)=\left(\left\{⟨3,-1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)\right)\left(3\right)$$
3		3ex	$$⊢3\in \mathrm{V}$$
4		negex	$$⊢-1\in \mathrm{V}$$
5	3 4	fnsn	$$⊢\left\{⟨3,-1⟩\right\}Fn\left\{3\right\}$$
6		c0ex	$$⊢0\in \mathrm{V}$$
7	6	fconst	$$⊢\left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right):\left(1\dots N\right)\setminus \left\{3\right\}⟶\left\{0\right\}$$
8		ffn	$$⊢\left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right):\left(1\dots N\right)\setminus \left\{3\right\}⟶\left\{0\right\}\to \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)Fn\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)$$
9	7 8	ax-mp	$$⊢\left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)Fn\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)$$
10		disjdif	$$⊢\left\{3\right\}\cap \left(\left(1\dots N\right)\setminus \left\{3\right\}\right)=\varnothing$$
11	3	snid	$$⊢3\in \left\{3\right\}$$
12	10 11	pm3.2i	$$⊢\left(\left\{3\right\}\cap \left(\left(1\dots N\right)\setminus \left\{3\right\}\right)=\varnothing \wedge 3\in \left\{3\right\}\right)$$
13		fvun1	$$⊢\left(\left\{⟨3,-1⟩\right\}Fn\left\{3\right\}\wedge \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)Fn\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\wedge \left(\left\{3\right\}\cap \left(\left(1\dots N\right)\setminus \left\{3\right\}\right)=\varnothing \wedge 3\in \left\{3\right\}\right)\right)\to \left(\left\{⟨3,-1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)\right)\left(3\right)=\left\{⟨3,-1⟩\right\}\left(3\right)$$
14	5 9 12 13	mp3an	$$⊢\left(\left\{⟨3,-1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)\right)\left(3\right)=\left\{⟨3,-1⟩\right\}\left(3\right)$$
15	3 4	fvsn	$$⊢\left\{⟨3,-1⟩\right\}\left(3\right)=-1$$
16	2 14 15	3eqtri	$$⊢P\left(3\right)=-1$$