Metamath Proof Explorer

Theorem naddcnfid2

Description: Identity law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 3-Jan-2025)

Ref Expression
Assertion naddcnfid2 ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝐹 ∈ 𝑆 ) → ( ( 𝑋 × { ∅ } ) ∘f +o 𝐹 ) = 𝐹 )

Proof

Step Hyp Ref Expression
1 peano1 ⊢ ∅ ∈ ω
2 fconst6g ⊢ ( ∅ ∈ ω → ( 𝑋 × { ∅ } ) : 𝑋 ⟶ ω )
3 1 2 mp1i ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝑋 × { ∅ } ) : 𝑋 ⟶ ω )
4 simpl ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → 𝑋 ∈ On )
5 1 a1i ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ∅ ∈ ω )
6 4 5 fczfsuppd ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝑋 × { ∅ } ) finSupp ∅ )
7 simpr ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → 𝑆 = dom ( ω CNF 𝑋 ) )
8 7 eleq2d ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( ( 𝑋 × { ∅ } ) ∈ 𝑆 ↔ ( 𝑋 × { ∅ } ) ∈ dom ( ω CNF 𝑋 ) ) )
9 eqid ⊢ dom ( ω CNF 𝑋 ) = dom ( ω CNF 𝑋 )
10 omelon ⊢ ω ∈ On
11 10 a1i ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ω ∈ On )
12 9 11 4 cantnfs ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( ( 𝑋 × { ∅ } ) ∈ dom ( ω CNF 𝑋 ) ↔ ( ( 𝑋 × { ∅ } ) : 𝑋 ⟶ ω ∧ ( 𝑋 × { ∅ } ) finSupp ∅ ) ) )
13 8 12 bitrd ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( ( 𝑋 × { ∅ } ) ∈ 𝑆 ↔ ( ( 𝑋 × { ∅ } ) : 𝑋 ⟶ ω ∧ ( 𝑋 × { ∅ } ) finSupp ∅ ) ) )
14 3 6 13 mpbir2and ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝑋 × { ∅ } ) ∈ 𝑆 )
15 naddcnfcom ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( ( 𝑋 × { ∅ } ) ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) ) → ( ( 𝑋 × { ∅ } ) ∘f +o 𝐹 ) = ( 𝐹 ∘f +o ( 𝑋 × { ∅ } ) ) )
16 15 ex ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( ( ( 𝑋 × { ∅ } ) ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ( ( 𝑋 × { ∅ } ) ∘f +o 𝐹 ) = ( 𝐹 ∘f +o ( 𝑋 × { ∅ } ) ) ) )
17 14 16 mpand ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝐹 ∈ 𝑆 → ( ( 𝑋 × { ∅ } ) ∘f +o 𝐹 ) = ( 𝐹 ∘f +o ( 𝑋 × { ∅ } ) ) ) )
18 17 imp ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝐹 ∈ 𝑆 ) → ( ( 𝑋 × { ∅ } ) ∘f +o 𝐹 ) = ( 𝐹 ∘f +o ( 𝑋 × { ∅ } ) ) )
19 naddcnfid1 ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝐹 ∈ 𝑆 ) → ( 𝐹 ∘f +o ( 𝑋 × { ∅ } ) ) = 𝐹 )
20 18 19 eqtrd ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝐹 ∈ 𝑆 ) → ( ( 𝑋 × { ∅ } ) ∘f +o 𝐹 ) = 𝐹 )