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 
|- ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ F e. S ) -> ( ( X X. { (/) } ) oF +o F ) = F )

Proof

Step Hyp Ref Expression
1 peano1 
 |-  (/) e. _om
2 fconst6g 
 |-  ( (/) e. _om -> ( X X. { (/) } ) : X --> _om )
3 1 2 mp1i 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( X X. { (/) } ) : X --> _om )
4 simpl 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> X e. On )
5 1 a1i 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> (/) e. _om )
6 4 5 fczfsuppd 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( X X. { (/) } ) finSupp (/) )
7 simpr 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> S = dom ( _om CNF X ) )
8 7 eleq2d 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( ( X X. { (/) } ) e. S <-> ( X X. { (/) } ) e. dom ( _om CNF X ) ) )
9 eqid 
 |-  dom ( _om CNF X ) = dom ( _om CNF X )
10 omelon 
 |-  _om e. On
11 10 a1i 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> _om e. On )
12 9 11 4 cantnfs 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( ( X X. { (/) } ) e. dom ( _om CNF X ) <-> ( ( X X. { (/) } ) : X --> _om /\ ( X X. { (/) } ) finSupp (/) ) ) )
13 8 12 bitrd 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( ( X X. { (/) } ) e. S <-> ( ( X X. { (/) } ) : X --> _om /\ ( X X. { (/) } ) finSupp (/) ) ) )
14 3 6 13 mpbir2and 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( X X. { (/) } ) e. S )
15 naddcnfcom 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( ( X X. { (/) } ) e. S /\ F e. S ) ) -> ( ( X X. { (/) } ) oF +o F ) = ( F oF +o ( X X. { (/) } ) ) )
16 15 ex 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( ( ( X X. { (/) } ) e. S /\ F e. S ) -> ( ( X X. { (/) } ) oF +o F ) = ( F oF +o ( X X. { (/) } ) ) ) )
17 14 16 mpand 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( F e. S -> ( ( X X. { (/) } ) oF +o F ) = ( F oF +o ( X X. { (/) } ) ) ) )
18 17 imp 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ F e. S ) -> ( ( X X. { (/) } ) oF +o F ) = ( F oF +o ( X X. { (/) } ) ) )
19 naddcnfid1 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ F e. S ) -> ( F oF +o ( X X. { (/) } ) ) = F )
20 18 19 eqtrd 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ F e. S ) -> ( ( X X. { (/) } ) oF +o F ) = F )