Metamath Proof Explorer

Theorem ofoacom

Description: Component-wise addition of natural numnber-yielding functions commutes. (Contributed by RP, 5-Jan-2025)

Ref Expression
Assertion ofoacom ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ∈ ( ω ↑m 𝐴 ) ∧ 𝐺 ∈ ( ω ↑m 𝐴 ) ) ) → ( 𝐹 ∘f +o 𝐺 ) = ( 𝐺 ∘f +o 𝐹 ) )

Proof

Step Hyp Ref Expression
1 elmapfn ⊢ ( 𝐹 ∈ ( ω ↑m 𝐴 ) → 𝐹 Fn 𝐴 )
2 1 ad2antrl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ∈ ( ω ↑m 𝐴 ) ∧ 𝐺 ∈ ( ω ↑m 𝐴 ) ) ) → 𝐹 Fn 𝐴 )
3 elmapfn ⊢ ( 𝐺 ∈ ( ω ↑m 𝐴 ) → 𝐺 Fn 𝐴 )
4 3 ad2antll ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ∈ ( ω ↑m 𝐴 ) ∧ 𝐺 ∈ ( ω ↑m 𝐴 ) ) ) → 𝐺 Fn 𝐴 )
5 simpl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ∈ ( ω ↑m 𝐴 ) ∧ 𝐺 ∈ ( ω ↑m 𝐴 ) ) ) → 𝐴 ∈ 𝑉 )
6 inidm ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
7 2 4 5 5 6 offn ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ∈ ( ω ↑m 𝐴 ) ∧ 𝐺 ∈ ( ω ↑m 𝐴 ) ) ) → ( 𝐹 ∘f +o 𝐺 ) Fn 𝐴 )
8 4 2 5 5 6 offn ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ∈ ( ω ↑m 𝐴 ) ∧ 𝐺 ∈ ( ω ↑m 𝐴 ) ) ) → ( 𝐺 ∘f +o 𝐹 ) Fn 𝐴 )
9 elmapi ⊢ ( 𝐹 ∈ ( ω ↑m 𝐴 ) → 𝐹 : 𝐴 ⟶ ω )
10 9 ad2antrl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ∈ ( ω ↑m 𝐴 ) ∧ 𝐺 ∈ ( ω ↑m 𝐴 ) ) ) → 𝐹 : 𝐴 ⟶ ω )
11 10 ffvelcdmda ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ∈ ( ω ↑m 𝐴 ) ∧ 𝐺 ∈ ( ω ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑎 ) ∈ ω )
12 elmapi ⊢ ( 𝐺 ∈ ( ω ↑m 𝐴 ) → 𝐺 : 𝐴 ⟶ ω )
13 12 ad2antll ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ∈ ( ω ↑m 𝐴 ) ∧ 𝐺 ∈ ( ω ↑m 𝐴 ) ) ) → 𝐺 : 𝐴 ⟶ ω )
14 13 ffvelcdmda ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ∈ ( ω ↑m 𝐴 ) ∧ 𝐺 ∈ ( ω ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑎 ) ∈ ω )
15 nnacom ⊢ ( ( ( 𝐹 ‘ 𝑎 ) ∈ ω ∧ ( 𝐺 ‘ 𝑎 ) ∈ ω ) → ( ( 𝐹 ‘ 𝑎 ) +o ( 𝐺 ‘ 𝑎 ) ) = ( ( 𝐺 ‘ 𝑎 ) +o ( 𝐹 ‘ 𝑎 ) ) )
16 11 14 15 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ∈ ( ω ↑m 𝐴 ) ∧ 𝐺 ∈ ( ω ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑎 ) +o ( 𝐺 ‘ 𝑎 ) ) = ( ( 𝐺 ‘ 𝑎 ) +o ( 𝐹 ‘ 𝑎 ) ) )
17 2 4 jca ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ∈ ( ω ↑m 𝐴 ) ∧ 𝐺 ∈ ( ω ↑m 𝐴 ) ) ) → ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) )
18 5 anim1i ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ∈ ( ω ↑m 𝐴 ) ∧ 𝐺 ∈ ( ω ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐴 ∈ 𝑉 ∧ 𝑎 ∈ 𝐴 ) )
19 fnfvof ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝑎 ∈ 𝐴 ) ) → ( ( 𝐹 ∘f +o 𝐺 ) ‘ 𝑎 ) = ( ( 𝐹 ‘ 𝑎 ) +o ( 𝐺 ‘ 𝑎 ) ) )
20 17 18 19 syl2an2r ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ∈ ( ω ↑m 𝐴 ) ∧ 𝐺 ∈ ( ω ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝐹 ∘f +o 𝐺 ) ‘ 𝑎 ) = ( ( 𝐹 ‘ 𝑎 ) +o ( 𝐺 ‘ 𝑎 ) ) )
21 4 2 jca ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ∈ ( ω ↑m 𝐴 ) ∧ 𝐺 ∈ ( ω ↑m 𝐴 ) ) ) → ( 𝐺 Fn 𝐴 ∧ 𝐹 Fn 𝐴 ) )
22 fnfvof ⊢ ( ( ( 𝐺 Fn 𝐴 ∧ 𝐹 Fn 𝐴 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝑎 ∈ 𝐴 ) ) → ( ( 𝐺 ∘f +o 𝐹 ) ‘ 𝑎 ) = ( ( 𝐺 ‘ 𝑎 ) +o ( 𝐹 ‘ 𝑎 ) ) )
23 21 18 22 syl2an2r ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ∈ ( ω ↑m 𝐴 ) ∧ 𝐺 ∈ ( ω ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝐺 ∘f +o 𝐹 ) ‘ 𝑎 ) = ( ( 𝐺 ‘ 𝑎 ) +o ( 𝐹 ‘ 𝑎 ) ) )
24 16 20 23 3eqtr4d ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ∈ ( ω ↑m 𝐴 ) ∧ 𝐺 ∈ ( ω ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝐹 ∘f +o 𝐺 ) ‘ 𝑎 ) = ( ( 𝐺 ∘f +o 𝐹 ) ‘ 𝑎 ) )
25 7 8 24 eqfnfvd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ∈ ( ω ↑m 𝐴 ) ∧ 𝐺 ∈ ( ω ↑m 𝐴 ) ) ) → ( 𝐹 ∘f +o 𝐺 ) = ( 𝐺 ∘f +o 𝐹 ) )