This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑅 ⟨“ 𝐵 ”⟩ ) = ⟨“ ( 𝐴 𝑅 𝐵 ) ”⟩ )