Metamath Proof Explorer

Theorem naddcnfass

Description: Component-wise addition of Cantor normal forms is associative. (Contributed by RP, 3-Jan-2025)

Ref Expression
Assertion naddcnfass ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) → ( ( 𝐹 ∘f +o 𝐺 ) ∘f +o 𝐻 ) = ( 𝐹 ∘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 9 ffnd ⊢ ( ( 𝐹 : 𝑋 ⟶ ω ∧ 𝐹 finSupp ∅ ) → 𝐹 Fn 𝑋 )
11 8 10 biimtrdi ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝐹 ∈ 𝑆 → 𝐹 Fn 𝑋 ) )
12 simp1 ⊢ ( ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) → 𝐹 ∈ 𝑆 )
13 11 12 impel ⊢ ( ( ( 𝑋 ∈ 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 17 ffnd ⊢ ( ( 𝐺 : 𝑋 ⟶ ω ∧ 𝐺 finSupp ∅ ) → 𝐺 Fn 𝑋 )
19 16 18 biimtrdi ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝐺 ∈ 𝑆 → 𝐺 Fn 𝑋 ) )
20 simp2 ⊢ ( ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) → 𝐺 ∈ 𝑆 )
21 19 20 impel ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) → 𝐺 Fn 𝑋 )
22 6 adantr ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) → 𝑋 ∈ On )
23 inidm ⊢ ( 𝑋 ∩ 𝑋 ) = 𝑋
24 13 21 22 22 23 offn ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) → ( 𝐹 ∘f +o 𝐺 ) Fn 𝑋 )
25 1 eleq2d ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝐻 ∈ 𝑆 ↔ 𝐻 ∈ dom ( ω CNF 𝑋 ) ) )
26 3 5 6 cantnfs ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝐻 ∈ dom ( ω CNF 𝑋 ) ↔ ( 𝐻 : 𝑋 ⟶ ω ∧ 𝐻 finSupp ∅ ) ) )
27 25 26 bitrd ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝐻 ∈ 𝑆 ↔ ( 𝐻 : 𝑋 ⟶ ω ∧ 𝐻 finSupp ∅ ) ) )
28 simpl ⊢ ( ( 𝐻 : 𝑋 ⟶ ω ∧ 𝐻 finSupp ∅ ) → 𝐻 : 𝑋 ⟶ ω )
29 28 ffnd ⊢ ( ( 𝐻 : 𝑋 ⟶ ω ∧ 𝐻 finSupp ∅ ) → 𝐻 Fn 𝑋 )
30 27 29 biimtrdi ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝐻 ∈ 𝑆 → 𝐻 Fn 𝑋 ) )
31 simp3 ⊢ ( ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) → 𝐻 ∈ 𝑆 )
32 30 31 impel ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) → 𝐻 Fn 𝑋 )
33 24 32 22 22 23 offn ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) → ( ( 𝐹 ∘f +o 𝐺 ) ∘f +o 𝐻 ) Fn 𝑋 )
34 21 32 22 22 23 offn ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) → ( 𝐺 ∘f +o 𝐻 ) Fn 𝑋 )
35 13 34 22 22 23 offn ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) → ( 𝐹 ∘f +o ( 𝐺 ∘f +o 𝐻 ) ) Fn 𝑋 )
36 8 9 biimtrdi ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝐹 ∈ 𝑆 → 𝐹 : 𝑋 ⟶ ω ) )
37 36 12 impel ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) → 𝐹 : 𝑋 ⟶ ω )
38 37 ffvelcdmda ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ω )
39 16 17 biimtrdi ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝐺 ∈ 𝑆 → 𝐺 : 𝑋 ⟶ ω ) )
40 39 20 impel ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) → 𝐺 : 𝑋 ⟶ ω )
41 40 ffvelcdmda ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝐺 ‘ 𝑥 ) ∈ ω )
42 27 28 biimtrdi ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝐻 ∈ 𝑆 → 𝐻 : 𝑋 ⟶ ω ) )
43 42 31 impel ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) → 𝐻 : 𝑋 ⟶ ω )
44 43 ffvelcdmda ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝐻 ‘ 𝑥 ) ∈ ω )
45 nnaass ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ω ∧ ( 𝐺 ‘ 𝑥 ) ∈ ω ∧ ( 𝐻 ‘ 𝑥 ) ∈ ω ) → ( ( ( 𝐹 ‘ 𝑥 ) +o ( 𝐺 ‘ 𝑥 ) ) +o ( 𝐻 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) +o ( ( 𝐺 ‘ 𝑥 ) +o ( 𝐻 ‘ 𝑥 ) ) ) )
46 38 41 44 45 syl3anc ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝐹 ‘ 𝑥 ) +o ( 𝐺 ‘ 𝑥 ) ) +o ( 𝐻 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) +o ( ( 𝐺 ‘ 𝑥 ) +o ( 𝐻 ‘ 𝑥 ) ) ) )
47 13 adantr ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝐹 Fn 𝑋 )
48 21 adantr ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝐺 Fn 𝑋 )
49 22 anim1i ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑋 ∈ On ∧ 𝑥 ∈ 𝑋 ) )
50 fnfvof ⊢ ( ( ( 𝐹 Fn 𝑋 ∧ 𝐺 Fn 𝑋 ) ∧ ( 𝑋 ∈ On ∧ 𝑥 ∈ 𝑋 ) ) → ( ( 𝐹 ∘f +o 𝐺 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) +o ( 𝐺 ‘ 𝑥 ) ) )
51 47 48 49 50 syl21anc ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ∘f +o 𝐺 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) +o ( 𝐺 ‘ 𝑥 ) ) )
52 51 oveq1d ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝐹 ∘f +o 𝐺 ) ‘ 𝑥 ) +o ( 𝐻 ‘ 𝑥 ) ) = ( ( ( 𝐹 ‘ 𝑥 ) +o ( 𝐺 ‘ 𝑥 ) ) +o ( 𝐻 ‘ 𝑥 ) ) )
53 32 adantr ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝐻 Fn 𝑋 )
54 fnfvof ⊢ ( ( ( 𝐺 Fn 𝑋 ∧ 𝐻 Fn 𝑋 ) ∧ ( 𝑋 ∈ On ∧ 𝑥 ∈ 𝑋 ) ) → ( ( 𝐺 ∘f +o 𝐻 ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) +o ( 𝐻 ‘ 𝑥 ) ) )
55 48 53 49 54 syl21anc ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐺 ∘f +o 𝐻 ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) +o ( 𝐻 ‘ 𝑥 ) ) )
56 55 oveq2d ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) +o ( ( 𝐺 ∘f +o 𝐻 ) ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) +o ( ( 𝐺 ‘ 𝑥 ) +o ( 𝐻 ‘ 𝑥 ) ) ) )
57 46 52 56 3eqtr4d ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝐹 ∘f +o 𝐺 ) ‘ 𝑥 ) +o ( 𝐻 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) +o ( ( 𝐺 ∘f +o 𝐻 ) ‘ 𝑥 ) ) )
58 24 adantr ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ∘f +o 𝐺 ) Fn 𝑋 )
59 fnfvof ⊢ ( ( ( ( 𝐹 ∘f +o 𝐺 ) Fn 𝑋 ∧ 𝐻 Fn 𝑋 ) ∧ ( 𝑋 ∈ On ∧ 𝑥 ∈ 𝑋 ) ) → ( ( ( 𝐹 ∘f +o 𝐺 ) ∘f +o 𝐻 ) ‘ 𝑥 ) = ( ( ( 𝐹 ∘f +o 𝐺 ) ‘ 𝑥 ) +o ( 𝐻 ‘ 𝑥 ) ) )
60 58 53 49 59 syl21anc ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝐹 ∘f +o 𝐺 ) ∘f +o 𝐻 ) ‘ 𝑥 ) = ( ( ( 𝐹 ∘f +o 𝐺 ) ‘ 𝑥 ) +o ( 𝐻 ‘ 𝑥 ) ) )
61 34 adantr ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝐺 ∘f +o 𝐻 ) Fn 𝑋 )
62 fnfvof ⊢ ( ( ( 𝐹 Fn 𝑋 ∧ ( 𝐺 ∘f +o 𝐻 ) Fn 𝑋 ) ∧ ( 𝑋 ∈ On ∧ 𝑥 ∈ 𝑋 ) ) → ( ( 𝐹 ∘f +o ( 𝐺 ∘f +o 𝐻 ) ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) +o ( ( 𝐺 ∘f +o 𝐻 ) ‘ 𝑥 ) ) )
63 47 61 49 62 syl21anc ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ∘f +o ( 𝐺 ∘f +o 𝐻 ) ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) +o ( ( 𝐺 ∘f +o 𝐻 ) ‘ 𝑥 ) ) )
64 57 60 63 3eqtr4d ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝐹 ∘f +o 𝐺 ) ∘f +o 𝐻 ) ‘ 𝑥 ) = ( ( 𝐹 ∘f +o ( 𝐺 ∘f +o 𝐻 ) ) ‘ 𝑥 ) )
65 33 35 64 eqfnfvd ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆 ) ) → ( ( 𝐹 ∘f +o 𝐺 ) ∘f +o 𝐻 ) = ( 𝐹 ∘f +o ( 𝐺 ∘f +o 𝐻 ) ) )