Metamath Proof Explorer

Theorem naddcnfcom

Description: Component-wise ordinal addition of Cantor normal forms commutes. (Contributed by RP, 2-Jan-2025)

Ref Expression
Assertion naddcnfcom ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) ) → ( 𝐹 ∘f +o 𝐺 ) = ( 𝐺 ∘f +o 𝐹 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → 𝑆 = dom ( ω CNF 𝑋 ) )
2 1 eleq2d ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝐹 ∈ 𝑆 ↔ 𝐹 ∈ dom ( ω CNF 𝑋 ) ) )
3 eqid ⊢ dom ( ω CNF 𝑋 ) = dom ( ω CNF 𝑋 )
4 omelon ⊢ ω ∈ On
5 4 a1i ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ω ∈ On )
6 simpl ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → 𝑋 ∈ On )
7 3 5 6 cantnfs ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝐹 ∈ dom ( ω CNF 𝑋 ) ↔ ( 𝐹 : 𝑋 ⟶ ω ∧ 𝐹 finSupp ∅ ) ) )
8 2 7 bitrd ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 : 𝑋 ⟶ ω ∧ 𝐹 finSupp ∅ ) ) )
9 simpl ⊢ ( ( 𝐹 : 𝑋 ⟶ ω ∧ 𝐹 finSupp ∅ ) → 𝐹 : 𝑋 ⟶ ω )
10 8 9 biimtrdi ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝐹 ∈ 𝑆 → 𝐹 : 𝑋 ⟶ ω ) )
11 simpl ⊢ ( ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) → 𝐹 ∈ 𝑆 )
12 10 11 impel ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) ) → 𝐹 : 𝑋 ⟶ ω )
13 12 ffnd ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) ) → 𝐹 Fn 𝑋 )
14 1 eleq2d ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝐺 ∈ 𝑆 ↔ 𝐺 ∈ dom ( ω CNF 𝑋 ) ) )
15 3 5 6 cantnfs ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝐺 ∈ dom ( ω CNF 𝑋 ) ↔ ( 𝐺 : 𝑋 ⟶ ω ∧ 𝐺 finSupp ∅ ) ) )
16 14 15 bitrd ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝐺 ∈ 𝑆 ↔ ( 𝐺 : 𝑋 ⟶ ω ∧ 𝐺 finSupp ∅ ) ) )
17 simpl ⊢ ( ( 𝐺 : 𝑋 ⟶ ω ∧ 𝐺 finSupp ∅ ) → 𝐺 : 𝑋 ⟶ ω )
18 16 17 biimtrdi ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝐺 ∈ 𝑆 → 𝐺 : 𝑋 ⟶ ω ) )
19 simpr ⊢ ( ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) → 𝐺 ∈ 𝑆 )
20 18 19 impel ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) ) → 𝐺 : 𝑋 ⟶ ω )
21 20 ffnd ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) ) → 𝐺 Fn 𝑋 )
22 simpll ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) ) → 𝑋 ∈ On )
23 inidm ⊢ ( 𝑋 ∩ 𝑋 ) = 𝑋
24 13 21 22 22 23 offn ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) ) → ( 𝐹 ∘f +o 𝐺 ) Fn 𝑋 )
25 21 13 22 22 23 offn ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) ) → ( 𝐺 ∘f +o 𝐹 ) Fn 𝑋 )
26 12 ffvelcdmda ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ω )
27 20 ffvelcdmda ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝐺 ‘ 𝑥 ) ∈ ω )
28 nnacom ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ω ∧ ( 𝐺 ‘ 𝑥 ) ∈ ω ) → ( ( 𝐹 ‘ 𝑥 ) +o ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐺 ‘ 𝑥 ) +o ( 𝐹 ‘ 𝑥 ) ) )
29 26 27 28 syl2anc ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) +o ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐺 ‘ 𝑥 ) +o ( 𝐹 ‘ 𝑥 ) ) )
30 13 adantr ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝐹 Fn 𝑋 )
31 21 adantr ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝐺 Fn 𝑋 )
32 simplll ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑋 ∈ On )
33 simpr ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
34 fnfvof ⊢ ( ( ( 𝐹 Fn 𝑋 ∧ 𝐺 Fn 𝑋 ) ∧ ( 𝑋 ∈ On ∧ 𝑥 ∈ 𝑋 ) ) → ( ( 𝐹 ∘f +o 𝐺 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) +o ( 𝐺 ‘ 𝑥 ) ) )
35 30 31 32 33 34 syl22anc ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ∘f +o 𝐺 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) +o ( 𝐺 ‘ 𝑥 ) ) )
36 fnfvof ⊢ ( ( ( 𝐺 Fn 𝑋 ∧ 𝐹 Fn 𝑋 ) ∧ ( 𝑋 ∈ On ∧ 𝑥 ∈ 𝑋 ) ) → ( ( 𝐺 ∘f +o 𝐹 ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) +o ( 𝐹 ‘ 𝑥 ) ) )
37 31 30 32 33 36 syl22anc ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐺 ∘f +o 𝐹 ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) +o ( 𝐹 ‘ 𝑥 ) ) )
38 29 35 37 3eqtr4d ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ∘f +o 𝐺 ) ‘ 𝑥 ) = ( ( 𝐺 ∘f +o 𝐹 ) ‘ 𝑥 ) )
39 24 25 38 eqfnfvd ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) ) → ( 𝐹 ∘f +o 𝐺 ) = ( 𝐺 ∘f +o 𝐹 ) )