dflim5

Description: A limit ordinal is either the proper class of ordinals or some nonzero product with omega. (Contributed by RP, 8-Jan-2025)

		Ref	Expression
	Assertion	dflim5	$⊢ Lim A \leftrightarrow (A = On \lor \exists x \in (On ∖ 1_{𝑜}) A = ω \cdot_{𝑜} x)$

Proof

Step	Hyp	Ref	Expression
1		limord	$⊢ Lim A \to Ord A$
2		ordeleqon	$⊢ Ord A \leftrightarrow (A \in On \lor A = On)$
3	2	biimpi	$⊢ Ord A \to (A \in On \lor A = On)$
4	3	orcomd	$⊢ Ord A \to (A = On \lor A \in On)$
5	1 4	syl	$⊢ Lim A \to (A = On \lor A \in On)$
6	5	pm4.71ri	$⊢ Lim A \leftrightarrow ((A = On \lor A \in On) \land Lim A)$
7		andir	$⊢ ((A = On \lor A \in On) \land Lim A) \leftrightarrow ((A = On \land Lim A) \lor (A \in On \land Lim A))$
8	6 7	bitri	$⊢ Lim A \leftrightarrow ((A = On \land Lim A) \lor (A \in On \land Lim A))$
9		limon	$⊢ Lim On$
10		limeq	$⊢ A = On \to (Lim A \leftrightarrow Lim On)$
11	9 10	mpbiri	$⊢ A = On \to Lim A$
12	11	pm4.71i	$⊢ A = On \leftrightarrow (A = On \land Lim A)$
13	12	orbi1i	$⊢ (A = On \lor (A \in On \land Lim A)) \leftrightarrow ((A = On \land Lim A) \lor (A \in On \land Lim A))$
14		simpl	$⊢ (A \in On \land Lim A) \to A \in On$
15		omelon	$⊢ ω \in On$
16	15	a1i	$⊢ A \in On \to ω \in On$
17		id	$⊢ A \in On \to A \in On$
18		peano1	$⊢ \emptyset \in ω$
19	18	ne0ii	$⊢ ω \neq \emptyset$
20	19	a1i	$⊢ A \in On \to ω \neq \emptyset$
21	16 17 20	3jca	$⊢ A \in On \to (ω \in On \land A \in On \land ω \neq \emptyset)$
22		omeulem1	$⊢ (ω \in On \land A \in On \land ω \neq \emptyset) \to \exists x \in On \exists y \in ω (ω \cdot_{𝑜} x) +_{𝑜} y = A$
23	14 21 22	3syl	$⊢ (A \in On \land Lim A) \to \exists x \in On \exists y \in ω (ω \cdot_{𝑜} x) +_{𝑜} y = A$
24		limeq	$⊢ (ω \cdot_{𝑜} x) +_{𝑜} y = A \to (Lim ((ω \cdot_{𝑜} x) +_{𝑜} y) \leftrightarrow Lim A)$
25	24	biimprd	$⊢ (ω \cdot_{𝑜} x) +_{𝑜} y = A \to (Lim A \to Lim ((ω \cdot_{𝑜} x) +_{𝑜} y))$
26		simplr	$⊢ ((x \in On \land y \in ω) \land \neg \emptyset \in x) \to y \in ω$
27		nnlim	$⊢ y \in ω \to \neg Lim y$
28	26 27	syl	$⊢ ((x \in On \land y \in ω) \land \neg \emptyset \in x) \to \neg Lim y$
29		on0eln0	$⊢ x \in On \to (\emptyset \in x \leftrightarrow x \neq \emptyset)$
30	29	biimprd	$⊢ x \in On \to (x \neq \emptyset \to \emptyset \in x)$
31	30	necon1bd	$⊢ x \in On \to (\neg \emptyset \in x \to x = \emptyset)$
32	31	adantr	$⊢ (x \in On \land y \in ω) \to (\neg \emptyset \in x \to x = \emptyset)$
33	32	imp	$⊢ ((x \in On \land y \in ω) \land \neg \emptyset \in x) \to x = \emptyset$
34	33 26	jca	$⊢ ((x \in On \land y \in ω) \land \neg \emptyset \in x) \to (x = \emptyset \land y \in ω)$
35		simpl	$⊢ (x = \emptyset \land y \in ω) \to x = \emptyset$
36	35	oveq2d	$⊢ (x = \emptyset \land y \in ω) \to ω \cdot_{𝑜} x = ω \cdot_{𝑜} \emptyset$
37		om0	$⊢ ω \in On \to ω \cdot_{𝑜} \emptyset = \emptyset$
38	15 37	mp1i	$⊢ (x = \emptyset \land y \in ω) \to ω \cdot_{𝑜} \emptyset = \emptyset$
39	36 38	eqtrd	$⊢ (x = \emptyset \land y \in ω) \to ω \cdot_{𝑜} x = \emptyset$
40	39	oveq1d	$⊢ (x = \emptyset \land y \in ω) \to (ω \cdot_{𝑜} x) +_{𝑜} y = \emptyset +_{𝑜} y$
41		nna0r	$⊢ y \in ω \to \emptyset +_{𝑜} y = y$
42	41	adantl	$⊢ (x = \emptyset \land y \in ω) \to \emptyset +_{𝑜} y = y$
43	40 42	eqtrd	$⊢ (x = \emptyset \land y \in ω) \to (ω \cdot_{𝑜} x) +_{𝑜} y = y$
44		limeq	$⊢ (ω \cdot_{𝑜} x) +_{𝑜} y = y \to (Lim ((ω \cdot_{𝑜} x) +_{𝑜} y) \leftrightarrow Lim y)$
45	34 43 44	3syl	$⊢ ((x \in On \land y \in ω) \land \neg \emptyset \in x) \to (Lim ((ω \cdot_{𝑜} x) +_{𝑜} y) \leftrightarrow Lim y)$
46	28 45	mtbird	$⊢ ((x \in On \land y \in ω) \land \neg \emptyset \in x) \to \neg Lim ((ω \cdot_{𝑜} x) +_{𝑜} y)$
47	46	ex	$⊢ (x \in On \land y \in ω) \to (\neg \emptyset \in x \to \neg Lim ((ω \cdot_{𝑜} x) +_{𝑜} y))$
48		ovex	$⊢ (ω \cdot_{𝑜} x) +_{𝑜} ⋃ y \in V$
49		nlimsucg	$⊢ (ω \cdot_{𝑜} x) +_{𝑜} ⋃ y \in V \to \neg Lim suc ((ω \cdot_{𝑜} x) +_{𝑜} ⋃ y)$
50	48 49	mp1i	$⊢ ((x \in On \land y \in ω) \land \neg y = \emptyset) \to \neg Lim suc ((ω \cdot_{𝑜} x) +_{𝑜} ⋃ y)$
51		nnord	$⊢ y \in ω \to Ord y$
52		orduniorsuc	$⊢ Ord y \to (y = ⋃ y \lor y = suc ⋃ y)$
53	51 52	syl	$⊢ y \in ω \to (y = ⋃ y \lor y = suc ⋃ y)$
54		3ianor	$⊢ \neg (Ord y \land y \neq \emptyset \land y = ⋃ y) \leftrightarrow (\neg Ord y \lor \neg y \neq \emptyset \lor \neg y = ⋃ y)$
55		df-lim	$⊢ Lim y \leftrightarrow (Ord y \land y \neq \emptyset \land y = ⋃ y)$
56	54 55	xchnxbir	$⊢ \neg Lim y \leftrightarrow (\neg Ord y \lor \neg y \neq \emptyset \lor \neg y = ⋃ y)$
57	27 56	sylib	$⊢ y \in ω \to (\neg Ord y \lor \neg y \neq \emptyset \lor \neg y = ⋃ y)$
58	51	pm2.24d	$⊢ y \in ω \to (\neg Ord y \to (y = ⋃ y \to y = \emptyset))$
59		nne	$⊢ \neg y \neq \emptyset \leftrightarrow y = \emptyset$
60	59	biimpi	$⊢ \neg y \neq \emptyset \to y = \emptyset$
61	60	a1i13	$⊢ y \in ω \to (\neg y \neq \emptyset \to (y = ⋃ y \to y = \emptyset))$
62		pm2.21	$⊢ \neg y = ⋃ y \to (y = ⋃ y \to y = \emptyset)$
63	62	a1i	$⊢ y \in ω \to (\neg y = ⋃ y \to (y = ⋃ y \to y = \emptyset))$
64	58 61 63	3jaod	$⊢ y \in ω \to ((\neg Ord y \lor \neg y \neq \emptyset \lor \neg y = ⋃ y) \to (y = ⋃ y \to y = \emptyset))$
65	57 64	mpd	$⊢ y \in ω \to (y = ⋃ y \to y = \emptyset)$
66	65	orim1d	$⊢ y \in ω \to ((y = ⋃ y \lor y = suc ⋃ y) \to (y = \emptyset \lor y = suc ⋃ y))$
67	53 66	mpd	$⊢ y \in ω \to (y = \emptyset \lor y = suc ⋃ y)$
68	67	ord	$⊢ y \in ω \to (\neg y = \emptyset \to y = suc ⋃ y)$
69	68	adantl	$⊢ (x \in On \land y \in ω) \to (\neg y = \emptyset \to y = suc ⋃ y)$
70	69	imp	$⊢ ((x \in On \land y \in ω) \land \neg y = \emptyset) \to y = suc ⋃ y$
71	70	oveq2d	$⊢ ((x \in On \land y \in ω) \land \neg y = \emptyset) \to (ω \cdot_{𝑜} x) +_{𝑜} y = (ω \cdot_{𝑜} x) +_{𝑜} suc ⋃ y$
72		simpl	$⊢ (x \in On \land y \in ω) \to x \in On$
73	72	adantr	$⊢ ((x \in On \land y \in ω) \land \neg y = \emptyset) \to x \in On$
74		omcl	$⊢ (ω \in On \land x \in On) \to ω \cdot_{𝑜} x \in On$
75	15 73 74	sylancr	$⊢ ((x \in On \land y \in ω) \land \neg y = \emptyset) \to ω \cdot_{𝑜} x \in On$
76		nnon	$⊢ y \in ω \to y \in On$
77		onuni	$⊢ y \in On \to ⋃ y \in On$
78	76 77	syl	$⊢ y \in ω \to ⋃ y \in On$
79	78	adantl	$⊢ (x \in On \land y \in ω) \to ⋃ y \in On$
80	79	adantr	$⊢ ((x \in On \land y \in ω) \land \neg y = \emptyset) \to ⋃ y \in On$
81		oasuc	$⊢ (ω \cdot_{𝑜} x \in On \land ⋃ y \in On) \to (ω \cdot_{𝑜} x) +_{𝑜} suc ⋃ y = suc ((ω \cdot_{𝑜} x) +_{𝑜} ⋃ y)$
82	75 80 81	syl2anc	$⊢ ((x \in On \land y \in ω) \land \neg y = \emptyset) \to (ω \cdot_{𝑜} x) +_{𝑜} suc ⋃ y = suc ((ω \cdot_{𝑜} x) +_{𝑜} ⋃ y)$
83	71 82	eqtrd	$⊢ ((x \in On \land y \in ω) \land \neg y = \emptyset) \to (ω \cdot_{𝑜} x) +_{𝑜} y = suc ((ω \cdot_{𝑜} x) +_{𝑜} ⋃ y)$
84		limeq	$⊢ (ω \cdot_{𝑜} x) +_{𝑜} y = suc ((ω \cdot_{𝑜} x) +_{𝑜} ⋃ y) \to (Lim ((ω \cdot_{𝑜} x) +_{𝑜} y) \leftrightarrow Lim suc ((ω \cdot_{𝑜} x) +_{𝑜} ⋃ y))$
85	83 84	syl	$⊢ ((x \in On \land y \in ω) \land \neg y = \emptyset) \to (Lim ((ω \cdot_{𝑜} x) +_{𝑜} y) \leftrightarrow Lim suc ((ω \cdot_{𝑜} x) +_{𝑜} ⋃ y))$
86	50 85	mtbird	$⊢ ((x \in On \land y \in ω) \land \neg y = \emptyset) \to \neg Lim ((ω \cdot_{𝑜} x) +_{𝑜} y)$
87	86	ex	$⊢ (x \in On \land y \in ω) \to (\neg y = \emptyset \to \neg Lim ((ω \cdot_{𝑜} x) +_{𝑜} y))$
88	47 87	jaod	$⊢ (x \in On \land y \in ω) \to ((\neg \emptyset \in x \lor \neg y = \emptyset) \to \neg Lim ((ω \cdot_{𝑜} x) +_{𝑜} y))$
89	88	con2d	$⊢ (x \in On \land y \in ω) \to (Lim ((ω \cdot_{𝑜} x) +_{𝑜} y) \to \neg (\neg \emptyset \in x \lor \neg y = \emptyset))$
90		anor	$⊢ (\emptyset \in x \land y = \emptyset) \leftrightarrow \neg (\neg \emptyset \in x \lor \neg y = \emptyset)$
91	89 90	imbitrrdi	$⊢ (x \in On \land y \in ω) \to (Lim ((ω \cdot_{𝑜} x) +_{𝑜} y) \to (\emptyset \in x \land y = \emptyset))$
92	25 91	syl9	$⊢ (ω \cdot_{𝑜} x) +_{𝑜} y = A \to ((x \in On \land y \in ω) \to (Lim A \to (\emptyset \in x \land y = \emptyset)))$
93	92	com13	$⊢ Lim A \to ((x \in On \land y \in ω) \to ((ω \cdot_{𝑜} x) +_{𝑜} y = A \to (\emptyset \in x \land y = \emptyset)))$
94	93	adantl	$⊢ (A \in On \land Lim A) \to ((x \in On \land y \in ω) \to ((ω \cdot_{𝑜} x) +_{𝑜} y = A \to (\emptyset \in x \land y = \emptyset)))$
95	94	3imp	$⊢ ((A \in On \land Lim A) \land (x \in On \land y \in ω) \land (ω \cdot_{𝑜} x) +_{𝑜} y = A) \to (\emptyset \in x \land y = \emptyset)$
96		simp2	$⊢ ((A \in On \land Lim A) \land (x \in On \land y \in ω) \land (ω \cdot_{𝑜} x) +_{𝑜} y = A) \to (x \in On \land y \in ω)$
97	96 72	syl	$⊢ ((A \in On \land Lim A) \land (x \in On \land y \in ω) \land (ω \cdot_{𝑜} x) +_{𝑜} y = A) \to x \in On$
98		simpl	$⊢ (\emptyset \in x \land y = \emptyset) \to \emptyset \in x$
99	97 98	anim12i	$⊢ (((A \in On \land Lim A) \land (x \in On \land y \in ω) \land (ω \cdot_{𝑜} x) +_{𝑜} y = A) \land (\emptyset \in x \land y = \emptyset)) \to (x \in On \land \emptyset \in x)$
100		ondif1	$⊢ x \in (On ∖ 1_{𝑜}) \leftrightarrow (x \in On \land \emptyset \in x)$
101	99 100	sylibr	$⊢ (((A \in On \land Lim A) \land (x \in On \land y \in ω) \land (ω \cdot_{𝑜} x) +_{𝑜} y = A) \land (\emptyset \in x \land y = \emptyset)) \to x \in (On ∖ 1_{𝑜})$
102		simpr	$⊢ (\emptyset \in x \land y = \emptyset) \to y = \emptyset$
103	102	oveq2d	$⊢ (\emptyset \in x \land y = \emptyset) \to (ω \cdot_{𝑜} x) +_{𝑜} y = (ω \cdot_{𝑜} x) +_{𝑜} \emptyset$
104	103	adantl	$⊢ (((A \in On \land Lim A) \land (x \in On \land y \in ω) \land (ω \cdot_{𝑜} x) +_{𝑜} y = A) \land (\emptyset \in x \land y = \emptyset)) \to (ω \cdot_{𝑜} x) +_{𝑜} y = (ω \cdot_{𝑜} x) +_{𝑜} \emptyset$
105		simpl3	$⊢ (((A \in On \land Lim A) \land (x \in On \land y \in ω) \land (ω \cdot_{𝑜} x) +_{𝑜} y = A) \land (\emptyset \in x \land y = \emptyset)) \to (ω \cdot_{𝑜} x) +_{𝑜} y = A$
106	15 72 74	sylancr	$⊢ (x \in On \land y \in ω) \to ω \cdot_{𝑜} x \in On$
107		oa0	$⊢ ω \cdot_{𝑜} x \in On \to (ω \cdot_{𝑜} x) +_{𝑜} \emptyset = ω \cdot_{𝑜} x$
108	96 106 107	3syl	$⊢ ((A \in On \land Lim A) \land (x \in On \land y \in ω) \land (ω \cdot_{𝑜} x) +_{𝑜} y = A) \to (ω \cdot_{𝑜} x) +_{𝑜} \emptyset = ω \cdot_{𝑜} x$
109	108	adantr	$⊢ (((A \in On \land Lim A) \land (x \in On \land y \in ω) \land (ω \cdot_{𝑜} x) +_{𝑜} y = A) \land (\emptyset \in x \land y = \emptyset)) \to (ω \cdot_{𝑜} x) +_{𝑜} \emptyset = ω \cdot_{𝑜} x$
110	104 105 109	3eqtr3d	$⊢ (((A \in On \land Lim A) \land (x \in On \land y \in ω) \land (ω \cdot_{𝑜} x) +_{𝑜} y = A) \land (\emptyset \in x \land y = \emptyset)) \to A = ω \cdot_{𝑜} x$
111	101 110	jca	$⊢ (((A \in On \land Lim A) \land (x \in On \land y \in ω) \land (ω \cdot_{𝑜} x) +_{𝑜} y = A) \land (\emptyset \in x \land y = \emptyset)) \to (x \in (On ∖ 1_{𝑜}) \land A = ω \cdot_{𝑜} x)$
112	95 111	mpdan	$⊢ ((A \in On \land Lim A) \land (x \in On \land y \in ω) \land (ω \cdot_{𝑜} x) +_{𝑜} y = A) \to (x \in (On ∖ 1_{𝑜}) \land A = ω \cdot_{𝑜} x)$
113	112	3exp	$⊢ (A \in On \land Lim A) \to ((x \in On \land y \in ω) \to ((ω \cdot_{𝑜} x) +_{𝑜} y = A \to (x \in (On ∖ 1_{𝑜}) \land A = ω \cdot_{𝑜} x)))$
114	113	expdimp	$⊢ ((A \in On \land Lim A) \land x \in On) \to (y \in ω \to ((ω \cdot_{𝑜} x) +_{𝑜} y = A \to (x \in (On ∖ 1_{𝑜}) \land A = ω \cdot_{𝑜} x)))$
115	114	rexlimdv	$⊢ ((A \in On \land Lim A) \land x \in On) \to (\exists y \in ω (ω \cdot_{𝑜} x) +_{𝑜} y = A \to (x \in (On ∖ 1_{𝑜}) \land A = ω \cdot_{𝑜} x))$
116	115	expimpd	$⊢ (A \in On \land Lim A) \to ((x \in On \land \exists y \in ω (ω \cdot_{𝑜} x) +_{𝑜} y = A) \to (x \in (On ∖ 1_{𝑜}) \land A = ω \cdot_{𝑜} x))$
117	116	reximdv2	$⊢ (A \in On \land Lim A) \to (\exists x \in On \exists y \in ω (ω \cdot_{𝑜} x) +_{𝑜} y = A \to \exists x \in (On ∖ 1_{𝑜}) A = ω \cdot_{𝑜} x)$
118	23 117	mpd	$⊢ (A \in On \land Lim A) \to \exists x \in (On ∖ 1_{𝑜}) A = ω \cdot_{𝑜} x$
119		simpr	$⊢ (x \in (On ∖ 1_{𝑜}) \land A = ω \cdot_{𝑜} x) \to A = ω \cdot_{𝑜} x$
120		eldifi	$⊢ x \in (On ∖ 1_{𝑜}) \to x \in On$
121	15 120 74	sylancr	$⊢ x \in (On ∖ 1_{𝑜}) \to ω \cdot_{𝑜} x \in On$
122	121	adantr	$⊢ (x \in (On ∖ 1_{𝑜}) \land A = ω \cdot_{𝑜} x) \to ω \cdot_{𝑜} x \in On$
123	119 122	eqeltrd	$⊢ (x \in (On ∖ 1_{𝑜}) \land A = ω \cdot_{𝑜} x) \to A \in On$
124		limom	$⊢ Lim ω$
125	15 124	pm3.2i	$⊢ (ω \in On \land Lim ω)$
126		omlimcl2	$⊢ ((x \in On \land (ω \in On \land Lim ω)) \land \emptyset \in x) \to Lim (ω \cdot_{𝑜} x)$
127	125 126	mpanl2	$⊢ (x \in On \land \emptyset \in x) \to Lim (ω \cdot_{𝑜} x)$
128	100 127	sylbi	$⊢ x \in (On ∖ 1_{𝑜}) \to Lim (ω \cdot_{𝑜} x)$
129	128	adantr	$⊢ (x \in (On ∖ 1_{𝑜}) \land A = ω \cdot_{𝑜} x) \to Lim (ω \cdot_{𝑜} x)$
130		limeq	$⊢ A = ω \cdot_{𝑜} x \to (Lim A \leftrightarrow Lim (ω \cdot_{𝑜} x))$
131	130	adantl	$⊢ (x \in (On ∖ 1_{𝑜}) \land A = ω \cdot_{𝑜} x) \to (Lim A \leftrightarrow Lim (ω \cdot_{𝑜} x))$
132	129 131	mpbird	$⊢ (x \in (On ∖ 1_{𝑜}) \land A = ω \cdot_{𝑜} x) \to Lim A$
133	123 132	jca	$⊢ (x \in (On ∖ 1_{𝑜}) \land A = ω \cdot_{𝑜} x) \to (A \in On \land Lim A)$
134	133	rexlimiva	$⊢ \exists x \in (On ∖ 1_{𝑜}) A = ω \cdot_{𝑜} x \to (A \in On \land Lim A)$
135	118 134	impbii	$⊢ (A \in On \land Lim A) \leftrightarrow \exists x \in (On ∖ 1_{𝑜}) A = ω \cdot_{𝑜} x$
136	135	orbi2i	$⊢ (A = On \lor (A \in On \land Lim A)) \leftrightarrow (A = On \lor \exists x \in (On ∖ 1_{𝑜}) A = ω \cdot_{𝑜} x)$
137	8 13 136	3bitr2i	$⊢ Lim A \leftrightarrow (A = On \lor \exists x \in (On ∖ 1_{𝑜}) A = ω \cdot_{𝑜} x)$

Metamath Proof Explorer

Theorem dflim5

Proof