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

Proof

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