oalimcl

Description: The ordinal sum with a limit ordinal is a limit ordinal. Proposition 8.11 of TakeutiZaring p. 60. Lemma 3.4 of Schloeder p. 7. (Contributed by NM, 8-Dec-2004)

		Ref	Expression
	Assertion	oalimcl	$⊢ (A \in On \land (B \in C \land Lim B)) \to Lim (A +_{𝑜} B)$

Proof

Step	Hyp	Ref	Expression
1		limelon	$⊢ (B \in C \land Lim B) \to B \in On$
2		oacl	$⊢ (A \in On \land B \in On) \to A +_{𝑜} B \in On$
3		eloni	$⊢ A +_{𝑜} B \in On \to Ord (A +_{𝑜} B)$
4	2 3	syl	$⊢ (A \in On \land B \in On) \to Ord (A +_{𝑜} B)$
5	1 4	sylan2	$⊢ (A \in On \land (B \in C \land Lim B)) \to Ord (A +_{𝑜} B)$
6		0ellim	$⊢ Lim B \to \emptyset \in B$
7		n0i	$⊢ \emptyset \in B \to \neg B = \emptyset$
8	6 7	syl	$⊢ Lim B \to \neg B = \emptyset$
9	8	ad2antll	$⊢ (A \in On \land (B \in C \land Lim B)) \to \neg B = \emptyset$
10		oa00	$⊢ (A \in On \land B \in On) \to (A +_{𝑜} B = \emptyset \leftrightarrow (A = \emptyset \land B = \emptyset))$
11		simpr	$⊢ (A = \emptyset \land B = \emptyset) \to B = \emptyset$
12	10 11	biimtrdi	$⊢ (A \in On \land B \in On) \to (A +_{𝑜} B = \emptyset \to B = \emptyset)$
13	12	con3d	$⊢ (A \in On \land B \in On) \to (\neg B = \emptyset \to \neg A +_{𝑜} B = \emptyset)$
14	1 13	sylan2	$⊢ (A \in On \land (B \in C \land Lim B)) \to (\neg B = \emptyset \to \neg A +_{𝑜} B = \emptyset)$
15	9 14	mpd	$⊢ (A \in On \land (B \in C \land Lim B)) \to \neg A +_{𝑜} B = \emptyset$
16		vex	$⊢ y \in V$
17	16	sucid	$⊢ y \in suc y$
18		oalim	$⊢ (A \in On \land (B \in C \land Lim B)) \to A +_{𝑜} B = ⋃_{x \in B} (A +_{𝑜} x)$
19		eqeq1	$⊢ A +_{𝑜} B = suc y \to (A +_{𝑜} B = ⋃_{x \in B} (A +_{𝑜} x) \leftrightarrow suc y = ⋃_{x \in B} (A +_{𝑜} x))$
20	18 19	imbitrid	$⊢ A +_{𝑜} B = suc y \to ((A \in On \land (B \in C \land Lim B)) \to suc y = ⋃_{x \in B} (A +_{𝑜} x))$
21	20	imp	$⊢ (A +_{𝑜} B = suc y \land (A \in On \land (B \in C \land Lim B))) \to suc y = ⋃_{x \in B} (A +_{𝑜} x)$
22	17 21	eleqtrid	$⊢ (A +_{𝑜} B = suc y \land (A \in On \land (B \in C \land Lim B))) \to y \in ⋃_{x \in B} (A +_{𝑜} x)$
23		eliun	$⊢ y \in ⋃_{x \in B} (A +_{𝑜} x) \leftrightarrow \exists x \in B y \in (A +_{𝑜} x)$
24	22 23	sylib	$⊢ (A +_{𝑜} B = suc y \land (A \in On \land (B \in C \land Lim B))) \to \exists x \in B y \in (A +_{𝑜} x)$
25		onelon	$⊢ (B \in On \land x \in B) \to x \in On$
26	1 25	sylan	$⊢ ((B \in C \land Lim B) \land x \in B) \to x \in On$
27		onnbtwn	$⊢ x \in On \to \neg (x \in B \land B \in suc x)$
28		imnan	$⊢ (x \in B \to \neg B \in suc x) \leftrightarrow \neg (x \in B \land B \in suc x)$
29	27 28	sylibr	$⊢ x \in On \to (x \in B \to \neg B \in suc x)$
30	29	com12	$⊢ x \in B \to (x \in On \to \neg B \in suc x)$
31	30	adantl	$⊢ ((B \in C \land Lim B) \land x \in B) \to (x \in On \to \neg B \in suc x)$
32	26 31	mpd	$⊢ ((B \in C \land Lim B) \land x \in B) \to \neg B \in suc x$
33	32	ad2antrl	$⊢ (A \in On \land (((B \in C \land Lim B) \land x \in B) \land y \in (A +_{𝑜} x))) \to \neg B \in suc x$
34		oacl	$⊢ (A \in On \land x \in On) \to A +_{𝑜} x \in On$
35		eloni	$⊢ A +_{𝑜} x \in On \to Ord (A +_{𝑜} x)$
36		ordsucelsuc	$⊢ Ord (A +_{𝑜} x) \to (y \in (A +_{𝑜} x) \leftrightarrow suc y \in suc (A +_{𝑜} x))$
37	34 35 36	3syl	$⊢ (A \in On \land x \in On) \to (y \in (A +_{𝑜} x) \leftrightarrow suc y \in suc (A +_{𝑜} x))$
38		oasuc	$⊢ (A \in On \land x \in On) \to A +_{𝑜} suc x = suc (A +_{𝑜} x)$
39	38	eleq2d	$⊢ (A \in On \land x \in On) \to (suc y \in (A +_{𝑜} suc x) \leftrightarrow suc y \in suc (A +_{𝑜} x))$
40	37 39	bitr4d	$⊢ (A \in On \land x \in On) \to (y \in (A +_{𝑜} x) \leftrightarrow suc y \in (A +_{𝑜} suc x))$
41	26 40	sylan2	$⊢ (A \in On \land ((B \in C \land Lim B) \land x \in B)) \to (y \in (A +_{𝑜} x) \leftrightarrow suc y \in (A +_{𝑜} suc x))$
42		eleq1	$⊢ A +_{𝑜} B = suc y \to (A +_{𝑜} B \in (A +_{𝑜} suc x) \leftrightarrow suc y \in (A +_{𝑜} suc x))$
43	42	bicomd	$⊢ A +_{𝑜} B = suc y \to (suc y \in (A +_{𝑜} suc x) \leftrightarrow A +_{𝑜} B \in (A +_{𝑜} suc x))$
44	41 43	sylan9bbr	$⊢ (A +_{𝑜} B = suc y \land (A \in On \land ((B \in C \land Lim B) \land x \in B))) \to (y \in (A +_{𝑜} x) \leftrightarrow A +_{𝑜} B \in (A +_{𝑜} suc x))$
45	1	adantr	$⊢ ((B \in C \land Lim B) \land x \in B) \to B \in On$
46		onsucb	$⊢ x \in On \leftrightarrow suc x \in On$
47	26 46	sylib	$⊢ ((B \in C \land Lim B) \land x \in B) \to suc x \in On$
48	45 47	jca	$⊢ ((B \in C \land Lim B) \land x \in B) \to (B \in On \land suc x \in On)$
49		oaord	$⊢ (B \in On \land suc x \in On \land A \in On) \to (B \in suc x \leftrightarrow A +_{𝑜} B \in (A +_{𝑜} suc x))$
50	49	3expa	$⊢ ((B \in On \land suc x \in On) \land A \in On) \to (B \in suc x \leftrightarrow A +_{𝑜} B \in (A +_{𝑜} suc x))$
51	48 50	sylan	$⊢ (((B \in C \land Lim B) \land x \in B) \land A \in On) \to (B \in suc x \leftrightarrow A +_{𝑜} B \in (A +_{𝑜} suc x))$
52	51	ancoms	$⊢ (A \in On \land ((B \in C \land Lim B) \land x \in B)) \to (B \in suc x \leftrightarrow A +_{𝑜} B \in (A +_{𝑜} suc x))$
53	52	adantl	$⊢ (A +_{𝑜} B = suc y \land (A \in On \land ((B \in C \land Lim B) \land x \in B))) \to (B \in suc x \leftrightarrow A +_{𝑜} B \in (A +_{𝑜} suc x))$
54	44 53	bitr4d	$⊢ (A +_{𝑜} B = suc y \land (A \in On \land ((B \in C \land Lim B) \land x \in B))) \to (y \in (A +_{𝑜} x) \leftrightarrow B \in suc x)$
55	54	biimpd	$⊢ (A +_{𝑜} B = suc y \land (A \in On \land ((B \in C \land Lim B) \land x \in B))) \to (y \in (A +_{𝑜} x) \to B \in suc x)$
56	55	exp32	$⊢ A +_{𝑜} B = suc y \to (A \in On \to (((B \in C \land Lim B) \land x \in B) \to (y \in (A +_{𝑜} x) \to B \in suc x)))$
57	56	com4l	$⊢ A \in On \to (((B \in C \land Lim B) \land x \in B) \to (y \in (A +_{𝑜} x) \to (A +_{𝑜} B = suc y \to B \in suc x)))$
58	57	imp32	$⊢ (A \in On \land (((B \in C \land Lim B) \land x \in B) \land y \in (A +_{𝑜} x))) \to (A +_{𝑜} B = suc y \to B \in suc x)$
59	33 58	mtod	$⊢ (A \in On \land (((B \in C \land Lim B) \land x \in B) \land y \in (A +_{𝑜} x))) \to \neg A +_{𝑜} B = suc y$
60	59	exp44	$⊢ A \in On \to ((B \in C \land Lim B) \to (x \in B \to (y \in (A +_{𝑜} x) \to \neg A +_{𝑜} B = suc y)))$
61	60	imp	$⊢ (A \in On \land (B \in C \land Lim B)) \to (x \in B \to (y \in (A +_{𝑜} x) \to \neg A +_{𝑜} B = suc y))$
62	61	rexlimdv	$⊢ (A \in On \land (B \in C \land Lim B)) \to (\exists x \in B y \in (A +_{𝑜} x) \to \neg A +_{𝑜} B = suc y)$
63	62	adantl	$⊢ (A +_{𝑜} B = suc y \land (A \in On \land (B \in C \land Lim B))) \to (\exists x \in B y \in (A +_{𝑜} x) \to \neg A +_{𝑜} B = suc y)$
64	24 63	mpd	$⊢ (A +_{𝑜} B = suc y \land (A \in On \land (B \in C \land Lim B))) \to \neg A +_{𝑜} B = suc y$
65	64	expcom	$⊢ (A \in On \land (B \in C \land Lim B)) \to (A +_{𝑜} B = suc y \to \neg A +_{𝑜} B = suc y)$
66	65	pm2.01d	$⊢ (A \in On \land (B \in C \land Lim B)) \to \neg A +_{𝑜} B = suc y$
67	66	adantr	$⊢ ((A \in On \land (B \in C \land Lim B)) \land y \in On) \to \neg A +_{𝑜} B = suc y$
68	67	nrexdv	$⊢ (A \in On \land (B \in C \land Lim B)) \to \neg \exists y \in On A +_{𝑜} B = suc y$
69		ioran	$⊢ \neg (A +_{𝑜} B = \emptyset \lor \exists y \in On A +_{𝑜} B = suc y) \leftrightarrow (\neg A +_{𝑜} B = \emptyset \land \neg \exists y \in On A +_{𝑜} B = suc y)$
70	15 68 69	sylanbrc	$⊢ (A \in On \land (B \in C \land Lim B)) \to \neg (A +_{𝑜} B = \emptyset \lor \exists y \in On A +_{𝑜} B = suc y)$
71		dflim3	$⊢ Lim (A +_{𝑜} B) \leftrightarrow (Ord (A +_{𝑜} B) \land \neg (A +_{𝑜} B = \emptyset \lor \exists y \in On A +_{𝑜} B = suc y))$
72	5 70 71	sylanbrc	$⊢ (A \in On \land (B \in C \land Lim B)) \to Lim (A +_{𝑜} B)$

Metamath Proof Explorer

Theorem oalimcl

Proof