This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐵 ) )