Metamath Proof Explorer

Theorem naddcnfid1

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

Ref Expression
Assertion naddcnfid1 ( ( ( 𝑋 ∈ 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 7 eleq2d ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝐹 ∈ 𝑆 ↔ 𝐹 ∈ dom ( ω CNF 𝑋 ) ) )
16 9 11 4 cantnfs ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝐹 ∈ dom ( ω CNF 𝑋 ) ↔ ( 𝐹 : 𝑋 ⟶ ω ∧ 𝐹 finSupp ∅ ) ) )
17 15 16 bitrd ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 : 𝑋 ⟶ ω ∧ 𝐹 finSupp ∅ ) ) )
18 17 simprbda ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝐹 ∈ 𝑆 ) → 𝐹 : 𝑋 ⟶ ω )
19 18 ffnd ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝐹 ∈ 𝑆 ) → 𝐹 Fn 𝑋 )
20 19 adantr ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) → 𝐹 Fn 𝑋 )
21 2 ffnd ⊢ ( ∅ ∈ ω → ( 𝑋 × { ∅ } ) Fn 𝑋 )
22 1 21 mp1i ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) → ( 𝑋 × { ∅ } ) Fn 𝑋 )
23 simplll ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) → 𝑋 ∈ On )
24 inidm ⊢ ( 𝑋 ∩ 𝑋 ) = 𝑋
25 20 22 23 23 24 offn ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) → ( 𝐹 ∘f +o ( 𝑋 × { ∅ } ) ) Fn 𝑋 )
26 20 adantr ⊢ ( ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑋 ) → 𝐹 Fn 𝑋 )
27 1 21 mp1i ⊢ ( ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑋 × { ∅ } ) Fn 𝑋 )
28 simp-4l ⊢ ( ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑋 ∈ On )
29 simpr ⊢ ( ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
30 fnfvof ⊢ ( ( ( 𝐹 Fn 𝑋 ∧ ( 𝑋 × { ∅ } ) Fn 𝑋 ) ∧ ( 𝑋 ∈ On ∧ 𝑥 ∈ 𝑋 ) ) → ( ( 𝐹 ∘f +o ( 𝑋 × { ∅ } ) ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) +o ( ( 𝑋 × { ∅ } ) ‘ 𝑥 ) ) )
31 26 27 28 29 30 syl22anc ⊢ ( ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ∘f +o ( 𝑋 × { ∅ } ) ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) +o ( ( 𝑋 × { ∅ } ) ‘ 𝑥 ) ) )
32 fvconst2g ⊢ ( ( ∅ ∈ ω ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑋 × { ∅ } ) ‘ 𝑥 ) = ∅ )
33 1 29 32 sylancr ⊢ ( ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑋 × { ∅ } ) ‘ 𝑥 ) = ∅ )
34 33 oveq2d ⊢ ( ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) +o ( ( 𝑋 × { ∅ } ) ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) +o ∅ ) )
35 18 adantr ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) → 𝐹 : 𝑋 ⟶ ω )
36 35 ffvelcdmda ⊢ ( ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ω )
37 nna0 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ω → ( ( 𝐹 ‘ 𝑥 ) +o ∅ ) = ( 𝐹 ‘ 𝑥 ) )
38 36 37 syl ⊢ ( ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) +o ∅ ) = ( 𝐹 ‘ 𝑥 ) )
39 31 34 38 3eqtrd ⊢ ( ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ∘f +o ( 𝑋 × { ∅ } ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
40 25 20 39 eqfnfvd ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝐹 ∈ 𝑆 ) ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) → ( 𝐹 ∘f +o ( 𝑋 × { ∅ } ) ) = 𝐹 )
41 14 40 mpidan ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝐹 ∈ 𝑆 ) → ( 𝐹 ∘f +o ( 𝑋 × { ∅ } ) ) = 𝐹 )