omlimcl

Description: The product of any nonzero ordinal with a limit ordinal is a limit ordinal. Proposition 8.24 of TakeutiZaring p. 64. (Contributed by NM, 25-Dec-2004)

		Ref	Expression
	Assertion	omlimcl	$⊢ ((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \to Lim (A \cdot_{𝑜} B)$

Proof

Step	Hyp	Ref	Expression
1		limelon	$⊢ (B \in C \land Lim B) \to B \in On$
2		omcl	$⊢ (A \in On \land B \in On) \to A \cdot_{𝑜} B \in On$
3		eloni	$⊢ A \cdot_{𝑜} B \in On \to Ord (A \cdot_{𝑜} B)$
4	2 3	syl	$⊢ (A \in On \land B \in On) \to Ord (A \cdot_{𝑜} B)$
5	1 4	sylan2	$⊢ (A \in On \land (B \in C \land Lim B)) \to Ord (A \cdot_{𝑜} B)$
6	5	adantr	$⊢ ((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \to Ord (A \cdot_{𝑜} B)$
7		0ellim	$⊢ Lim B \to \emptyset \in B$
8		n0i	$⊢ \emptyset \in B \to \neg B = \emptyset$
9	7 8	syl	$⊢ Lim B \to \neg B = \emptyset$
10		n0i	$⊢ \emptyset \in A \to \neg A = \emptyset$
11	9 10	anim12ci	$⊢ (Lim B \land \emptyset \in A) \to (\neg A = \emptyset \land \neg B = \emptyset)$
12	11	adantll	$⊢ ((B \in C \land Lim B) \land \emptyset \in A) \to (\neg A = \emptyset \land \neg B = \emptyset)$
13	12	adantll	$⊢ ((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \to (\neg A = \emptyset \land \neg B = \emptyset)$
14		om00	$⊢ (A \in On \land B \in On) \to (A \cdot_{𝑜} B = \emptyset \leftrightarrow (A = \emptyset \lor B = \emptyset))$
15	14	notbid	$⊢ (A \in On \land B \in On) \to (\neg A \cdot_{𝑜} B = \emptyset \leftrightarrow \neg (A = \emptyset \lor B = \emptyset))$
16		ioran	$⊢ \neg (A = \emptyset \lor B = \emptyset) \leftrightarrow (\neg A = \emptyset \land \neg B = \emptyset)$
17	15 16	bitrdi	$⊢ (A \in On \land B \in On) \to (\neg A \cdot_{𝑜} B = \emptyset \leftrightarrow (\neg A = \emptyset \land \neg B = \emptyset))$
18	1 17	sylan2	$⊢ (A \in On \land (B \in C \land Lim B)) \to (\neg A \cdot_{𝑜} B = \emptyset \leftrightarrow (\neg A = \emptyset \land \neg B = \emptyset))$
19	18	adantr	$⊢ ((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \to (\neg A \cdot_{𝑜} B = \emptyset \leftrightarrow (\neg A = \emptyset \land \neg B = \emptyset))$
20	13 19	mpbird	$⊢ ((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \to \neg A \cdot_{𝑜} B = \emptyset$
21		vex	$⊢ y \in V$
22	21	sucid	$⊢ y \in suc y$
23		omlim	$⊢ (A \in On \land (B \in C \land Lim B)) \to A \cdot_{𝑜} B = ⋃_{x \in B} (A \cdot_{𝑜} x)$
24		eqeq1	$⊢ A \cdot_{𝑜} B = suc y \to (A \cdot_{𝑜} B = ⋃_{x \in B} (A \cdot_{𝑜} x) \leftrightarrow suc y = ⋃_{x \in B} (A \cdot_{𝑜} x))$
25	24	biimpac	$⊢ (A \cdot_{𝑜} B = ⋃_{x \in B} (A \cdot_{𝑜} x) \land A \cdot_{𝑜} B = suc y) \to suc y = ⋃_{x \in B} (A \cdot_{𝑜} x)$
26	23 25	sylan	$⊢ ((A \in On \land (B \in C \land Lim B)) \land A \cdot_{𝑜} B = suc y) \to suc y = ⋃_{x \in B} (A \cdot_{𝑜} x)$
27	22 26	eleqtrid	$⊢ ((A \in On \land (B \in C \land Lim B)) \land A \cdot_{𝑜} B = suc y) \to y \in ⋃_{x \in B} (A \cdot_{𝑜} x)$
28		eliun	$⊢ y \in ⋃_{x \in B} (A \cdot_{𝑜} x) \leftrightarrow \exists x \in B y \in (A \cdot_{𝑜} x)$
29	27 28	sylib	$⊢ ((A \in On \land (B \in C \land Lim B)) \land A \cdot_{𝑜} B = suc y) \to \exists x \in B y \in (A \cdot_{𝑜} x)$
30	29	adantlr	$⊢ (((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \land A \cdot_{𝑜} B = suc y) \to \exists x \in B y \in (A \cdot_{𝑜} x)$
31		onelon	$⊢ (B \in On \land x \in B) \to x \in On$
32	1 31	sylan	$⊢ ((B \in C \land Lim B) \land x \in B) \to x \in On$
33		onnbtwn	$⊢ x \in On \to \neg (x \in B \land B \in suc x)$
34		imnan	$⊢ (x \in B \to \neg B \in suc x) \leftrightarrow \neg (x \in B \land B \in suc x)$
35	33 34	sylibr	$⊢ x \in On \to (x \in B \to \neg B \in suc x)$
36	35	com12	$⊢ x \in B \to (x \in On \to \neg B \in suc x)$
37	36	adantl	$⊢ ((B \in C \land Lim B) \land x \in B) \to (x \in On \to \neg B \in suc x)$
38	32 37	mpd	$⊢ ((B \in C \land Lim B) \land x \in B) \to \neg B \in suc x$
39	38	ad5ant24	$⊢ ((((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \land x \in B) \land y \in (A \cdot_{𝑜} x)) \to \neg B \in suc x$
40		simpl	$⊢ (B \in On \land x \in B) \to B \in On$
41	40 31	jca	$⊢ (B \in On \land x \in B) \to (B \in On \land x \in On)$
42	1 41	sylan	$⊢ ((B \in C \land Lim B) \land x \in B) \to (B \in On \land x \in On)$
43	42	anim2i	$⊢ (A \in On \land ((B \in C \land Lim B) \land x \in B)) \to (A \in On \land (B \in On \land x \in On))$
44	43	anassrs	$⊢ ((A \in On \land (B \in C \land Lim B)) \land x \in B) \to (A \in On \land (B \in On \land x \in On))$
45		omcl	$⊢ (A \in On \land x \in On) \to A \cdot_{𝑜} x \in On$
46		eloni	$⊢ A \cdot_{𝑜} x \in On \to Ord (A \cdot_{𝑜} x)$
47		ordsucelsuc	$⊢ Ord (A \cdot_{𝑜} x) \to (y \in (A \cdot_{𝑜} x) \leftrightarrow suc y \in suc (A \cdot_{𝑜} x))$
48	46 47	syl	$⊢ A \cdot_{𝑜} x \in On \to (y \in (A \cdot_{𝑜} x) \leftrightarrow suc y \in suc (A \cdot_{𝑜} x))$
49		oa1suc	$⊢ A \cdot_{𝑜} x \in On \to (A \cdot_{𝑜} x) +_{𝑜} 1_{𝑜} = suc (A \cdot_{𝑜} x)$
50	49	eleq2d	$⊢ A \cdot_{𝑜} x \in On \to (suc y \in ((A \cdot_{𝑜} x) +_{𝑜} 1_{𝑜}) \leftrightarrow suc y \in suc (A \cdot_{𝑜} x))$
51	48 50	bitr4d	$⊢ A \cdot_{𝑜} x \in On \to (y \in (A \cdot_{𝑜} x) \leftrightarrow suc y \in ((A \cdot_{𝑜} x) +_{𝑜} 1_{𝑜}))$
52	45 51	syl	$⊢ (A \in On \land x \in On) \to (y \in (A \cdot_{𝑜} x) \leftrightarrow suc y \in ((A \cdot_{𝑜} x) +_{𝑜} 1_{𝑜}))$
53	52	adantr	$⊢ ((A \in On \land x \in On) \land \emptyset \in A) \to (y \in (A \cdot_{𝑜} x) \leftrightarrow suc y \in ((A \cdot_{𝑜} x) +_{𝑜} 1_{𝑜}))$
54		eloni	$⊢ A \in On \to Ord A$
55		ordgt0ge1	$⊢ Ord A \to (\emptyset \in A \leftrightarrow 1_{𝑜} \subseteq A)$
56	54 55	syl	$⊢ A \in On \to (\emptyset \in A \leftrightarrow 1_{𝑜} \subseteq A)$
57	56	adantr	$⊢ (A \in On \land x \in On) \to (\emptyset \in A \leftrightarrow 1_{𝑜} \subseteq A)$
58		1on	$⊢ 1_{𝑜} \in On$
59		oaword	$⊢ (1_{𝑜} \in On \land A \in On \land A \cdot_{𝑜} x \in On) \to (1_{𝑜} \subseteq A \leftrightarrow (A \cdot_{𝑜} x) +_{𝑜} 1_{𝑜} \subseteq (A \cdot_{𝑜} x) +_{𝑜} A)$
60	58 59	mp3an1	$⊢ (A \in On \land A \cdot_{𝑜} x \in On) \to (1_{𝑜} \subseteq A \leftrightarrow (A \cdot_{𝑜} x) +_{𝑜} 1_{𝑜} \subseteq (A \cdot_{𝑜} x) +_{𝑜} A)$
61	45 60	syldan	$⊢ (A \in On \land x \in On) \to (1_{𝑜} \subseteq A \leftrightarrow (A \cdot_{𝑜} x) +_{𝑜} 1_{𝑜} \subseteq (A \cdot_{𝑜} x) +_{𝑜} A)$
62	57 61	bitrd	$⊢ (A \in On \land x \in On) \to (\emptyset \in A \leftrightarrow (A \cdot_{𝑜} x) +_{𝑜} 1_{𝑜} \subseteq (A \cdot_{𝑜} x) +_{𝑜} A)$
63	62	biimpa	$⊢ ((A \in On \land x \in On) \land \emptyset \in A) \to (A \cdot_{𝑜} x) +_{𝑜} 1_{𝑜} \subseteq (A \cdot_{𝑜} x) +_{𝑜} A$
64		omsuc	$⊢ (A \in On \land x \in On) \to A \cdot_{𝑜} suc x = (A \cdot_{𝑜} x) +_{𝑜} A$
65	64	adantr	$⊢ ((A \in On \land x \in On) \land \emptyset \in A) \to A \cdot_{𝑜} suc x = (A \cdot_{𝑜} x) +_{𝑜} A$
66	63 65	sseqtrrd	$⊢ ((A \in On \land x \in On) \land \emptyset \in A) \to (A \cdot_{𝑜} x) +_{𝑜} 1_{𝑜} \subseteq A \cdot_{𝑜} suc x$
67	66	sseld	$⊢ ((A \in On \land x \in On) \land \emptyset \in A) \to (suc y \in ((A \cdot_{𝑜} x) +_{𝑜} 1_{𝑜}) \to suc y \in (A \cdot_{𝑜} suc x))$
68	53 67	sylbid	$⊢ ((A \in On \land x \in On) \land \emptyset \in A) \to (y \in (A \cdot_{𝑜} x) \to suc y \in (A \cdot_{𝑜} suc x))$
69		eleq1	$⊢ A \cdot_{𝑜} B = suc y \to (A \cdot_{𝑜} B \in (A \cdot_{𝑜} suc x) \leftrightarrow suc y \in (A \cdot_{𝑜} suc x))$
70	69	biimprd	$⊢ A \cdot_{𝑜} B = suc y \to (suc y \in (A \cdot_{𝑜} suc x) \to A \cdot_{𝑜} B \in (A \cdot_{𝑜} suc x))$
71	68 70	syl9	$⊢ ((A \in On \land x \in On) \land \emptyset \in A) \to (A \cdot_{𝑜} B = suc y \to (y \in (A \cdot_{𝑜} x) \to A \cdot_{𝑜} B \in (A \cdot_{𝑜} suc x)))$
72	71	com23	$⊢ ((A \in On \land x \in On) \land \emptyset \in A) \to (y \in (A \cdot_{𝑜} x) \to (A \cdot_{𝑜} B = suc y \to A \cdot_{𝑜} B \in (A \cdot_{𝑜} suc x)))$
73	72	adantlrl	$⊢ ((A \in On \land (B \in On \land x \in On)) \land \emptyset \in A) \to (y \in (A \cdot_{𝑜} x) \to (A \cdot_{𝑜} B = suc y \to A \cdot_{𝑜} B \in (A \cdot_{𝑜} suc x)))$
74		onsucb	$⊢ x \in On \leftrightarrow suc x \in On$
75		omord	$⊢ (B \in On \land suc x \in On \land A \in On) \to ((B \in suc x \land \emptyset \in A) \leftrightarrow A \cdot_{𝑜} B \in (A \cdot_{𝑜} suc x))$
76		simpl	$⊢ (B \in suc x \land \emptyset \in A) \to B \in suc x$
77	75 76	syl6bir	$⊢ (B \in On \land suc x \in On \land A \in On) \to (A \cdot_{𝑜} B \in (A \cdot_{𝑜} suc x) \to B \in suc x)$
78	74 77	syl3an2b	$⊢ (B \in On \land x \in On \land A \in On) \to (A \cdot_{𝑜} B \in (A \cdot_{𝑜} suc x) \to B \in suc x)$
79	78	3comr	$⊢ (A \in On \land B \in On \land x \in On) \to (A \cdot_{𝑜} B \in (A \cdot_{𝑜} suc x) \to B \in suc x)$
80	79	3expb	$⊢ (A \in On \land (B \in On \land x \in On)) \to (A \cdot_{𝑜} B \in (A \cdot_{𝑜} suc x) \to B \in suc x)$
81	80	adantr	$⊢ ((A \in On \land (B \in On \land x \in On)) \land \emptyset \in A) \to (A \cdot_{𝑜} B \in (A \cdot_{𝑜} suc x) \to B \in suc x)$
82	73 81	syl6d	$⊢ ((A \in On \land (B \in On \land x \in On)) \land \emptyset \in A) \to (y \in (A \cdot_{𝑜} x) \to (A \cdot_{𝑜} B = suc y \to B \in suc x))$
83	44 82	sylan	$⊢ (((A \in On \land (B \in C \land Lim B)) \land x \in B) \land \emptyset \in A) \to (y \in (A \cdot_{𝑜} x) \to (A \cdot_{𝑜} B = suc y \to B \in suc x))$
84	83	an32s	$⊢ (((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \land x \in B) \to (y \in (A \cdot_{𝑜} x) \to (A \cdot_{𝑜} B = suc y \to B \in suc x))$
85	84	imp	$⊢ ((((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \land x \in B) \land y \in (A \cdot_{𝑜} x)) \to (A \cdot_{𝑜} B = suc y \to B \in suc x)$
86	39 85	mtod	$⊢ ((((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \land x \in B) \land y \in (A \cdot_{𝑜} x)) \to \neg A \cdot_{𝑜} B = suc y$
87	86	rexlimdva2	$⊢ ((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \to (\exists x \in B y \in (A \cdot_{𝑜} x) \to \neg A \cdot_{𝑜} B = suc y)$
88	87	adantr	$⊢ (((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \land A \cdot_{𝑜} B = suc y) \to (\exists x \in B y \in (A \cdot_{𝑜} x) \to \neg A \cdot_{𝑜} B = suc y)$
89	30 88	mpd	$⊢ (((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \land A \cdot_{𝑜} B = suc y) \to \neg A \cdot_{𝑜} B = suc y$
90	89	pm2.01da	$⊢ ((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \to \neg A \cdot_{𝑜} B = suc y$
91	90	adantr	$⊢ (((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \land y \in On) \to \neg A \cdot_{𝑜} B = suc y$
92	91	nrexdv	$⊢ ((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \to \neg \exists y \in On A \cdot_{𝑜} B = suc y$
93		ioran	$⊢ \neg (A \cdot_{𝑜} B = \emptyset \lor \exists y \in On A \cdot_{𝑜} B = suc y) \leftrightarrow (\neg A \cdot_{𝑜} B = \emptyset \land \neg \exists y \in On A \cdot_{𝑜} B = suc y)$
94	20 92 93	sylanbrc	$⊢ ((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \to \neg (A \cdot_{𝑜} B = \emptyset \lor \exists y \in On A \cdot_{𝑜} B = suc y)$
95		dflim3	$⊢ Lim (A \cdot_{𝑜} B) \leftrightarrow (Ord (A \cdot_{𝑜} B) \land \neg (A \cdot_{𝑜} B = \emptyset \lor \exists y \in On A \cdot_{𝑜} B = suc y))$
96	6 94 95	sylanbrc	$⊢ ((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \to Lim (A \cdot_{𝑜} B)$

Metamath Proof Explorer

Theorem omlimcl

Proof