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 ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( card ‘ ( 𝐴𝐵 ) ) = ( 𝐴 +o 𝐵 ) )

Proof

Step Hyp Ref Expression
1 djueq2 ( 𝑥 = 𝐵 → ( 𝐴𝑥 ) = ( 𝐴𝐵 ) )
2 oveq2 ( 𝑥 = 𝐵 → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o 𝐵 ) )
3 1 2 breq12d ( 𝑥 = 𝐵 → ( ( 𝐴𝑥 ) ≈ ( 𝐴 +o 𝑥 ) ↔ ( 𝐴𝐵 ) ≈ ( 𝐴 +o 𝐵 ) ) )
4 3 imbi2d ( 𝑥 = 𝐵 → ( ( 𝐴 ∈ ω → ( 𝐴𝑥 ) ≈ ( 𝐴 +o 𝑥 ) ) ↔ ( 𝐴 ∈ ω → ( 𝐴𝐵 ) ≈ ( 𝐴 +o 𝐵 ) ) ) )
5 djueq2 ( 𝑥 = ∅ → ( 𝐴𝑥 ) = ( 𝐴 ⊔ ∅ ) )
6 oveq2 ( 𝑥 = ∅ → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o ∅ ) )
7 5 6 breq12d ( 𝑥 = ∅ → ( ( 𝐴𝑥 ) ≈ ( 𝐴 +o 𝑥 ) ↔ ( 𝐴 ⊔ ∅ ) ≈ ( 𝐴 +o ∅ ) ) )
8 djueq2 ( 𝑥 = 𝑦 → ( 𝐴𝑥 ) = ( 𝐴𝑦 ) )
9 oveq2 ( 𝑥 = 𝑦 → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o 𝑦 ) )
10 8 9 breq12d ( 𝑥 = 𝑦 → ( ( 𝐴𝑥 ) ≈ ( 𝐴 +o 𝑥 ) ↔ ( 𝐴𝑦 ) ≈ ( 𝐴 +o 𝑦 ) ) )
11 djueq2 ( 𝑥 = suc 𝑦 → ( 𝐴𝑥 ) = ( 𝐴 ⊔ suc 𝑦 ) )
12 oveq2 ( 𝑥 = suc 𝑦 → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o suc 𝑦 ) )
13 11 12 breq12d ( 𝑥 = suc 𝑦 → ( ( 𝐴𝑥 ) ≈ ( 𝐴 +o 𝑥 ) ↔ ( 𝐴 ⊔ suc 𝑦 ) ≈ ( 𝐴 +o suc 𝑦 ) ) )
14 dju0en ( 𝐴 ∈ ω → ( 𝐴 ⊔ ∅ ) ≈ 𝐴 )
15 nna0 ( 𝐴 ∈ ω → ( 𝐴 +o ∅ ) = 𝐴 )
16 14 15 breqtrrd ( 𝐴 ∈ ω → ( 𝐴 ⊔ ∅ ) ≈ ( 𝐴 +o ∅ ) )
17 1oex 1o ∈ V
18 djuassen ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ∧ 1o ∈ V ) → ( ( 𝐴𝑦 ) ⊔ 1o ) ≈ ( 𝐴 ⊔ ( 𝑦 ⊔ 1o ) ) )
19 17 18 mp3an3 ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴𝑦 ) ⊔ 1o ) ≈ ( 𝐴 ⊔ ( 𝑦 ⊔ 1o ) ) )
20 enrefg ( 𝐴 ∈ ω → 𝐴𝐴 )
21 nnord ( 𝑦 ∈ ω → Ord 𝑦 )
22 ordirr ( Ord 𝑦 → ¬ 𝑦𝑦 )
23 21 22 syl ( 𝑦 ∈ ω → ¬ 𝑦𝑦 )
24 dju1en ( ( 𝑦 ∈ ω ∧ ¬ 𝑦𝑦 ) → ( 𝑦 ⊔ 1o ) ≈ suc 𝑦 )
25 23 24 mpdan ( 𝑦 ∈ ω → ( 𝑦 ⊔ 1o ) ≈ suc 𝑦 )
26 djuen ( ( 𝐴𝐴 ∧ ( 𝑦 ⊔ 1o ) ≈ suc 𝑦 ) → ( 𝐴 ⊔ ( 𝑦 ⊔ 1o ) ) ≈ ( 𝐴 ⊔ suc 𝑦 ) )
27 20 25 26 syl2an ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐴 ⊔ ( 𝑦 ⊔ 1o ) ) ≈ ( 𝐴 ⊔ suc 𝑦 ) )
28 entr ( ( ( ( 𝐴𝑦 ) ⊔ 1o ) ≈ ( 𝐴 ⊔ ( 𝑦 ⊔ 1o ) ) ∧ ( 𝐴 ⊔ ( 𝑦 ⊔ 1o ) ) ≈ ( 𝐴 ⊔ suc 𝑦 ) ) → ( ( 𝐴𝑦 ) ⊔ 1o ) ≈ ( 𝐴 ⊔ suc 𝑦 ) )
29 19 27 28 syl2anc ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴𝑦 ) ⊔ 1o ) ≈ ( 𝐴 ⊔ suc 𝑦 ) )
30 29 ensymd ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐴 ⊔ suc 𝑦 ) ≈ ( ( 𝐴𝑦 ) ⊔ 1o ) )
31 17 enref 1o ≈ 1o
32 djuen ( ( ( 𝐴𝑦 ) ≈ ( 𝐴 +o 𝑦 ) ∧ 1o ≈ 1o ) → ( ( 𝐴𝑦 ) ⊔ 1o ) ≈ ( ( 𝐴 +o 𝑦 ) ⊔ 1o ) )
33 31 32 mpan2 ( ( 𝐴𝑦 ) ≈ ( 𝐴 +o 𝑦 ) → ( ( 𝐴𝑦 ) ⊔ 1o ) ≈ ( ( 𝐴 +o 𝑦 ) ⊔ 1o ) )
34 33 a1i ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴𝑦 ) ≈ ( 𝐴 +o 𝑦 ) → ( ( 𝐴𝑦 ) ⊔ 1o ) ≈ ( ( 𝐴 +o 𝑦 ) ⊔ 1o ) ) )
35 nnacl ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐴 +o 𝑦 ) ∈ ω )
36 nnord ( ( 𝐴 +o 𝑦 ) ∈ ω → Ord ( 𝐴 +o 𝑦 ) )
37 ordirr ( Ord ( 𝐴 +o 𝑦 ) → ¬ ( 𝐴 +o 𝑦 ) ∈ ( 𝐴 +o 𝑦 ) )
38 35 36 37 3syl ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ¬ ( 𝐴 +o 𝑦 ) ∈ ( 𝐴 +o 𝑦 ) )
39 dju1en ( ( ( 𝐴 +o 𝑦 ) ∈ ω ∧ ¬ ( 𝐴 +o 𝑦 ) ∈ ( 𝐴 +o 𝑦 ) ) → ( ( 𝐴 +o 𝑦 ) ⊔ 1o ) ≈ suc ( 𝐴 +o 𝑦 ) )
40 35 38 39 syl2anc ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 +o 𝑦 ) ⊔ 1o ) ≈ suc ( 𝐴 +o 𝑦 ) )
41 nnasuc ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐴 +o suc 𝑦 ) = suc ( 𝐴 +o 𝑦 ) )
42 40 41 breqtrrd ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 +o 𝑦 ) ⊔ 1o ) ≈ ( 𝐴 +o suc 𝑦 ) )
43 34 42 jctird ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴𝑦 ) ≈ ( 𝐴 +o 𝑦 ) → ( ( ( 𝐴𝑦 ) ⊔ 1o ) ≈ ( ( 𝐴 +o 𝑦 ) ⊔ 1o ) ∧ ( ( 𝐴 +o 𝑦 ) ⊔ 1o ) ≈ ( 𝐴 +o suc 𝑦 ) ) ) )
44 entr ( ( ( ( 𝐴𝑦 ) ⊔ 1o ) ≈ ( ( 𝐴 +o 𝑦 ) ⊔ 1o ) ∧ ( ( 𝐴 +o 𝑦 ) ⊔ 1o ) ≈ ( 𝐴 +o suc 𝑦 ) ) → ( ( 𝐴𝑦 ) ⊔ 1o ) ≈ ( 𝐴 +o suc 𝑦 ) )
45 43 44 syl6 ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴𝑦 ) ≈ ( 𝐴 +o 𝑦 ) → ( ( 𝐴𝑦 ) ⊔ 1o ) ≈ ( 𝐴 +o suc 𝑦 ) ) )
46 entr ( ( ( 𝐴 ⊔ suc 𝑦 ) ≈ ( ( 𝐴𝑦 ) ⊔ 1o ) ∧ ( ( 𝐴𝑦 ) ⊔ 1o ) ≈ ( 𝐴 +o suc 𝑦 ) ) → ( 𝐴 ⊔ suc 𝑦 ) ≈ ( 𝐴 +o suc 𝑦 ) )
47 30 45 46 syl6an ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴𝑦 ) ≈ ( 𝐴 +o 𝑦 ) → ( 𝐴 ⊔ suc 𝑦 ) ≈ ( 𝐴 +o suc 𝑦 ) ) )
48 47 expcom ( 𝑦 ∈ ω → ( 𝐴 ∈ ω → ( ( 𝐴𝑦 ) ≈ ( 𝐴 +o 𝑦 ) → ( 𝐴 ⊔ suc 𝑦 ) ≈ ( 𝐴 +o suc 𝑦 ) ) ) )
49 7 10 13 16 48 finds2 ( 𝑥 ∈ ω → ( 𝐴 ∈ ω → ( 𝐴𝑥 ) ≈ ( 𝐴 +o 𝑥 ) ) )
50 4 49 vtoclga ( 𝐵 ∈ ω → ( 𝐴 ∈ ω → ( 𝐴𝐵 ) ≈ ( 𝐴 +o 𝐵 ) ) )
51 50 impcom ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴𝐵 ) ≈ ( 𝐴 +o 𝐵 ) )
52 carden2b ( ( 𝐴𝐵 ) ≈ ( 𝐴 +o 𝐵 ) → ( card ‘ ( 𝐴𝐵 ) ) = ( card ‘ ( 𝐴 +o 𝐵 ) ) )
53 51 52 syl ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( card ‘ ( 𝐴𝐵 ) ) = ( card ‘ ( 𝐴 +o 𝐵 ) ) )
54 nnacl ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 +o 𝐵 ) ∈ ω )
55 cardnn ( ( 𝐴 +o 𝐵 ) ∈ ω → ( card ‘ ( 𝐴 +o 𝐵 ) ) = ( 𝐴 +o 𝐵 ) )
56 54 55 syl ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( card ‘ ( 𝐴 +o 𝐵 ) ) = ( 𝐴 +o 𝐵 ) )
57 53 56 eqtrd ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( card ‘ ( 𝐴𝐵 ) ) = ( 𝐴 +o 𝐵 ) )