Theorem s1co

Description: Mapping of a singleton word. (Contributed by Mario Carneiro, 27-Sep-2015) (Revised by Mario Carneiro, 26-Feb-2016)

	Ref	Expression
Assertion	s1co	$$⊢\left(S\in A\wedge F:A⟶B\right)\to F\circ ⟨“S”⟩=⟨“F\left(S\right)”⟩$$

Proof

Step	Hyp	Ref	Expression
1		s1val	$$⊢S\in A\to ⟨“S”⟩=\left\{⟨0,S⟩\right\}$$
2		0cn	$$⊢0\in ℂ$$
3		xpsng	$$⊢\left(0\in ℂ\wedge S\in A\right)\to \left\{0\right\}\times \left\{S\right\}=\left\{⟨0,S⟩\right\}$$
4	2 3	mpan	$$⊢S\in A\to \left\{0\right\}\times \left\{S\right\}=\left\{⟨0,S⟩\right\}$$
5	1 4	eqtr4d	$$⊢S\in A\to ⟨“S”⟩=\left\{0\right\}\times \left\{S\right\}$$
6	5	adantr	$$⊢\left(S\in A\wedge F:A⟶B\right)\to ⟨“S”⟩=\left\{0\right\}\times \left\{S\right\}$$
7	6	coeq2d	$$⊢\left(S\in A\wedge F:A⟶B\right)\to F\circ ⟨“S”⟩=F\circ \left(\left\{0\right\}\times \left\{S\right\}\right)$$
8		fvex	$$⊢F\left(S\right)\in \mathrm{V}$$
9		s1val	$$⊢F\left(S\right)\in \mathrm{V}\to ⟨“F\left(S\right)”⟩=\left\{⟨0,F\left(S\right)⟩\right\}$$
10	8 9	ax-mp	$$⊢⟨“F\left(S\right)”⟩=\left\{⟨0,F\left(S\right)⟩\right\}$$
11		c0ex	$$⊢0\in \mathrm{V}$$
12	11 8	xpsn	$$⊢\left\{0\right\}\times \left\{F\left(S\right)\right\}=\left\{⟨0,F\left(S\right)⟩\right\}$$
13	10 12	eqtr4i	$$⊢⟨“F\left(S\right)”⟩=\left\{0\right\}\times \left\{F\left(S\right)\right\}$$
14		ffn	$$⊢F:A⟶B\to FFnA$$
15		id	$$⊢S\in A\to S\in A$$
16		fcoconst	$$⊢\left(FFnA\wedge S\in A\right)\to F\circ \left(\left\{0\right\}\times \left\{S\right\}\right)=\left\{0\right\}\times \left\{F\left(S\right)\right\}$$
17	14 15 16	syl2anr	$$⊢\left(S\in A\wedge F:A⟶B\right)\to F\circ \left(\left\{0\right\}\times \left\{S\right\}\right)=\left\{0\right\}\times \left\{F\left(S\right)\right\}$$
18	13 17	eqtr4id	$$⊢\left(S\in A\wedge F:A⟶B\right)\to ⟨“F\left(S\right)”⟩=F\circ \left(\left\{0\right\}\times \left\{S\right\}\right)$$
19	7 18	eqtr4d	$$⊢\left(S\in A\wedge F:A⟶B\right)\to F\circ ⟨“S”⟩=⟨“F\left(S\right)”⟩$$