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	⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ⟨“ 𝑆 ”⟩ ) = ⟨“ ( 𝐹 ‘ 𝑆 ) ”⟩ )

Proof

Step	Hyp	Ref	Expression
1		s1val	⊢ ( 𝑆 ∈ 𝐴 → ⟨“ 𝑆 ”⟩ = { ⟨ 0 , 𝑆 ⟩ } )
2		0cn	⊢ 0 ∈ ℂ
3		xpsng	⊢ ( ( 0 ∈ ℂ ∧ 𝑆 ∈ 𝐴 ) → ( { 0 } × { 𝑆 } ) = { ⟨ 0 , 𝑆 ⟩ } )
4	2 3	mpan	⊢ ( 𝑆 ∈ 𝐴 → ( { 0 } × { 𝑆 } ) = { ⟨ 0 , 𝑆 ⟩ } )
5	1 4	eqtr4d	⊢ ( 𝑆 ∈ 𝐴 → ⟨“ 𝑆 ”⟩ = ( { 0 } × { 𝑆 } ) )
6	5	adantr	⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ⟨“ 𝑆 ”⟩ = ( { 0 } × { 𝑆 } ) )
7	6	coeq2d	⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ⟨“ 𝑆 ”⟩ ) = ( 𝐹 ∘ ( { 0 } × { 𝑆 } ) ) )
8		fvex	⊢ ( 𝐹 ‘ 𝑆 ) ∈ V
9		s1val	⊢ ( ( 𝐹 ‘ 𝑆 ) ∈ V → ⟨“ ( 𝐹 ‘ 𝑆 ) ”⟩ = { ⟨ 0 , ( 𝐹 ‘ 𝑆 ) ⟩ } )
10	8 9	ax-mp	⊢ ⟨“ ( 𝐹 ‘ 𝑆 ) ”⟩ = { ⟨ 0 , ( 𝐹 ‘ 𝑆 ) ⟩ }
11		c0ex	⊢ 0 ∈ V
12	11 8	xpsn	⊢ ( { 0 } × { ( 𝐹 ‘ 𝑆 ) } ) = { ⟨ 0 , ( 𝐹 ‘ 𝑆 ) ⟩ }
13	10 12	eqtr4i	⊢ ⟨“ ( 𝐹 ‘ 𝑆 ) ”⟩ = ( { 0 } × { ( 𝐹 ‘ 𝑆 ) } )
14		ffn	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
15		id	⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ 𝐴 )
16		fcoconst	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( 𝐹 ∘ ( { 0 } × { 𝑆 } ) ) = ( { 0 } × { ( 𝐹 ‘ 𝑆 ) } ) )
17	14 15 16	syl2anr	⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ( { 0 } × { 𝑆 } ) ) = ( { 0 } × { ( 𝐹 ‘ 𝑆 ) } ) )
18	13 17	eqtr4id	⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ⟨“ ( 𝐹 ‘ 𝑆 ) ”⟩ = ( 𝐹 ∘ ( { 0 } × { 𝑆 } ) ) )
19	7 18	eqtr4d	⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ⟨“ 𝑆 ”⟩ ) = ⟨“ ( 𝐹 ‘ 𝑆 ) ”⟩ )