Theorem cflim2 9950

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.)

Hypothesis

Ref	Expression
cflim2.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
cflim2	⊢ (Lim 𝐴 ↔ Lim (cf‘𝐴))

Proof of Theorem cflim2

Dummy variables 𝑠 𝑦 𝑥 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rabid 3304	. . . . . . 7 ⊢ (𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} ↔ (𝑦 ∈ 𝒫 𝐴 ∧ ∪ 𝑦 = 𝐴))
2		velpw 4535	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴)
3		limord 6310	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Lim 𝐴 → Ord 𝐴)
4		ordsson 7610	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Ord 𝐴 → 𝐴 ⊆ On)
5		sstr 3925	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ On) → 𝑦 ⊆ On)
6	5	expcom 413	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ⊆ On → (𝑦 ⊆ 𝐴 → 𝑦 ⊆ On))
7	3, 4, 6	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (Lim 𝐴 → (𝑦 ⊆ 𝐴 → 𝑦 ⊆ On))
8	7	imp 406	. . . . . . . . . . . . . . . . . 18 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴) → 𝑦 ⊆ On)
9	8	3adant3 1130	. . . . . . . . . . . . . . . . 17 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → 𝑦 ⊆ On)
10		ssel2 3912	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → 𝑠 ∈ On)
11		eloni 6261	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ On → Ord 𝑠)
12		ordirr 6269	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord 𝑠 → ¬ 𝑠 ∈ 𝑠)
13	10, 11, 12	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → ¬ 𝑠 ∈ 𝑠)
14		ssel 3910	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ⊆ 𝑠 → (𝑠 ∈ 𝑦 → 𝑠 ∈ 𝑠))
15	14	com12 32	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ 𝑦 → (𝑦 ⊆ 𝑠 → 𝑠 ∈ 𝑠))
16	15	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → (𝑦 ⊆ 𝑠 → 𝑠 ∈ 𝑠))
17	13, 16	mtod 197	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → ¬ 𝑦 ⊆ 𝑠)
18	9, 17	sylan 579	. . . . . . . . . . . . . . . 16 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ¬ 𝑦 ⊆ 𝑠)
19		simpl2 1190	. . . . . . . . . . . . . . . . 17 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → 𝑦 ⊆ 𝐴)
20		sstr 3925	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑠) → 𝑦 ⊆ 𝑠)
21	19, 20	sylan 579	. . . . . . . . . . . . . . . 16 ⊢ ((((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) ∧ 𝐴 ⊆ 𝑠) → 𝑦 ⊆ 𝑠)
22	18, 21	mtand 812	. . . . . . . . . . . . . . 15 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ¬ 𝐴 ⊆ 𝑠)
23		simpl3 1191	. . . . . . . . . . . . . . . 16 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ∪ 𝑦 = 𝐴)
24	23	sseq1d 3948	. . . . . . . . . . . . . . 15 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → (∪ 𝑦 ⊆ 𝑠 ↔ 𝐴 ⊆ 𝑠))
25	22, 24	mtbird 324	. . . . . . . . . . . . . 14 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ¬ ∪ 𝑦 ⊆ 𝑠)
26		unissb 4870	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑦 ⊆ 𝑠 ↔ ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠)
27	25, 26	sylnib 327	. . . . . . . . . . . . 13 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ¬ ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠)
28	27	nrexdv 3197	. . . . . . . . . . . 12 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → ¬ ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠)
29		ssel 3910	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ On → (𝑠 ∈ 𝑦 → 𝑠 ∈ On))
30		ssel 3910	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ On → (𝑡 ∈ 𝑦 → 𝑡 ∈ On))
31		ontri1 6285	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ On ∧ 𝑠 ∈ On) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑠 ∈ 𝑡))
32	31	ancoms 458	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ∈ On ∧ 𝑡 ∈ On) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑠 ∈ 𝑡))
33		vex 3426	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑡 ∈ V
34		vex 3426	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑠 ∈ V
35	33, 34	brcnv 5780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡◡ E 𝑠 ↔ 𝑠 E 𝑡)
36		epel 5489	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 E 𝑡 ↔ 𝑠 ∈ 𝑡)
37	35, 36	bitri 274	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡◡ E 𝑠 ↔ 𝑠 ∈ 𝑡)
38	37	notbii 319	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑡◡ E 𝑠 ↔ ¬ 𝑠 ∈ 𝑡)
39	32, 38	bitr4di 288	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑠 ∈ On ∧ 𝑡 ∈ On) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑡◡ E 𝑠))
40	39	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ On → ((𝑠 ∈ On ∧ 𝑡 ∈ On) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑡◡ E 𝑠)))
41	29, 30, 40	syl2and 607	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ⊆ On → ((𝑠 ∈ 𝑦 ∧ 𝑡 ∈ 𝑦) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑡◡ E 𝑠)))
42	41	impl 455	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) ∧ 𝑡 ∈ 𝑦) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑡◡ E 𝑠))
43	42	ralbidva 3119	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → (∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠 ↔ ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E 𝑠))
44	43	rexbidva 3224	. . . . . . . . . . . . 13 ⊢ (𝑦 ⊆ On → (∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠 ↔ ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E 𝑠))
45	9, 44	syl 17	. . . . . . . . . . . 12 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → (∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠 ↔ ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E 𝑠))
46	28, 45	mtbid 323	. . . . . . . . . . 11 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → ¬ ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E 𝑠)
47		vex 3426	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
48	47	a1i 11	. . . . . . . . . . . 12 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦 ∈ V)
49		epweon 7603	. . . . . . . . . . . . . . . . . 18 ⊢ E We On
50		wess 5567	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ⊆ On → ( E We On → E We 𝑦))
51	49, 50	mpi 20	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ On → E We 𝑦)
52		weso 5571	. . . . . . . . . . . . . . . . 17 ⊢ ( E We 𝑦 → E Or 𝑦)
53	51, 52	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ⊆ On → E Or 𝑦)
54		cnvso 6180	. . . . . . . . . . . . . . . 16 ⊢ ( E Or 𝑦 ↔ ◡ E Or 𝑦)
55	53, 54	sylib 217	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ⊆ On → ◡ E Or 𝑦)
56		onssnum 9727	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ V ∧ 𝑦 ⊆ On) → 𝑦 ∈ dom card)
57	47, 56	mpan 686	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ⊆ On → 𝑦 ∈ dom card)
58		cardid2 9642	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ dom card → (card‘𝑦) ≈ 𝑦)
59		ensym 8744	. . . . . . . . . . . . . . . . . 18 ⊢ ((card‘𝑦) ≈ 𝑦 → 𝑦 ≈ (card‘𝑦))
60	57, 58, 59	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ On → 𝑦 ≈ (card‘𝑦))
61		nnsdom 9342	. . . . . . . . . . . . . . . . 17 ⊢ ((card‘𝑦) ∈ ω → (card‘𝑦) ≺ ω)
62		ensdomtr 8849	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ≈ (card‘𝑦) ∧ (card‘𝑦) ≺ ω) → 𝑦 ≺ ω)
63	60, 61, 62	syl2an 595	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ⊆ On ∧ (card‘𝑦) ∈ ω) → 𝑦 ≺ ω)
64		isfinite 9340	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ Fin ↔ 𝑦 ≺ ω)
65	63, 64	sylibr 233	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ⊆ On ∧ (card‘𝑦) ∈ ω) → 𝑦 ∈ Fin)
66		wofi 8993	. . . . . . . . . . . . . . 15 ⊢ ((◡ E Or 𝑦 ∧ 𝑦 ∈ Fin) → ◡ E We 𝑦)
67	55, 65, 66	syl2an2r 681	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ⊆ On ∧ (card‘𝑦) ∈ ω) → ◡ E We 𝑦)
68	9, 67	sylan 579	. . . . . . . . . . . . 13 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → ◡ E We 𝑦)
69		wefr 5570	. . . . . . . . . . . . 13 ⊢ (◡ E We 𝑦 → ◡ E Fr 𝑦)
70	68, 69	syl 17	. . . . . . . . . . . 12 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → ◡ E Fr 𝑦)
71		ssidd 3940	. . . . . . . . . . . 12 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦 ⊆ 𝑦)
72		unieq 4847	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ∅ → ∪ 𝑦 = ∪ ∅)
73		uni0 4866	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ ∅ = ∅
74	72, 73	eqtrdi 2795	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ∅ → ∪ 𝑦 = ∅)
75		eqeq1 2742	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑦 = 𝐴 → (∪ 𝑦 = ∅ ↔ 𝐴 = ∅))
76	74, 75	syl5ib 243	. . . . . . . . . . . . . . . . 17 ⊢ (∪ 𝑦 = 𝐴 → (𝑦 = ∅ → 𝐴 = ∅))
77		nlim0 6309	. . . . . . . . . . . . . . . . . 18 ⊢ ¬ Lim ∅
78		limeq 6263	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 = ∅ → (Lim 𝐴 ↔ Lim ∅))
79	77, 78	mtbiri 326	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 = ∅ → ¬ Lim 𝐴)
80	76, 79	syl6 35	. . . . . . . . . . . . . . . 16 ⊢ (∪ 𝑦 = 𝐴 → (𝑦 = ∅ → ¬ Lim 𝐴))
81	80	necon2ad 2957	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑦 = 𝐴 → (Lim 𝐴 → 𝑦 ≠ ∅))
82	81	impcom 407	. . . . . . . . . . . . . 14 ⊢ ((Lim 𝐴 ∧ ∪ 𝑦 = 𝐴) → 𝑦 ≠ ∅)
83	82	3adant2 1129	. . . . . . . . . . . . 13 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → 𝑦 ≠ ∅)
84	83	adantr 480	. . . . . . . . . . . 12 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦 ≠ ∅)
85		fri 5540	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ V ∧ ◡ E Fr 𝑦) ∧ (𝑦 ⊆ 𝑦 ∧ 𝑦 ≠ ∅)) → ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E 𝑠)
86	48, 70, 71, 84, 85	syl22anc 835	. . . . . . . . . . 11 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E 𝑠)
87	46, 86	mtand 812	. . . . . . . . . 10 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → ¬ (card‘𝑦) ∈ ω)
88		cardon 9633	. . . . . . . . . . 11 ⊢ (card‘𝑦) ∈ On
89		eloni 6261	. . . . . . . . . . 11 ⊢ ((card‘𝑦) ∈ On → Ord (card‘𝑦))
90		ordom 7697	. . . . . . . . . . . 12 ⊢ Ord ω
91		ordtri1 6284	. . . . . . . . . . . 12 ⊢ ((Ord ω ∧ Ord (card‘𝑦)) → (ω ⊆ (card‘𝑦) ↔ ¬ (card‘𝑦) ∈ ω))
92	90, 91	mpan 686	. . . . . . . . . . 11 ⊢ (Ord (card‘𝑦) → (ω ⊆ (card‘𝑦) ↔ ¬ (card‘𝑦) ∈ ω))
93	88, 89, 92	mp2b 10	. . . . . . . . . 10 ⊢ (ω ⊆ (card‘𝑦) ↔ ¬ (card‘𝑦) ∈ ω)
94	87, 93	sylibr 233	. . . . . . . . 9 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → ω ⊆ (card‘𝑦))
95	2, 94	syl3an2b 1402	. . . . . . . 8 ⊢ ((Lim 𝐴 ∧ 𝑦 ∈ 𝒫 𝐴 ∧ ∪ 𝑦 = 𝐴) → ω ⊆ (card‘𝑦))
96	95	3expb 1118	. . . . . . 7 ⊢ ((Lim 𝐴 ∧ (𝑦 ∈ 𝒫 𝐴 ∧ ∪ 𝑦 = 𝐴)) → ω ⊆ (card‘𝑦))
97	1, 96	sylan2b 593	. . . . . 6 ⊢ ((Lim 𝐴 ∧ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}) → ω ⊆ (card‘𝑦))
98	97	ralrimiva 3107	. . . . 5 ⊢ (Lim 𝐴 → ∀𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}ω ⊆ (card‘𝑦))
99		ssiin 4981	. . . . 5 ⊢ (ω ⊆ ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} (card‘𝑦) ↔ ∀𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}ω ⊆ (card‘𝑦))
100	98, 99	sylibr 233	. . . 4 ⊢ (Lim 𝐴 → ω ⊆ ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} (card‘𝑦))
101		cflim2.1	. . . . 5 ⊢ 𝐴 ∈ V
102	101	cflim3 9949	. . . 4 ⊢ (Lim 𝐴 → (cf‘𝐴) = ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} (card‘𝑦))
103	100, 102	sseqtrrd 3958	. . 3 ⊢ (Lim 𝐴 → ω ⊆ (cf‘𝐴))
104		fvex 6769	. . . . . . 7 ⊢ (card‘𝑦) ∈ V
105	104	dfiin2 4960	. . . . . 6 ⊢ ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} (card‘𝑦) = ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)}
106	102, 105	eqtrdi 2795	. . . . 5 ⊢ (Lim 𝐴 → (cf‘𝐴) = ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)})
107		cardlim 9661	. . . . . . . . 9 ⊢ (ω ⊆ (card‘𝑦) ↔ Lim (card‘𝑦))
108		sseq2 3943	. . . . . . . . . 10 ⊢ (𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ ω ⊆ (card‘𝑦)))
109		limeq 6263	. . . . . . . . . 10 ⊢ (𝑥 = (card‘𝑦) → (Lim 𝑥 ↔ Lim (card‘𝑦)))
110	108, 109	bibi12d 345	. . . . . . . . 9 ⊢ (𝑥 = (card‘𝑦) → ((ω ⊆ 𝑥 ↔ Lim 𝑥) ↔ (ω ⊆ (card‘𝑦) ↔ Lim (card‘𝑦))))
111	107, 110	mpbiri 257	. . . . . . . 8 ⊢ (𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ Lim 𝑥))
112	111	rexlimivw 3210	. . . . . . 7 ⊢ (∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ Lim 𝑥))
113	112	ss2abi 3996	. . . . . 6 ⊢ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)}
114		eleq1 2826	. . . . . . . . . 10 ⊢ (𝑥 = (card‘𝑦) → (𝑥 ∈ On ↔ (card‘𝑦) ∈ On))
115	88, 114	mpbiri 257	. . . . . . . . 9 ⊢ (𝑥 = (card‘𝑦) → 𝑥 ∈ On)
116	115	rexlimivw 3210	. . . . . . . 8 ⊢ (∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦) → 𝑥 ∈ On)
117	116	abssi 3999	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ On
118		fvex 6769	. . . . . . . . 9 ⊢ (cf‘𝐴) ∈ V
119	106, 118	eqeltrrdi 2848	. . . . . . . 8 ⊢ (Lim 𝐴 → ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ V)
120		intex 5256	. . . . . . . 8 ⊢ ({𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅ ↔ ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ V)
121	119, 120	sylibr 233	. . . . . . 7 ⊢ (Lim 𝐴 → {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅)
122		onint 7617	. . . . . . 7 ⊢ (({𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ On ∧ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅) → ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)})
123	117, 121, 122	sylancr 586	. . . . . 6 ⊢ (Lim 𝐴 → ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)})
124	113, 123	sselid 3915	. . . . 5 ⊢ (Lim 𝐴 → ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)})
125	106, 124	eqeltrd 2839	. . . 4 ⊢ (Lim 𝐴 → (cf‘𝐴) ∈ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)})
126		sseq2 3943	. . . . . 6 ⊢ (𝑥 = (cf‘𝐴) → (ω ⊆ 𝑥 ↔ ω ⊆ (cf‘𝐴)))
127		limeq 6263	. . . . . 6 ⊢ (𝑥 = (cf‘𝐴) → (Lim 𝑥 ↔ Lim (cf‘𝐴)))
128	126, 127	bibi12d 345	. . . . 5 ⊢ (𝑥 = (cf‘𝐴) → ((ω ⊆ 𝑥 ↔ Lim 𝑥) ↔ (ω ⊆ (cf‘𝐴) ↔ Lim (cf‘𝐴))))
129	118, 128	elab 3602	. . . 4 ⊢ ((cf‘𝐴) ∈ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)} ↔ (ω ⊆ (cf‘𝐴) ↔ Lim (cf‘𝐴)))
130	125, 129	sylib 217	. . 3 ⊢ (Lim 𝐴 → (ω ⊆ (cf‘𝐴) ↔ Lim (cf‘𝐴)))
131	103, 130	mpbid 231	. 2 ⊢ (Lim 𝐴 → Lim (cf‘𝐴))
132		eloni 6261	. . . . . . 7 ⊢ (𝐴 ∈ On → Ord 𝐴)
133		ordzsl 7667	. . . . . . 7 ⊢ (Ord 𝐴 ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴))
134	132, 133	sylib 217	. . . . . 6 ⊢ (𝐴 ∈ On → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴))
135		df-3or 1086	. . . . . . 7 ⊢ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴) ↔ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥) ∨ Lim 𝐴))
136		orcom 866	. . . . . . 7 ⊢ (((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥) ∨ Lim 𝐴) ↔ (Lim 𝐴 ∨ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)))
137		df-or 844	. . . . . . 7 ⊢ ((Lim 𝐴 ∨ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)) ↔ (¬ Lim 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)))
138	135, 136, 137	3bitri 296	. . . . . 6 ⊢ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴) ↔ (¬ Lim 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)))
139	134, 138	sylib 217	. . . . 5 ⊢ (𝐴 ∈ On → (¬ Lim 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)))
140		fveq2 6756	. . . . . . . . 9 ⊢ (𝐴 = ∅ → (cf‘𝐴) = (cf‘∅))
141		cf0 9938	. . . . . . . . 9 ⊢ (cf‘∅) = ∅
142	140, 141	eqtrdi 2795	. . . . . . . 8 ⊢ (𝐴 = ∅ → (cf‘𝐴) = ∅)
143		limeq 6263	. . . . . . . 8 ⊢ ((cf‘𝐴) = ∅ → (Lim (cf‘𝐴) ↔ Lim ∅))
144	142, 143	syl 17	. . . . . . 7 ⊢ (𝐴 = ∅ → (Lim (cf‘𝐴) ↔ Lim ∅))
145	77, 144	mtbiri 326	. . . . . 6 ⊢ (𝐴 = ∅ → ¬ Lim (cf‘𝐴))
146		1n0 8286	. . . . . . . . . 10 ⊢ 1o ≠ ∅
147		df1o2 8279	. . . . . . . . . . . 12 ⊢ 1o = {∅}
148	147	unieqi 4849	. . . . . . . . . . 11 ⊢ ∪ 1o = ∪ {∅}
149		0ex 5226	. . . . . . . . . . . 12 ⊢ ∅ ∈ V
150	149	unisn 4858	. . . . . . . . . . 11 ⊢ ∪ {∅} = ∅
151	148, 150	eqtri 2766	. . . . . . . . . 10 ⊢ ∪ 1o = ∅
152	146, 151	neeqtrri 3016	. . . . . . . . 9 ⊢ 1o ≠ ∪ 1o
153		limuni 6311	. . . . . . . . . 10 ⊢ (Lim 1o → 1o = ∪ 1o)
154	153	necon3ai 2967	. . . . . . . . 9 ⊢ (1o ≠ ∪ 1o → ¬ Lim 1o)
155	152, 154	ax-mp 5	. . . . . . . 8 ⊢ ¬ Lim 1o
156		fveq2 6756	. . . . . . . . . 10 ⊢ (𝐴 = suc 𝑥 → (cf‘𝐴) = (cf‘suc 𝑥))
157		cfsuc 9944	. . . . . . . . . 10 ⊢ (𝑥 ∈ On → (cf‘suc 𝑥) = 1o)
158	156, 157	sylan9eqr 2801	. . . . . . . . 9 ⊢ ((𝑥 ∈ On ∧ 𝐴 = suc 𝑥) → (cf‘𝐴) = 1o)
159		limeq 6263	. . . . . . . . 9 ⊢ ((cf‘𝐴) = 1o → (Lim (cf‘𝐴) ↔ Lim 1o))
160	158, 159	syl 17	. . . . . . . 8 ⊢ ((𝑥 ∈ On ∧ 𝐴 = suc 𝑥) → (Lim (cf‘𝐴) ↔ Lim 1o))
161	155, 160	mtbiri 326	. . . . . . 7 ⊢ ((𝑥 ∈ On ∧ 𝐴 = suc 𝑥) → ¬ Lim (cf‘𝐴))
162	161	rexlimiva 3209	. . . . . 6 ⊢ (∃𝑥 ∈ On 𝐴 = suc 𝑥 → ¬ Lim (cf‘𝐴))
163	145, 162	jaoi 853	. . . . 5 ⊢ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥) → ¬ Lim (cf‘𝐴))
164	139, 163	syl6 35	. . . 4 ⊢ (𝐴 ∈ On → (¬ Lim 𝐴 → ¬ Lim (cf‘𝐴)))
165	164	con4d 115	. . 3 ⊢ (𝐴 ∈ On → (Lim (cf‘𝐴) → Lim 𝐴))
166		cff 9935	. . . . . . . . 9 ⊢ cf:On⟶On
167	166	fdmi 6596	. . . . . . . 8 ⊢ dom cf = On
168	167	eleq2i 2830	. . . . . . 7 ⊢ (𝐴 ∈ dom cf ↔ 𝐴 ∈ On)
169		ndmfv 6786	. . . . . . 7 ⊢ (¬ 𝐴 ∈ dom cf → (cf‘𝐴) = ∅)
170	168, 169	sylnbir 330	. . . . . 6 ⊢ (¬ 𝐴 ∈ On → (cf‘𝐴) = ∅)
171	170, 143	syl 17	. . . . 5 ⊢ (¬ 𝐴 ∈ On → (Lim (cf‘𝐴) ↔ Lim ∅))
172	77, 171	mtbiri 326	. . . 4 ⊢ (¬ 𝐴 ∈ On → ¬ Lim (cf‘𝐴))
173	172	pm2.21d 121	. . 3 ⊢ (¬ 𝐴 ∈ On → (Lim (cf‘𝐴) → Lim 𝐴))
174	165, 173	pm2.61i 182	. 2 ⊢ (Lim (cf‘𝐴) → Lim 𝐴)
175	131, 174	impbii 208	1 ⊢ (Lim 𝐴 ↔ Lim (cf‘𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 843   ∨ w3o 1084   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108  {cab 2715   ≠ wne 2942  ∀wral 3063  ∃wrex 3064  {crab 3067  Vcvv 3422   ⊆ wss 3883  ∅c0 4253  𝒫 cpw 4530  {csn 4558  ∪ cuni 4836  ∩ cint 4876  ∩ ciin 4922   class class class wbr 5070   E cep 5485   Or wor 5493   Fr wfr 5532   We wwe 5534  ^◡ccnv 5579  dom cdm 5580  Ord word 6250  Oncon0 6251  Lim wlim 6252  suc csuc 6253  ‘cfv 6418  ωcom 7687  1_oc1o 8260   ≈ cen 8688   ≺ csdm 8690  Fincfn 8691  cardccrd 9624  cfccf 9626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-inf2 9329

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-int 4877  df-iun 4923  df-iin 4924  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-se 5536  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-isom 6427  df-riota 7212  df-ov 7258  df-om 7688  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-1o 8267  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-fin 8695  df-card 9628  df-cf 9630

This theorem is referenced by:  cfom  9951