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