Theorem ofs1

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

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

Proof

Step	Hyp	Ref	Expression
1		snex	⊢ { 0 } ∈ V
2	1	a1i	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) → { 0 } ∈ V )
3		simpll	⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ∧ 𝑖 ∈ { 0 } ) → 𝐴 ∈ 𝑆 )
4		simplr	⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ∧ 𝑖 ∈ { 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		s1val	⊢ ( 𝐵 ∈ 𝑇 → ⟨“ 𝐵 ”⟩ = { ⟨ 0 , 𝐵 ⟩ } )
12		fmptsn	⊢ ( ( 0 ∈ ℕ0 ∧ 𝐵 ∈ 𝑇 ) → { ⟨ 0 , 𝐵 ⟩ } = ( 𝑖 ∈ { 0 } ↦ 𝐵 ) )
13	6 12	mpan	⊢ ( 𝐵 ∈ 𝑇 → { ⟨ 0 , 𝐵 ⟩ } = ( 𝑖 ∈ { 0 } ↦ 𝐵 ) )
14	11 13	eqtrd	⊢ ( 𝐵 ∈ 𝑇 → ⟨“ 𝐵 ”⟩ = ( 𝑖 ∈ { 0 } ↦ 𝐵 ) )
15	14	adantl	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) → ⟨“ 𝐵 ”⟩ = ( 𝑖 ∈ { 0 } ↦ 𝐵 ) )
16	2 3 4 10 15	offval2	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) → ( ⟨“ 𝐴 ”⟩ ∘f 𝑅 ⟨“ 𝐵 ”⟩ ) = ( 𝑖 ∈ { 0 } ↦ ( 𝐴 𝑅 𝐵 ) ) )
17		ovex	⊢ ( 𝐴 𝑅 𝐵 ) ∈ V
18		s1val	⊢ ( ( 𝐴 𝑅 𝐵 ) ∈ V → ⟨“ ( 𝐴 𝑅 𝐵 ) ”⟩ = { ⟨ 0 , ( 𝐴 𝑅 𝐵 ) ⟩ } )
19	17 18	ax-mp	⊢ ⟨“ ( 𝐴 𝑅 𝐵 ) ”⟩ = { ⟨ 0 , ( 𝐴 𝑅 𝐵 ) ⟩ }
20		fmptsn	⊢ ( ( 0 ∈ ℕ0 ∧ ( 𝐴 𝑅 𝐵 ) ∈ V ) → { ⟨ 0 , ( 𝐴 𝑅 𝐵 ) ⟩ } = ( 𝑖 ∈ { 0 } ↦ ( 𝐴 𝑅 𝐵 ) ) )
21	6 17 20	mp2an	⊢ { ⟨ 0 , ( 𝐴 𝑅 𝐵 ) ⟩ } = ( 𝑖 ∈ { 0 } ↦ ( 𝐴 𝑅 𝐵 ) )
22	19 21	eqtri	⊢ ⟨“ ( 𝐴 𝑅 𝐵 ) ”⟩ = ( 𝑖 ∈ { 0 } ↦ ( 𝐴 𝑅 𝐵 ) )
23	16 22	eqtr4di	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) → ( ⟨“ 𝐴 ”⟩ ∘f 𝑅 ⟨“ 𝐵 ”⟩ ) = ⟨“ ( 𝐴 𝑅 𝐵 ) ”⟩ )