cflim2

Description: The cofinality function is a limit ordinal iff its argument is. (Contributed by Mario Carneiro, 28-Feb-2013) (Revised by Mario Carneiro, 15-Sep-2013)

		Ref	Expression
	Hypothesis	cflim2.1	$⊢ A \in V$
	Assertion	cflim2	$⊢ Lim A \leftrightarrow Lim cf (A)$

Proof

Step	Hyp	Ref	Expression
1		cflim2.1	$⊢ A \in V$
2		rabid	$⊢ y \in \{y \in 𝒫 A \| ⋃ y = A\} \leftrightarrow (y \in 𝒫 A \land ⋃ y = A)$
3		velpw	$⊢ y \in 𝒫 A \leftrightarrow y \subseteq A$
4		limord	$⊢ Lim A \to Ord A$
5		ordsson	$⊢ Ord A \to A \subseteq On$
6		sstr	$⊢ (y \subseteq A \land A \subseteq On) \to y \subseteq On$
7	6	expcom	$⊢ A \subseteq On \to (y \subseteq A \to y \subseteq On)$
8	4 5 7	3syl	$⊢ Lim A \to (y \subseteq A \to y \subseteq On)$
9	8	imp	$⊢ (Lim A \land y \subseteq A) \to y \subseteq On$
10	9	3adant3	$⊢ (Lim A \land y \subseteq A \land ⋃ y = A) \to y \subseteq On$
11		ssel2	$⊢ (y \subseteq On \land s \in y) \to s \in On$
12		eloni	$⊢ s \in On \to Ord s$
13		ordirr	$⊢ Ord s \to \neg s \in s$
14	11 12 13	3syl	$⊢ (y \subseteq On \land s \in y) \to \neg s \in s$
15		ssel	$⊢ y \subseteq s \to (s \in y \to s \in s)$
16	15	com12	$⊢ s \in y \to (y \subseteq s \to s \in s)$
17	16	adantl	$⊢ (y \subseteq On \land s \in y) \to (y \subseteq s \to s \in s)$
18	14 17	mtod	$⊢ (y \subseteq On \land s \in y) \to \neg y \subseteq s$
19	10 18	sylan	$⊢ ((Lim A \land y \subseteq A \land ⋃ y = A) \land s \in y) \to \neg y \subseteq s$
20		simpl2	$⊢ ((Lim A \land y \subseteq A \land ⋃ y = A) \land s \in y) \to y \subseteq A$
21		sstr	$⊢ (y \subseteq A \land A \subseteq s) \to y \subseteq s$
22	20 21	sylan	$⊢ (((Lim A \land y \subseteq A \land ⋃ y = A) \land s \in y) \land A \subseteq s) \to y \subseteq s$
23	19 22	mtand	$⊢ ((Lim A \land y \subseteq A \land ⋃ y = A) \land s \in y) \to \neg A \subseteq s$
24		simpl3	$⊢ ((Lim A \land y \subseteq A \land ⋃ y = A) \land s \in y) \to ⋃ y = A$
25	24	sseq1d	$⊢ ((Lim A \land y \subseteq A \land ⋃ y = A) \land s \in y) \to (⋃ y \subseteq s \leftrightarrow A \subseteq s)$
26	23 25	mtbird	$⊢ ((Lim A \land y \subseteq A \land ⋃ y = A) \land s \in y) \to \neg ⋃ y \subseteq s$
27		unissb	$⊢ ⋃ y \subseteq s \leftrightarrow \forall t \in y t \subseteq s$
28	26 27	sylnib	$⊢ ((Lim A \land y \subseteq A \land ⋃ y = A) \land s \in y) \to \neg \forall t \in y t \subseteq s$
29	28	nrexdv	$⊢ (Lim A \land y \subseteq A \land ⋃ y = A) \to \neg \exists s \in y \forall t \in y t \subseteq s$
30		ssel	$⊢ y \subseteq On \to (s \in y \to s \in On)$
31		ssel	$⊢ y \subseteq On \to (t \in y \to t \in On)$
32		ontri1	$⊢ (t \in On \land s \in On) \to (t \subseteq s \leftrightarrow \neg s \in t)$
33	32	ancoms	$⊢ (s \in On \land t \in On) \to (t \subseteq s \leftrightarrow \neg s \in t)$
34		vex	$⊢ t \in V$
35		vex	$⊢ s \in V$
36	34 35	brcnv	$⊢ t E^{-1} s \leftrightarrow s E t$
37		epel	$⊢ s E t \leftrightarrow s \in t$
38	36 37	bitri	$⊢ t E^{-1} s \leftrightarrow s \in t$
39	38	notbii	$⊢ \neg t E^{-1} s \leftrightarrow \neg s \in t$
40	33 39	bitr4di	$⊢ (s \in On \land t \in On) \to (t \subseteq s \leftrightarrow \neg t E^{-1} s)$
41	40	a1i	$⊢ y \subseteq On \to ((s \in On \land t \in On) \to (t \subseteq s \leftrightarrow \neg t E^{-1} s))$
42	30 31 41	syl2and	$⊢ y \subseteq On \to ((s \in y \land t \in y) \to (t \subseteq s \leftrightarrow \neg t E^{-1} s))$
43	42	impl	$⊢ ((y \subseteq On \land s \in y) \land t \in y) \to (t \subseteq s \leftrightarrow \neg t E^{-1} s)$
44	43	ralbidva	$⊢ (y \subseteq On \land s \in y) \to (\forall t \in y t \subseteq s \leftrightarrow \forall t \in y \neg t E^{-1} s)$
45	44	rexbidva	$⊢ y \subseteq On \to (\exists s \in y \forall t \in y t \subseteq s \leftrightarrow \exists s \in y \forall t \in y \neg t E^{-1} s)$
46	10 45	syl	$⊢ (Lim A \land y \subseteq A \land ⋃ y = A) \to (\exists s \in y \forall t \in y t \subseteq s \leftrightarrow \exists s \in y \forall t \in y \neg t E^{-1} s)$
47	29 46	mtbid	$⊢ (Lim A \land y \subseteq A \land ⋃ y = A) \to \neg \exists s \in y \forall t \in y \neg t E^{-1} s$
48		vex	$⊢ y \in V$
49	48	a1i	$⊢ ((Lim A \land y \subseteq A \land ⋃ y = A) \land card (y) \in ω) \to y \in V$
50		epweon	$⊢ E We On$
51		wess	$⊢ y \subseteq On \to (E We On \to E We y)$
52	50 51	mpi	$⊢ y \subseteq On \to E We y$
53		weso	$⊢ E We y \to E Or y$
54	52 53	syl	$⊢ y \subseteq On \to E Or y$
55		cnvso	$⊢ E Or y \leftrightarrow E^{-1} Or y$
56	54 55	sylib	$⊢ y \subseteq On \to E^{-1} Or y$
57		onssnum	$⊢ (y \in V \land y \subseteq On) \to y \in dom card$
58	48 57	mpan	$⊢ y \subseteq On \to y \in dom card$
59		cardid2	$⊢ y \in dom card \to card (y) \approx y$
60		ensym	$⊢ card (y) \approx y \to y \approx card (y)$
61	58 59 60	3syl	$⊢ y \subseteq On \to y \approx card (y)$
62		nnsdom	$⊢ card (y) \in ω \to card (y) ≺ ω$
63		ensdomtr	$⊢ (y \approx card (y) \land card (y) ≺ ω) \to y ≺ ω$
64	61 62 63	syl2an	$⊢ (y \subseteq On \land card (y) \in ω) \to y ≺ ω$
65		isfinite	$⊢ y \in Fin \leftrightarrow y ≺ ω$
66	64 65	sylibr	$⊢ (y \subseteq On \land card (y) \in ω) \to y \in Fin$
67		wofi	$⊢ (E^{-1} Or y \land y \in Fin) \to E^{-1} We y$
68	56 66 67	syl2an2r	$⊢ (y \subseteq On \land card (y) \in ω) \to E^{-1} We y$
69	10 68	sylan	$⊢ ((Lim A \land y \subseteq A \land ⋃ y = A) \land card (y) \in ω) \to E^{-1} We y$
70		wefr	$⊢ E^{-1} We y \to E^{-1} Fr y$
71	69 70	syl	$⊢ ((Lim A \land y \subseteq A \land ⋃ y = A) \land card (y) \in ω) \to E^{-1} Fr y$
72		ssidd	$⊢ ((Lim A \land y \subseteq A \land ⋃ y = A) \land card (y) \in ω) \to y \subseteq y$
73		unieq	$⊢ y = \emptyset \to ⋃ y = ⋃ \emptyset$
74		uni0	$⊢ ⋃ \emptyset = \emptyset$
75	73 74	eqtrdi	$⊢ y = \emptyset \to ⋃ y = \emptyset$
76		eqeq1	$⊢ ⋃ y = A \to (⋃ y = \emptyset \leftrightarrow A = \emptyset)$
77	75 76	imbitrid	$⊢ ⋃ y = A \to (y = \emptyset \to A = \emptyset)$
78		nlim0	$⊢ \neg Lim \emptyset$
79		limeq	$⊢ A = \emptyset \to (Lim A \leftrightarrow Lim \emptyset)$
80	78 79	mtbiri	$⊢ A = \emptyset \to \neg Lim A$
81	77 80	syl6	$⊢ ⋃ y = A \to (y = \emptyset \to \neg Lim A)$
82	81	necon2ad	$⊢ ⋃ y = A \to (Lim A \to y \neq \emptyset)$
83	82	impcom	$⊢ (Lim A \land ⋃ y = A) \to y \neq \emptyset$
84	83	3adant2	$⊢ (Lim A \land y \subseteq A \land ⋃ y = A) \to y \neq \emptyset$
85	84	adantr	$⊢ ((Lim A \land y \subseteq A \land ⋃ y = A) \land card (y) \in ω) \to y \neq \emptyset$
86		fri	$⊢ ((y \in V \land E^{-1} Fr y) \land (y \subseteq y \land y \neq \emptyset)) \to \exists s \in y \forall t \in y \neg t E^{-1} s$
87	49 71 72 85 86	syl22anc	$⊢ ((Lim A \land y \subseteq A \land ⋃ y = A) \land card (y) \in ω) \to \exists s \in y \forall t \in y \neg t E^{-1} s$
88	47 87	mtand	$⊢ (Lim A \land y \subseteq A \land ⋃ y = A) \to \neg card (y) \in ω$
89		cardon	$⊢ card (y) \in On$
90		eloni	$⊢ card (y) \in On \to Ord card (y)$
91		ordom	$⊢ Ord ω$
92		ordtri1	$⊢ (Ord ω \land Ord card (y)) \to (ω \subseteq card (y) \leftrightarrow \neg card (y) \in ω)$
93	91 92	mpan	$⊢ Ord card (y) \to (ω \subseteq card (y) \leftrightarrow \neg card (y) \in ω)$
94	89 90 93	mp2b	$⊢ ω \subseteq card (y) \leftrightarrow \neg card (y) \in ω$
95	88 94	sylibr	$⊢ (Lim A \land y \subseteq A \land ⋃ y = A) \to ω \subseteq card (y)$
96	3 95	syl3an2b	$⊢ (Lim A \land y \in 𝒫 A \land ⋃ y = A) \to ω \subseteq card (y)$
97	96	3expb	$⊢ (Lim A \land (y \in 𝒫 A \land ⋃ y = A)) \to ω \subseteq card (y)$
98	2 97	sylan2b	$⊢ (Lim A \land y \in \{y \in 𝒫 A \| ⋃ y = A\}) \to ω \subseteq card (y)$
99	98	ralrimiva	$⊢ Lim A \to \forall y \in \{y \in 𝒫 A \| ⋃ y = A\} ω \subseteq card (y)$
100		ssiin	$⊢ ω \subseteq ⋂_{y \in \{y \in 𝒫 A \| ⋃ y = A\}} card (y) \leftrightarrow \forall y \in \{y \in 𝒫 A \| ⋃ y = A\} ω \subseteq card (y)$
101	99 100	sylibr	$⊢ Lim A \to ω \subseteq ⋂_{y \in \{y \in 𝒫 A \| ⋃ y = A\}} card (y)$
102	1	cflim3	$⊢ Lim A \to cf (A) = ⋂_{y \in \{y \in 𝒫 A \| ⋃ y = A\}} card (y)$
103	101 102	sseqtrrd	$⊢ Lim A \to ω \subseteq cf (A)$
104		fvex	$⊢ card (y) \in V$
105	104	dfiin2	$⊢ ⋂_{y \in \{y \in 𝒫 A \| ⋃ y = A\}} card (y) = ⋂ \{x \| \exists y \in \{y \in 𝒫 A \| ⋃ y = A\} x = card (y)\}$
106	102 105	eqtrdi	$⊢ Lim A \to cf (A) = ⋂ \{x \| \exists y \in \{y \in 𝒫 A \| ⋃ y = A\} x = card (y)\}$
107		cardlim	$⊢ ω \subseteq card (y) \leftrightarrow Lim card (y)$
108		sseq2	$⊢ x = card (y) \to (ω \subseteq x \leftrightarrow ω \subseteq card (y))$
109		limeq	$⊢ x = card (y) \to (Lim x \leftrightarrow Lim card (y))$
110	108 109	bibi12d	$⊢ x = card (y) \to ((ω \subseteq x \leftrightarrow Lim x) \leftrightarrow (ω \subseteq card (y) \leftrightarrow Lim card (y)))$
111	107 110	mpbiri	$⊢ x = card (y) \to (ω \subseteq x \leftrightarrow Lim x)$
112	111	rexlimivw	$⊢ \exists y \in \{y \in 𝒫 A \| ⋃ y = A\} x = card (y) \to (ω \subseteq x \leftrightarrow Lim x)$
113	112	ss2abi	$⊢ \{x \| \exists y \in \{y \in 𝒫 A \| ⋃ y = A\} x = card (y)\} \subseteq \{x \| (ω \subseteq x \leftrightarrow Lim x)\}$
114		eleq1	$⊢ x = card (y) \to (x \in On \leftrightarrow card (y) \in On)$
115	89 114	mpbiri	$⊢ x = card (y) \to x \in On$
116	115	rexlimivw	$⊢ \exists y \in \{y \in 𝒫 A \| ⋃ y = A\} x = card (y) \to x \in On$
117	116	abssi	$⊢ \{x \| \exists y \in \{y \in 𝒫 A \| ⋃ y = A\} x = card (y)\} \subseteq On$
118		fvex	$⊢ cf (A) \in V$
119	106 118	eqeltrrdi	$⊢ Lim A \to ⋂ \{x \| \exists y \in \{y \in 𝒫 A \| ⋃ y = A\} x = card (y)\} \in V$
120		intex	$⊢ \{x \| \exists y \in \{y \in 𝒫 A \| ⋃ y = A\} x = card (y)\} \neq \emptyset \leftrightarrow ⋂ \{x \| \exists y \in \{y \in 𝒫 A \| ⋃ y = A\} x = card (y)\} \in V$
121	119 120	sylibr	$⊢ Lim A \to \{x \| \exists y \in \{y \in 𝒫 A \| ⋃ y = A\} x = card (y)\} \neq \emptyset$
122		onint	$⊢ (\{x \| \exists y \in \{y \in 𝒫 A \| ⋃ y = A\} x = card (y)\} \subseteq On \land \{x \| \exists y \in \{y \in 𝒫 A \| ⋃ y = A\} x = card (y)\} \neq \emptyset) \to ⋂ \{x \| \exists y \in \{y \in 𝒫 A \| ⋃ y = A\} x = card (y)\} \in \{x \| \exists y \in \{y \in 𝒫 A \| ⋃ y = A\} x = card (y)\}$
123	117 121 122	sylancr	$⊢ Lim A \to ⋂ \{x \| \exists y \in \{y \in 𝒫 A \| ⋃ y = A\} x = card (y)\} \in \{x \| \exists y \in \{y \in 𝒫 A \| ⋃ y = A\} x = card (y)\}$
124	113 123	sselid	$⊢ Lim A \to ⋂ \{x \| \exists y \in \{y \in 𝒫 A \| ⋃ y = A\} x = card (y)\} \in \{x \| (ω \subseteq x \leftrightarrow Lim x)\}$
125	106 124	eqeltrd	$⊢ Lim A \to cf (A) \in \{x \| (ω \subseteq x \leftrightarrow Lim x)\}$
126		sseq2	$⊢ x = cf (A) \to (ω \subseteq x \leftrightarrow ω \subseteq cf (A))$
127		limeq	$⊢ x = cf (A) \to (Lim x \leftrightarrow Lim cf (A))$
128	126 127	bibi12d	$⊢ x = cf (A) \to ((ω \subseteq x \leftrightarrow Lim x) \leftrightarrow (ω \subseteq cf (A) \leftrightarrow Lim cf (A)))$
129	118 128	elab	$⊢ cf (A) \in \{x \| (ω \subseteq x \leftrightarrow Lim x)\} \leftrightarrow (ω \subseteq cf (A) \leftrightarrow Lim cf (A))$
130	125 129	sylib	$⊢ Lim A \to (ω \subseteq cf (A) \leftrightarrow Lim cf (A))$
131	103 130	mpbid	$⊢ Lim A \to Lim cf (A)$
132		eloni	$⊢ A \in On \to Ord A$
133		ordzsl	$⊢ Ord A \leftrightarrow (A = \emptyset \lor \exists x \in On A = suc x \lor Lim A)$
134	132 133	sylib	$⊢ A \in On \to (A = \emptyset \lor \exists x \in On A = suc x \lor Lim A)$
135		df-3or	$⊢ (A = \emptyset \lor \exists x \in On A = suc x \lor Lim A) \leftrightarrow ((A = \emptyset \lor \exists x \in On A = suc x) \lor Lim A)$
136		orcom	$⊢ ((A = \emptyset \lor \exists x \in On A = suc x) \lor Lim A) \leftrightarrow (Lim A \lor (A = \emptyset \lor \exists x \in On A = suc x))$
137		df-or	$⊢ (Lim A \lor (A = \emptyset \lor \exists x \in On A = suc x)) \leftrightarrow (\neg Lim A \to (A = \emptyset \lor \exists x \in On A = suc x))$
138	135 136 137	3bitri	$⊢ (A = \emptyset \lor \exists x \in On A = suc x \lor Lim A) \leftrightarrow (\neg Lim A \to (A = \emptyset \lor \exists x \in On A = suc x))$
139	134 138	sylib	$⊢ A \in On \to (\neg Lim A \to (A = \emptyset \lor \exists x \in On A = suc x))$
140		fveq2	$⊢ A = \emptyset \to cf (A) = cf (\emptyset)$
141		cf0	$⊢ cf (\emptyset) = \emptyset$
142	140 141	eqtrdi	$⊢ A = \emptyset \to cf (A) = \emptyset$
143		limeq	$⊢ cf (A) = \emptyset \to (Lim cf (A) \leftrightarrow Lim \emptyset)$
144	142 143	syl	$⊢ A = \emptyset \to (Lim cf (A) \leftrightarrow Lim \emptyset)$
145	78 144	mtbiri	$⊢ A = \emptyset \to \neg Lim cf (A)$
146		1n0	$⊢ 1_{𝑜} \neq \emptyset$
147		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
148	147	unieqi	$⊢ ⋃ 1_{𝑜} = ⋃ \{\emptyset\}$
149		0ex	$⊢ \emptyset \in V$
150	149	unisn	$⊢ ⋃ \{\emptyset\} = \emptyset$
151	148 150	eqtri	$⊢ ⋃ 1_{𝑜} = \emptyset$
152	146 151	neeqtrri	$⊢ 1_{𝑜} \neq ⋃ 1_{𝑜}$
153		limuni	$⊢ Lim 1_{𝑜} \to 1_{𝑜} = ⋃ 1_{𝑜}$
154	153	necon3ai	$⊢ 1_{𝑜} \neq ⋃ 1_{𝑜} \to \neg Lim 1_{𝑜}$
155	152 154	ax-mp	$⊢ \neg Lim 1_{𝑜}$
156		fveq2	$⊢ A = suc x \to cf (A) = cf (suc x)$
157		cfsuc	$⊢ x \in On \to cf (suc x) = 1_{𝑜}$
158	156 157	sylan9eqr	$⊢ (x \in On \land A = suc x) \to cf (A) = 1_{𝑜}$
159		limeq	$⊢ cf (A) = 1_{𝑜} \to (Lim cf (A) \leftrightarrow Lim 1_{𝑜})$
160	158 159	syl	$⊢ (x \in On \land A = suc x) \to (Lim cf (A) \leftrightarrow Lim 1_{𝑜})$
161	155 160	mtbiri	$⊢ (x \in On \land A = suc x) \to \neg Lim cf (A)$
162	161	rexlimiva	$⊢ \exists x \in On A = suc x \to \neg Lim cf (A)$
163	145 162	jaoi	$⊢ (A = \emptyset \lor \exists x \in On A = suc x) \to \neg Lim cf (A)$
164	139 163	syl6	$⊢ A \in On \to (\neg Lim A \to \neg Lim cf (A))$
165	164	con4d	$⊢ A \in On \to (Lim cf (A) \to Lim A)$
166		cff	$⊢ cf : On ⟶ On$
167	166	fdmi	$⊢ dom cf = On$
168	167	eleq2i	$⊢ A \in dom cf \leftrightarrow A \in On$
169		ndmfv	$⊢ \neg A \in dom cf \to cf (A) = \emptyset$
170	168 169	sylnbir	$⊢ \neg A \in On \to cf (A) = \emptyset$
171	170 143	syl	$⊢ \neg A \in On \to (Lim cf (A) \leftrightarrow Lim \emptyset)$
172	78 171	mtbiri	$⊢ \neg A \in On \to \neg Lim cf (A)$
173	172	pm2.21d	$⊢ \neg A \in On \to (Lim cf (A) \to Lim A)$
174	165 173	pm2.61i	$⊢ Lim cf (A) \to Lim A$
175	131 174	impbii	$⊢ Lim A \leftrightarrow Lim cf (A)$

Metamath Proof Explorer

Theorem cflim2

Proof