Theorem ofcs1

Description: Letterwise operations on a single letter word. (Contributed by Thierry Arnoux, 7-Oct-2018)

	Ref	Expression
Assertion	ofcs1	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) → ( ⟨“ 𝐴 ”⟩ ∘f/c 𝑅 𝐵 ) = ⟨“ ( 𝐴 𝑅 𝐵 ) ”⟩ )

Proof

Step	Hyp	Ref	Expression
1		snex	⊢ { 0 } ∈ V
2	1	a1i	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) → { 0 } ∈ V )
3		simpr	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) → 𝐵 ∈ 𝑇 )
4		simpll	⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ∧ 𝑖 ∈ { 0 } ) → 𝐴 ∈ 𝑆 )
5		s1val	⊢ ( 𝐴 ∈ 𝑆 → ⟨“ 𝐴 ”⟩ = { ⟨ 0 , 𝐴 ⟩ } )
6		0nn0	⊢ 0 ∈ ℕ0
7		fmptsn	⊢ ( ( 0 ∈ ℕ0 ∧ 𝐴 ∈ 𝑆 ) → { ⟨ 0 , 𝐴 ⟩ } = ( 𝑖 ∈ { 0 } ↦ 𝐴 ) )
8	6 7	mpan	⊢ ( 𝐴 ∈ 𝑆 → { ⟨ 0 , 𝐴 ⟩ } = ( 𝑖 ∈ { 0 } ↦ 𝐴 ) )
9	5 8	eqtrd	⊢ ( 𝐴 ∈ 𝑆 → ⟨“ 𝐴 ”⟩ = ( 𝑖 ∈ { 0 } ↦ 𝐴 ) )
10	9	adantr	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) → ⟨“ 𝐴 ”⟩ = ( 𝑖 ∈ { 0 } ↦ 𝐴 ) )
11	2 3 4 10	ofcfval2	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) → ( ⟨“ 𝐴 ”⟩ ∘f/c 𝑅 𝐵 ) = ( 𝑖 ∈ { 0 } ↦ ( 𝐴 𝑅 𝐵 ) ) )
12		ovex	⊢ ( 𝐴 𝑅 𝐵 ) ∈ V
13		s1val	⊢ ( ( 𝐴 𝑅 𝐵 ) ∈ V → ⟨“ ( 𝐴 𝑅 𝐵 ) ”⟩ = { ⟨ 0 , ( 𝐴 𝑅 𝐵 ) ⟩ } )
14	12 13	ax-mp	⊢ ⟨“ ( 𝐴 𝑅 𝐵 ) ”⟩ = { ⟨ 0 , ( 𝐴 𝑅 𝐵 ) ⟩ }
15		fmptsn	⊢ ( ( 0 ∈ ℕ0 ∧ ( 𝐴 𝑅 𝐵 ) ∈ V ) → { ⟨ 0 , ( 𝐴 𝑅 𝐵 ) ⟩ } = ( 𝑖 ∈ { 0 } ↦ ( 𝐴 𝑅 𝐵 ) ) )
16	6 12 15	mp2an	⊢ { ⟨ 0 , ( 𝐴 𝑅 𝐵 ) ⟩ } = ( 𝑖 ∈ { 0 } ↦ ( 𝐴 𝑅 𝐵 ) )
17	14 16	eqtri	⊢ ⟨“ ( 𝐴 𝑅 𝐵 ) ”⟩ = ( 𝑖 ∈ { 0 } ↦ ( 𝐴 𝑅 𝐵 ) )
18	11 17	eqtr4di	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) → ( ⟨“ 𝐴 ”⟩ ∘f/c 𝑅 𝐵 ) = ⟨“ ( 𝐴 𝑅 𝐵 ) ”⟩ )