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 \in ω \land B \in ω) \to card ((A ⊔︀ B)) = A +_{𝑜} B$

Proof

Step	Hyp	Ref	Expression
1		djueq2	$⊢ x = B \to (A ⊔︀ x) = (A ⊔︀ B)$
2		oveq2	$⊢ x = B \to A +_{𝑜} x = A +_{𝑜} B$
3	1 2	breq12d	$⊢ x = B \to ((A ⊔︀ x) \approx (A +_{𝑜} x) \leftrightarrow (A ⊔︀ B) \approx (A +_{𝑜} B))$
4	3	imbi2d	$⊢ x = B \to ((A \in ω \to (A ⊔︀ x) \approx (A +_{𝑜} x)) \leftrightarrow (A \in ω \to (A ⊔︀ B) \approx (A +_{𝑜} B)))$
5		djueq2	$⊢ x = \emptyset \to (A ⊔︀ x) = (A ⊔︀ \emptyset)$
6		oveq2	$⊢ x = \emptyset \to A +_{𝑜} x = A +_{𝑜} \emptyset$
7	5 6	breq12d	$⊢ x = \emptyset \to ((A ⊔︀ x) \approx (A +_{𝑜} x) \leftrightarrow (A ⊔︀ \emptyset) \approx (A +_{𝑜} \emptyset))$
8		djueq2	$⊢ x = y \to (A ⊔︀ x) = (A ⊔︀ y)$
9		oveq2	$⊢ x = y \to A +_{𝑜} x = A +_{𝑜} y$
10	8 9	breq12d	$⊢ x = y \to ((A ⊔︀ x) \approx (A +_{𝑜} x) \leftrightarrow (A ⊔︀ y) \approx (A +_{𝑜} y))$
11		djueq2	$⊢ x = suc y \to (A ⊔︀ x) = (A ⊔︀ suc y)$
12		oveq2	$⊢ x = suc y \to A +_{𝑜} x = A +_{𝑜} suc y$
13	11 12	breq12d	$⊢ x = suc y \to ((A ⊔︀ x) \approx (A +_{𝑜} x) \leftrightarrow (A ⊔︀ suc y) \approx (A +_{𝑜} suc y))$
14		dju0en	$⊢ A \in ω \to (A ⊔︀ \emptyset) \approx A$
15		nna0	$⊢ A \in ω \to A +_{𝑜} \emptyset = A$
16	14 15	breqtrrd	$⊢ A \in ω \to (A ⊔︀ \emptyset) \approx (A +_{𝑜} \emptyset)$
17		1oex	$⊢ 1_{𝑜} \in V$
18		djuassen	$⊢ (A \in ω \land y \in ω \land 1_{𝑜} \in V) \to ((A ⊔︀ y) ⊔︀ 1_{𝑜}) \approx (A ⊔︀ (y ⊔︀ 1_{𝑜}))$
19	17 18	mp3an3	$⊢ (A \in ω \land y \in ω) \to ((A ⊔︀ y) ⊔︀ 1_{𝑜}) \approx (A ⊔︀ (y ⊔︀ 1_{𝑜}))$
20		enrefg	$⊢ A \in ω \to A \approx A$
21		nnord	$⊢ y \in ω \to Ord y$
22		ordirr	$⊢ Ord y \to \neg y \in y$
23	21 22	syl	$⊢ y \in ω \to \neg y \in y$
24		dju1en	$⊢ (y \in ω \land \neg y \in y) \to (y ⊔︀ 1_{𝑜}) \approx suc y$
25	23 24	mpdan	$⊢ y \in ω \to (y ⊔︀ 1_{𝑜}) \approx suc y$
26		djuen	$⊢ (A \approx A \land (y ⊔︀ 1_{𝑜}) \approx suc y) \to (A ⊔︀ (y ⊔︀ 1_{𝑜})) \approx (A ⊔︀ suc y)$
27	20 25 26	syl2an	$⊢ (A \in ω \land y \in ω) \to (A ⊔︀ (y ⊔︀ 1_{𝑜})) \approx (A ⊔︀ suc y)$
28		entr	$⊢ (((A ⊔︀ y) ⊔︀ 1_{𝑜}) \approx (A ⊔︀ (y ⊔︀ 1_{𝑜})) \land (A ⊔︀ (y ⊔︀ 1_{𝑜})) \approx (A ⊔︀ suc y)) \to ((A ⊔︀ y) ⊔︀ 1_{𝑜}) \approx (A ⊔︀ suc y)$
29	19 27 28	syl2anc	$⊢ (A \in ω \land y \in ω) \to ((A ⊔︀ y) ⊔︀ 1_{𝑜}) \approx (A ⊔︀ suc y)$
30	29	ensymd	$⊢ (A \in ω \land y \in ω) \to (A ⊔︀ suc y) \approx ((A ⊔︀ y) ⊔︀ 1_{𝑜})$
31	17	enref	$⊢ 1_{𝑜} \approx 1_{𝑜}$
32		djuen	$⊢ ((A ⊔︀ y) \approx (A +_{𝑜} y) \land 1_{𝑜} \approx 1_{𝑜}) \to ((A ⊔︀ y) ⊔︀ 1_{𝑜}) \approx ((A +_{𝑜} y) ⊔︀ 1_{𝑜})$
33	31 32	mpan2	$⊢ (A ⊔︀ y) \approx (A +_{𝑜} y) \to ((A ⊔︀ y) ⊔︀ 1_{𝑜}) \approx ((A +_{𝑜} y) ⊔︀ 1_{𝑜})$
34	33	a1i	$⊢ (A \in ω \land y \in ω) \to ((A ⊔︀ y) \approx (A +_{𝑜} y) \to ((A ⊔︀ y) ⊔︀ 1_{𝑜}) \approx ((A +_{𝑜} y) ⊔︀ 1_{𝑜}))$
35		nnacl	$⊢ (A \in ω \land y \in ω) \to A +_{𝑜} y \in ω$
36		nnord	$⊢ A +_{𝑜} y \in ω \to Ord (A +_{𝑜} y)$
37		ordirr	$⊢ Ord (A +_{𝑜} y) \to \neg A +_{𝑜} y \in (A +_{𝑜} y)$
38	35 36 37	3syl	$⊢ (A \in ω \land y \in ω) \to \neg A +_{𝑜} y \in (A +_{𝑜} y)$
39		dju1en	$⊢ (A +_{𝑜} y \in ω \land \neg A +_{𝑜} y \in (A +_{𝑜} y)) \to ((A +_{𝑜} y) ⊔︀ 1_{𝑜}) \approx suc (A +_{𝑜} y)$
40	35 38 39	syl2anc	$⊢ (A \in ω \land y \in ω) \to ((A +_{𝑜} y) ⊔︀ 1_{𝑜}) \approx suc (A +_{𝑜} y)$
41		nnasuc	$⊢ (A \in ω \land y \in ω) \to A +_{𝑜} suc y = suc (A +_{𝑜} y)$
42	40 41	breqtrrd	$⊢ (A \in ω \land y \in ω) \to ((A +_{𝑜} y) ⊔︀ 1_{𝑜}) \approx (A +_{𝑜} suc y)$
43	34 42	jctird	$⊢ (A \in ω \land y \in ω) \to ((A ⊔︀ y) \approx (A +_{𝑜} y) \to (((A ⊔︀ y) ⊔︀ 1_{𝑜}) \approx ((A +_{𝑜} y) ⊔︀ 1_{𝑜}) \land ((A +_{𝑜} y) ⊔︀ 1_{𝑜}) \approx (A +_{𝑜} suc y)))$
44		entr	$⊢ (((A ⊔︀ y) ⊔︀ 1_{𝑜}) \approx ((A +_{𝑜} y) ⊔︀ 1_{𝑜}) \land ((A +_{𝑜} y) ⊔︀ 1_{𝑜}) \approx (A +_{𝑜} suc y)) \to ((A ⊔︀ y) ⊔︀ 1_{𝑜}) \approx (A +_{𝑜} suc y)$
45	43 44	syl6	$⊢ (A \in ω \land y \in ω) \to ((A ⊔︀ y) \approx (A +_{𝑜} y) \to ((A ⊔︀ y) ⊔︀ 1_{𝑜}) \approx (A +_{𝑜} suc y))$
46		entr	$⊢ ((A ⊔︀ suc y) \approx ((A ⊔︀ y) ⊔︀ 1_{𝑜}) \land ((A ⊔︀ y) ⊔︀ 1_{𝑜}) \approx (A +_{𝑜} suc y)) \to (A ⊔︀ suc y) \approx (A +_{𝑜} suc y)$
47	30 45 46	syl6an	$⊢ (A \in ω \land y \in ω) \to ((A ⊔︀ y) \approx (A +_{𝑜} y) \to (A ⊔︀ suc y) \approx (A +_{𝑜} suc y))$
48	47	expcom	$⊢ y \in ω \to (A \in ω \to ((A ⊔︀ y) \approx (A +_{𝑜} y) \to (A ⊔︀ suc y) \approx (A +_{𝑜} suc y)))$
49	7 10 13 16 48	finds2	$⊢ x \in ω \to (A \in ω \to (A ⊔︀ x) \approx (A +_{𝑜} x))$
50	4 49	vtoclga	$⊢ B \in ω \to (A \in ω \to (A ⊔︀ B) \approx (A +_{𝑜} B))$
51	50	impcom	$⊢ (A \in ω \land B \in ω) \to (A ⊔︀ B) \approx (A +_{𝑜} B)$
52		carden2b	$⊢ (A ⊔︀ B) \approx (A +_{𝑜} B) \to card ((A ⊔︀ B)) = card (A +_{𝑜} B)$
53	51 52	syl	$⊢ (A \in ω \land B \in ω) \to card ((A ⊔︀ B)) = card (A +_{𝑜} B)$
54		nnacl	$⊢ (A \in ω \land B \in ω) \to A +_{𝑜} B \in ω$
55		cardnn	$⊢ A +_{𝑜} B \in ω \to card (A +_{𝑜} B) = A +_{𝑜} B$
56	54 55	syl	$⊢ (A \in ω \land B \in ω) \to card (A +_{𝑜} B) = A +_{𝑜} B$
57	53 56	eqtrd	$⊢ (A \in ω \land B \in ω) \to card ((A ⊔︀ B)) = A +_{𝑜} B$

Metamath Proof Explorer

Theorem nnadju

Proof