Metamath Proof Explorer

Theorem nnadju

Description: The cardinal and ordinal sums of finite ordinals are equal. For a shorter proof using ax-rep , see nnadjuALT . (Contributed by Paul Chapman, 11-Apr-2009) (Revised by Mario Carneiro, 6-Feb-2013) Avoid ax-rep . (Revised by BTernaryTau, 2-Jul-2024)

Ref Expression
Assertion nnadju 
|- ( ( A e. _om /\ B e. _om ) -> ( card ` ( A |_| B ) ) = ( A +o B ) )

Proof

Step Hyp Ref Expression
1 djueq2 
 |-  ( x = B -> ( A |_| x ) = ( A |_| B ) )
2 oveq2 
 |-  ( x = B -> ( A +o x ) = ( A +o B ) )
3 1 2 breq12d 
 |-  ( x = B -> ( ( A |_| x ) ~~ ( A +o x ) <-> ( A |_| B ) ~~ ( A +o B ) ) )
4 3 imbi2d 
 |-  ( x = B -> ( ( A e. _om -> ( A |_| x ) ~~ ( A +o x ) ) <-> ( A e. _om -> ( A |_| B ) ~~ ( A +o B ) ) ) )
5 djueq2 
 |-  ( x = (/) -> ( A |_| x ) = ( A |_| (/) ) )
6 oveq2 
 |-  ( x = (/) -> ( A +o x ) = ( A +o (/) ) )
7 5 6 breq12d 
 |-  ( x = (/) -> ( ( A |_| x ) ~~ ( A +o x ) <-> ( A |_| (/) ) ~~ ( A +o (/) ) ) )
8 djueq2 
 |-  ( x = y -> ( A |_| x ) = ( A |_| y ) )
9 oveq2 
 |-  ( x = y -> ( A +o x ) = ( A +o y ) )
10 8 9 breq12d 
 |-  ( x = y -> ( ( A |_| x ) ~~ ( A +o x ) <-> ( A |_| y ) ~~ ( A +o y ) ) )
11 djueq2 
 |-  ( x = suc y -> ( A |_| x ) = ( A |_| suc y ) )
12 oveq2 
 |-  ( x = suc y -> ( A +o x ) = ( A +o suc y ) )
13 11 12 breq12d 
 |-  ( x = suc y -> ( ( A |_| x ) ~~ ( A +o x ) <-> ( A |_| suc y ) ~~ ( A +o suc y ) ) )
14 dju0en 
 |-  ( A e. _om -> ( A |_| (/) ) ~~ A )
15 nna0 
 |-  ( A e. _om -> ( A +o (/) ) = A )
16 14 15 breqtrrd 
 |-  ( A e. _om -> ( A |_| (/) ) ~~ ( A +o (/) ) )
17 1oex 
 |-  1o e. _V
18 djuassen 
 |-  ( ( A e. _om /\ y e. _om /\ 1o e. _V ) -> ( ( A |_| y ) |_| 1o ) ~~ ( A |_| ( y |_| 1o ) ) )
19 17 18 mp3an3 
 |-  ( ( A e. _om /\ y e. _om ) -> ( ( A |_| y ) |_| 1o ) ~~ ( A |_| ( y |_| 1o ) ) )
20 enrefg 
 |-  ( A e. _om -> A ~~ A )
21 nnord 
 |-  ( y e. _om -> Ord y )
22 ordirr 
 |-  ( Ord y -> -. y e. y )
23 21 22 syl 
 |-  ( y e. _om -> -. y e. y )
24 dju1en 
 |-  ( ( y e. _om /\ -. y e. y ) -> ( y |_| 1o ) ~~ suc y )
25 23 24 mpdan 
 |-  ( y e. _om -> ( y |_| 1o ) ~~ suc y )
26 djuen 
 |-  ( ( A ~~ A /\ ( y |_| 1o ) ~~ suc y ) -> ( A |_| ( y |_| 1o ) ) ~~ ( A |_| suc y ) )
27 20 25 26 syl2an 
 |-  ( ( A e. _om /\ y e. _om ) -> ( A |_| ( y |_| 1o ) ) ~~ ( A |_| suc y ) )
28 entr 
 |-  ( ( ( ( A |_| y ) |_| 1o ) ~~ ( A |_| ( y |_| 1o ) ) /\ ( A |_| ( y |_| 1o ) ) ~~ ( A |_| suc y ) ) -> ( ( A |_| y ) |_| 1o ) ~~ ( A |_| suc y ) )
29 19 27 28 syl2anc 
 |-  ( ( A e. _om /\ y e. _om ) -> ( ( A |_| y ) |_| 1o ) ~~ ( A |_| suc y ) )
30 29 ensymd 
 |-  ( ( A e. _om /\ y e. _om ) -> ( A |_| suc y ) ~~ ( ( A |_| y ) |_| 1o ) )
31 17 enref 
 |-  1o ~~ 1o
32 djuen 
 |-  ( ( ( A |_| y ) ~~ ( A +o y ) /\ 1o ~~ 1o ) -> ( ( A |_| y ) |_| 1o ) ~~ ( ( A +o y ) |_| 1o ) )
33 31 32 mpan2 
 |-  ( ( A |_| y ) ~~ ( A +o y ) -> ( ( A |_| y ) |_| 1o ) ~~ ( ( A +o y ) |_| 1o ) )
34 33 a1i 
 |-  ( ( A e. _om /\ y e. _om ) -> ( ( A |_| y ) ~~ ( A +o y ) -> ( ( A |_| y ) |_| 1o ) ~~ ( ( A +o y ) |_| 1o ) ) )
35 nnacl 
 |-  ( ( A e. _om /\ y e. _om ) -> ( A +o y ) e. _om )
36 nnord 
 |-  ( ( A +o y ) e. _om -> Ord ( A +o y ) )
37 ordirr 
 |-  ( Ord ( A +o y ) -> -. ( A +o y ) e. ( A +o y ) )
38 35 36 37 3syl 
 |-  ( ( A e. _om /\ y e. _om ) -> -. ( A +o y ) e. ( A +o y ) )
39 dju1en 
 |-  ( ( ( A +o y ) e. _om /\ -. ( A +o y ) e. ( A +o y ) ) -> ( ( A +o y ) |_| 1o ) ~~ suc ( A +o y ) )
40 35 38 39 syl2anc 
 |-  ( ( A e. _om /\ y e. _om ) -> ( ( A +o y ) |_| 1o ) ~~ suc ( A +o y ) )
41 nnasuc 
 |-  ( ( A e. _om /\ y e. _om ) -> ( A +o suc y ) = suc ( A +o y ) )
42 40 41 breqtrrd 
 |-  ( ( A e. _om /\ y e. _om ) -> ( ( A +o y ) |_| 1o ) ~~ ( A +o suc y ) )
43 34 42 jctird 
 |-  ( ( A e. _om /\ y e. _om ) -> ( ( A |_| y ) ~~ ( A +o y ) -> ( ( ( A |_| y ) |_| 1o ) ~~ ( ( A +o y ) |_| 1o ) /\ ( ( A +o y ) |_| 1o ) ~~ ( A +o suc y ) ) ) )
44 entr 
 |-  ( ( ( ( A |_| y ) |_| 1o ) ~~ ( ( A +o y ) |_| 1o ) /\ ( ( A +o y ) |_| 1o ) ~~ ( A +o suc y ) ) -> ( ( A |_| y ) |_| 1o ) ~~ ( A +o suc y ) )
45 43 44 syl6 
 |-  ( ( A e. _om /\ y e. _om ) -> ( ( A |_| y ) ~~ ( A +o y ) -> ( ( A |_| y ) |_| 1o ) ~~ ( A +o suc y ) ) )
46 entr 
 |-  ( ( ( A |_| suc y ) ~~ ( ( A |_| y ) |_| 1o ) /\ ( ( A |_| y ) |_| 1o ) ~~ ( A +o suc y ) ) -> ( A |_| suc y ) ~~ ( A +o suc y ) )
47 30 45 46 syl6an 
 |-  ( ( A e. _om /\ y e. _om ) -> ( ( A |_| y ) ~~ ( A +o y ) -> ( A |_| suc y ) ~~ ( A +o suc y ) ) )
48 47 expcom 
 |-  ( y e. _om -> ( A e. _om -> ( ( A |_| y ) ~~ ( A +o y ) -> ( A |_| suc y ) ~~ ( A +o suc y ) ) ) )
49 7 10 13 16 48 finds2 
 |-  ( x e. _om -> ( A e. _om -> ( A |_| x ) ~~ ( A +o x ) ) )
50 4 49 vtoclga 
 |-  ( B e. _om -> ( A e. _om -> ( A |_| B ) ~~ ( A +o B ) ) )
51 50 impcom 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A |_| B ) ~~ ( A +o B ) )
52 carden2b 
 |-  ( ( A |_| B ) ~~ ( A +o B ) -> ( card ` ( A |_| B ) ) = ( card ` ( A +o B ) ) )
53 51 52 syl 
 |-  ( ( A e. _om /\ B e. _om ) -> ( card ` ( A |_| B ) ) = ( card ` ( A +o B ) ) )
54 nnacl 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A +o B ) e. _om )
55 cardnn 
 |-  ( ( A +o B ) e. _om -> ( card ` ( A +o B ) ) = ( A +o B ) )
56 54 55 syl 
 |-  ( ( A e. _om /\ B e. _om ) -> ( card ` ( A +o B ) ) = ( A +o B ) )
57 53 56 eqtrd 
 |-  ( ( A e. _om /\ B e. _om ) -> ( card ` ( A |_| B ) ) = ( A +o B ) )