Theorem cflim2 10344

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 3432	. . . . . . 7 ⊢ (𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} ↔ (𝑦 ∈ 𝒫 𝐴 ∧ ∪ 𝑦 = 𝐴))
2		velpw 4561	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴)
3		limord 6424	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Lim 𝐴 → Ord 𝐴)
4		ordsson 7797	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Ord 𝐴 → 𝐴 ⊆ On)
5		sstr 3916	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ On) → 𝑦 ⊆ On)
6	5	expcom 419	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ⊆ On → (𝑦 ⊆ 𝐴 → 𝑦 ⊆ On))
7	3, 4, 6	3syl 19	. . . . . . . . . . . . . . . . . . 19 ⊢ (Lim 𝐴 → (𝑦 ⊆ 𝐴 → 𝑦 ⊆ On))
8	7	imp 412	. . . . . . . . . . . . . . . . . 18 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴) → 𝑦 ⊆ On)
9	8	3adant3 1150	. . . . . . . . . . . . . . . . 17 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → 𝑦 ⊆ On)
10		ssel2 3903	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → 𝑠 ∈ On)
11		eloni 6372	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ On → Ord 𝑠)
12		ordirr 6380	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord 𝑠 → ¬ 𝑠 ∈ 𝑠)
13	10, 11, 12	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → ¬ 𝑠 ∈ 𝑠)
14		ssel 3902	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ⊆ 𝑠 → (𝑠 ∈ 𝑦 → 𝑠 ∈ 𝑠))
15	14	com12 33	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ 𝑦 → (𝑦 ⊆ 𝑠 → 𝑠 ∈ 𝑠))
16	15	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → (𝑦 ⊆ 𝑠 → 𝑠 ∈ 𝑠))
17	13, 16	mtod 201	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → ¬ 𝑦 ⊆ 𝑠)
18	9, 17	sylan 592	. . . . . . . . . . . . . . . 16 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ¬ 𝑦 ⊆ 𝑠)
19		simpl2 1211	. . . . . . . . . . . . . . . . 17 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → 𝑦 ⊆ 𝐴)
20		sstr 3916	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑠) → 𝑦 ⊆ 𝑠)
21	19, 20	sylan 592	. . . . . . . . . . . . . . . 16 ⊢ ((((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) ∧ 𝐴 ⊆ 𝑠) → 𝑦 ⊆ 𝑠)
22	18, 21	mtand 828	. . . . . . . . . . . . . . 15 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ¬ 𝐴 ⊆ 𝑠)
23		simpl3 1212	. . . . . . . . . . . . . . . 16 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ∪ 𝑦 = 𝐴)
24	23	sseq1d 3939	. . . . . . . . . . . . . . 15 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → (∪ 𝑦 ⊆ 𝑠 ↔ 𝐴 ⊆ 𝑠))
25	22, 24	mtbird 328	. . . . . . . . . . . . . 14 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ¬ ∪ 𝑦 ⊆ 𝑠)
26		unissb 4900	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑦 ⊆ 𝑠 ↔ ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠)
27	25, 26	sylnib 331	. . . . . . . . . . . . 13 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ¬ ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠)
28	27	nrexdv 3157	. . . . . . . . . . . 12 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → ¬ ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠)
29		ssel 3902	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ On → (𝑠 ∈ 𝑦 → 𝑠 ∈ On))
30		ssel 3902	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ On → (𝑡 ∈ 𝑦 → 𝑡 ∈ On))
31		ontri1 6397	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ On ∧ 𝑠 ∈ On) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑠 ∈ 𝑡))
32	31	ancoms 464	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ∈ On ∧ 𝑡 ∈ On) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑠 ∈ 𝑡))
33		vex 3454	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑡 ∈ V
34		vex 3454	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑠 ∈ V
35	33, 34	brcnv 5859	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡◡ E 𝑠 ↔ 𝑠 E 𝑡)
36		epel 5553	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 E 𝑡 ↔ 𝑠 ∈ 𝑡)
37	35, 36	bitri 278	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡◡ E 𝑠 ↔ 𝑠 ∈ 𝑡)
38	37	notbii 323	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑡◡ E 𝑠 ↔ ¬ 𝑠 ∈ 𝑡)
39	32, 38	bitr4di 292	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑠 ∈ On ∧ 𝑡 ∈ On) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑡◡ E 𝑠))
40	39	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ On → ((𝑠 ∈ On ∧ 𝑡 ∈ On) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑡◡ E 𝑠)))
41	29, 30, 40	syl2and 620	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ⊆ On → ((𝑠 ∈ 𝑦 ∧ 𝑡 ∈ 𝑦) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑡◡ E 𝑠)))
42	41	impl 461	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) ∧ 𝑡 ∈ 𝑦) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑡◡ E 𝑠))
43	42	ralbidva 3183	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → (∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠 ↔ ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E 𝑠))
44	43	rexbidva 3184	. . . . . . . . . . . . 13 ⊢ (𝑦 ⊆ On → (∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠 ↔ ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E 𝑠))
45	9, 44	syl 18	. . . . . . . . . . . 12 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → (∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠 ↔ ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E 𝑠))
46	28, 45	mtbid 327	. . . . . . . . . . 11 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → ¬ ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E 𝑠)
47		vex 3454	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
48	47	a1i 11	. . . . . . . . . . . 12 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦 ∈ V)
49		epweon 7789	. . . . . . . . . . . . . . . . . 18 ⊢ E We On
50		wess 5636	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ⊆ On → ( E We On → E We 𝑦))
51	49, 50	mpi 21	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ On → E We 𝑦)
52		weso 5641	. . . . . . . . . . . . . . . . 17 ⊢ ( E We 𝑦 → E Or 𝑦)
53	51, 52	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ⊆ On → E Or 𝑦)
54		cnvso 6291	. . . . . . . . . . . . . . . 16 ⊢ ( E Or 𝑦 ↔ ◡ E Or 𝑦)
55	53, 54	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ⊆ On → ◡ E Or 𝑦)
56		onssnum 10122	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ V ∧ 𝑦 ⊆ On) → 𝑦 ∈ dom card)
57	47, 56	mpan 703	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ⊆ On → 𝑦 ∈ dom card)
58		cardid2 10037	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ dom card → (card‘𝑦) ≈ 𝑦)
59		ensym 9033	. . . . . . . . . . . . . . . . . 18 ⊢ ((card‘𝑦) ≈ 𝑦 → 𝑦 ≈ (card‘𝑦))
60	57, 58, 59	3syl 19	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ On → 𝑦 ≈ (card‘𝑦))
61		nnsdom 9658	. . . . . . . . . . . . . . . . 17 ⊢ ((card‘𝑦) ∈ ω → (card‘𝑦) ≺ ω)
62		ensdomtr 9135	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ≈ (card‘𝑦) ∧ (card‘𝑦) ≺ ω) → 𝑦 ≺ ω)
63	60, 61, 62	syl2an 608	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ⊆ On ∧ (card‘𝑦) ∈ ω) → 𝑦 ≺ ω)
64		isfinite 9656	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ Fin ↔ 𝑦 ≺ ω)
65	63, 64	sylibr 237	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ⊆ On ∧ (card‘𝑦) ∈ ω) → 𝑦 ∈ Fin)
66		wofi 9283	. . . . . . . . . . . . . . 15 ⊢ ((◡ E Or 𝑦 ∧ 𝑦 ∈ Fin) → ◡ E We 𝑦)
67	55, 65, 66	syl2an2r 698	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ⊆ On ∧ (card‘𝑦) ∈ ω) → ◡ E We 𝑦)
68	9, 67	sylan 592	. . . . . . . . . . . . 13 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → ◡ E We 𝑦)
69		wefr 5640	. . . . . . . . . . . . 13 ⊢ (◡ E We 𝑦 → ◡ E Fr 𝑦)
70	68, 69	syl 18	. . . . . . . . . . . 12 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → ◡ E Fr 𝑦)
71		ssidd 3931	. . . . . . . . . . . 12 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦 ⊆ 𝑦)
72		unieq 4877	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ∅ → ∪ 𝑦 = ∪ ∅)
73		uni0 4895	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ ∅ = ∅
74	72, 73	eqtrdi 2811	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ∅ → ∪ 𝑦 = ∅)
75		eqeq1 2764	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑦 = 𝐴 → (∪ 𝑦 = ∅ ↔ 𝐴 = ∅))
76	74, 75	imbitrid 247	. . . . . . . . . . . . . . . . 17 ⊢ (∪ 𝑦 = 𝐴 → (𝑦 = ∅ → 𝐴 = ∅))
77		nlim0 6423	. . . . . . . . . . . . . . . . . 18 ⊢ ¬ Lim ∅
78		limeq 6374	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 = ∅ → (Lim 𝐴 ↔ Lim ∅))
79	77, 78	mtbiri 330	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 = ∅ → ¬ Lim 𝐴)
80	76, 79	syl6 36	. . . . . . . . . . . . . . . 16 ⊢ (∪ 𝑦 = 𝐴 → (𝑦 = ∅ → ¬ Lim 𝐴))
81	80	necon2ad 2970	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑦 = 𝐴 → (Lim 𝐴 → 𝑦 ≠ ∅))
82	81	impcom 413	. . . . . . . . . . . . . 14 ⊢ ((Lim 𝐴 ∧ ∪ 𝑦 = 𝐴) → 𝑦 ≠ ∅)
83	82	3adant2 1149	. . . . . . . . . . . . 13 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → 𝑦 ≠ ∅)
84	83	adantr 486	. . . . . . . . . . . 12 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦 ≠ ∅)
85		fri 5608	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ V ∧ ◡ E Fr 𝑦) ∧ (𝑦 ⊆ 𝑦 ∧ 𝑦 ≠ ∅)) → ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E 𝑠)
86	48, 70, 71, 84, 85	syl22anc 852	. . . . . . . . . . 11 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E 𝑠)
87	46, 86	mtand 828	. . . . . . . . . 10 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → ¬ (card‘𝑦) ∈ ω)
88		cardon 10028	. . . . . . . . . . 11 ⊢ (card‘𝑦) ∈ On
89		eloni 6372	. . . . . . . . . . 11 ⊢ ((card‘𝑦) ∈ On → Ord (card‘𝑦))
90		ordom 7887	. . . . . . . . . . . 12 ⊢ Ord ω
91		ordtri1 6396	. . . . . . . . . . . 12 ⊢ ((Ord ω ∧ Ord (card‘𝑦)) → (ω ⊆ (card‘𝑦) ↔ ¬ (card‘𝑦) ∈ ω))
92	90, 91	mpan 703	. . . . . . . . . . 11 ⊢ (Ord (card‘𝑦) → (ω ⊆ (card‘𝑦) ↔ ¬ (card‘𝑦) ∈ ω))
93	88, 89, 92	mp2b 10	. . . . . . . . . 10 ⊢ (ω ⊆ (card‘𝑦) ↔ ¬ (card‘𝑦) ∈ ω)
94	87, 93	sylibr 237	. . . . . . . . 9 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → ω ⊆ (card‘𝑦))
95	2, 94	syl3an2b 1431	. . . . . . . 8 ⊢ ((Lim 𝐴 ∧ 𝑦 ∈ 𝒫 𝐴 ∧ ∪ 𝑦 = 𝐴) → ω ⊆ (card‘𝑦))
96	95	3expb 1138	. . . . . . 7 ⊢ ((Lim 𝐴 ∧ (𝑦 ∈ 𝒫 𝐴 ∧ ∪ 𝑦 = 𝐴)) → ω ⊆ (card‘𝑦))
97	1, 96	sylan2b 606	. . . . . 6 ⊢ ((Lim 𝐴 ∧ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}) → ω ⊆ (card‘𝑦))
98	97	ralrimiva 3154	. . . . 5 ⊢ (Lim 𝐴 → ∀𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}ω ⊆ (card‘𝑦))
99		ssiin 5013	. . . . 5 ⊢ (ω ⊆ ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} (card‘𝑦) ↔ ∀𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}ω ⊆ (card‘𝑦))
100	98, 99	sylibr 237	. . . 4 ⊢ (Lim 𝐴 → ω ⊆ ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} (card‘𝑦))
101		cflim2.1	. . . . 5 ⊢ 𝐴 ∈ V
102	101	cflim3 10343	. . . 4 ⊢ (Lim 𝐴 → (cf‘𝐴) = ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} (card‘𝑦))
103	100, 102	sseqtrrd 3945	. . 3 ⊢ (Lim 𝐴 → ω ⊆ (cf‘𝐴))
104		fvex 6898	. . . . . . 7 ⊢ (card‘𝑦) ∈ V
105	104	dfiin2 4990	. . . . . 6 ⊢ ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} (card‘𝑦) = ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)}
106	102, 105	eqtrdi 2811	. . . . 5 ⊢ (Lim 𝐴 → (cf‘𝐴) = ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)})
107		cardlim 10056	. . . . . . . . 9 ⊢ (ω ⊆ (card‘𝑦) ↔ Lim (card‘𝑦))
108		sseq2 3934	. . . . . . . . . 10 ⊢ (𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ ω ⊆ (card‘𝑦)))
109		limeq 6374	. . . . . . . . . 10 ⊢ (𝑥 = (card‘𝑦) → (Lim 𝑥 ↔ Lim (card‘𝑦)))
110	108, 109	bibi12d 348	. . . . . . . . 9 ⊢ (𝑥 = (card‘𝑦) → ((ω ⊆ 𝑥 ↔ Lim 𝑥) ↔ (ω ⊆ (card‘𝑦) ↔ Lim (card‘𝑦))))
111	107, 110	mpbiri 261	. . . . . . . 8 ⊢ (𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ Lim 𝑥))
112	111	rexlimivw 3159	. . . . . . 7 ⊢ (∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ Lim 𝑥))
113	112	ss2abi 3991	. . . . . 6 ⊢ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)}
114		eleq1 2848	. . . . . . . . . 10 ⊢ (𝑥 = (card‘𝑦) → (𝑥 ∈ On ↔ (card‘𝑦) ∈ On))
115	88, 114	mpbiri 261	. . . . . . . . 9 ⊢ (𝑥 = (card‘𝑦) → 𝑥 ∈ On)
116	115	rexlimivw 3159	. . . . . . . 8 ⊢ (∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦) → 𝑥 ∈ On)
117	116	abssi 3993	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ On
118		fvex 6898	. . . . . . . . 9 ⊢ (cf‘𝐴) ∈ V
119	106, 118	eqeltrrdi 2869	. . . . . . . 8 ⊢ (Lim 𝐴 → ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ V)
120		intex 5304	. . . . . . . 8 ⊢ ({𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅ ↔ ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ V)
121	119, 120	sylibr 237	. . . . . . 7 ⊢ (Lim 𝐴 → {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅)
122		onint 7804	. . . . . . 7 ⊢ (({𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ On ∧ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅) → ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)})
123	117, 121, 122	sylancr 599	. . . . . 6 ⊢ (Lim 𝐴 → ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)})
124	113, 123	sselid 3906	. . . . 5 ⊢ (Lim 𝐴 → ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)})
125	106, 124	eqeltrd 2860	. . . 4 ⊢ (Lim 𝐴 → (cf‘𝐴) ∈ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)})
126		sseq2 3934	. . . . . 6 ⊢ (𝑥 = (cf‘𝐴) → (ω ⊆ 𝑥 ↔ ω ⊆ (cf‘𝐴)))
127		limeq 6374	. . . . . 6 ⊢ (𝑥 = (cf‘𝐴) → (Lim 𝑥 ↔ Lim (cf‘𝐴)))
128	126, 127	bibi12d 348	. . . . 5 ⊢ (𝑥 = (cf‘𝐴) → ((ω ⊆ 𝑥 ↔ Lim 𝑥) ↔ (ω ⊆ (cf‘𝐴) ↔ Lim (cf‘𝐴))))
129	118, 128	elab 3632	. . . 4 ⊢ ((cf‘𝐴) ∈ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)} ↔ (ω ⊆ (cf‘𝐴) ↔ Lim (cf‘𝐴)))
130	125, 129	sylib 221	. . 3 ⊢ (Lim 𝐴 → (ω ⊆ (cf‘𝐴) ↔ Lim (cf‘𝐴)))
131	103, 130	mpbid 235	. 2 ⊢ (Lim 𝐴 → Lim (cf‘𝐴))
132		eloni 6372	. . . . . . 7 ⊢ (𝐴 ∈ On → Ord 𝐴)
133		ordzsl 7856	. . . . . . 7 ⊢ (Ord 𝐴 ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴))
134	132, 133	sylib 221	. . . . . 6 ⊢ (𝐴 ∈ On → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴))
135		df-3or 1104	. . . . . . 7 ⊢ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴) ↔ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥) ∨ Lim 𝐴))
136		orcom 884	. . . . . . 7 ⊢ (((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥) ∨ Lim 𝐴) ↔ (Lim 𝐴 ∨ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)))
137		df-or 862	. . . . . . 7 ⊢ ((Lim 𝐴 ∨ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)) ↔ (¬ Lim 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)))
138	135, 136, 137	3bitri 300	. . . . . 6 ⊢ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴) ↔ (¬ Lim 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)))
139	134, 138	sylib 221	. . . . 5 ⊢ (𝐴 ∈ On → (¬ Lim 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)))
140		fveq2 6885	. . . . . . . . 9 ⊢ (𝐴 = ∅ → (cf‘𝐴) = (cf‘∅))
141		cf0 10331	. . . . . . . . 9 ⊢ (cf‘∅) = ∅
142	140, 141	eqtrdi 2811	. . . . . . . 8 ⊢ (𝐴 = ∅ → (cf‘𝐴) = ∅)
143		limeq 6374	. . . . . . . 8 ⊢ ((cf‘𝐴) = ∅ → (Lim (cf‘𝐴) ↔ Lim ∅))
144	142, 143	syl 18	. . . . . . 7 ⊢ (𝐴 = ∅ → (Lim (cf‘𝐴) ↔ Lim ∅))
145	77, 144	mtbiri 330	. . . . . 6 ⊢ (𝐴 = ∅ → ¬ Lim (cf‘𝐴))
146		nlim1 8500	. . . . . . . 8 ⊢ ¬ Lim 1o
147		fveq2 6885	. . . . . . . . . 10 ⊢ (𝐴 = suc 𝑥 → (cf‘𝐴) = (cf‘suc 𝑥))
148		cfsuc 10338	. . . . . . . . . 10 ⊢ (𝑥 ∈ On → (cf‘suc 𝑥) = 1o)
149	147, 148	sylan9eqr 2817	. . . . . . . . 9 ⊢ ((𝑥 ∈ On ∧ 𝐴 = suc 𝑥) → (cf‘𝐴) = 1o)
150		limeq 6374	. . . . . . . . 9 ⊢ ((cf‘𝐴) = 1o → (Lim (cf‘𝐴) ↔ Lim 1o))
151	149, 150	syl 18	. . . . . . . 8 ⊢ ((𝑥 ∈ On ∧ 𝐴 = suc 𝑥) → (Lim (cf‘𝐴) ↔ Lim 1o))
152	146, 151	mtbiri 330	. . . . . . 7 ⊢ ((𝑥 ∈ On ∧ 𝐴 = suc 𝑥) → ¬ Lim (cf‘𝐴))
153	152	rexlimiva 3155	. . . . . 6 ⊢ (∃𝑥 ∈ On 𝐴 = suc 𝑥 → ¬ Lim (cf‘𝐴))
154	145, 153	jaoi 871	. . . . 5 ⊢ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥) → ¬ Lim (cf‘𝐴))
155	139, 154	syl6 36	. . . 4 ⊢ (𝐴 ∈ On → (¬ Lim 𝐴 → ¬ Lim (cf‘𝐴)))
156	155	con4d 116	. . 3 ⊢ (𝐴 ∈ On → (Lim (cf‘𝐴) → Lim 𝐴))
157		cff 10328	. . . . . . . . 9 ⊢ cf:On⟶On
158	157	fdmi 6721	. . . . . . . 8 ⊢ dom cf = On
159	158	eleq2i 2852	. . . . . . 7 ⊢ (𝐴 ∈ dom cf ↔ 𝐴 ∈ On)
160		ndmfv 6917	. . . . . . 7 ⊢ (¬ 𝐴 ∈ dom cf → (cf‘𝐴) = ∅)
161	159, 160	sylnbir 334	. . . . . 6 ⊢ (¬ 𝐴 ∈ On → (cf‘𝐴) = ∅)
162	161, 143	syl 18	. . . . 5 ⊢ (¬ 𝐴 ∈ On → (Lim (cf‘𝐴) ↔ Lim ∅))
163	77, 162	mtbiri 330	. . . 4 ⊢ (¬ 𝐴 ∈ On → ¬ Lim (cf‘𝐴))
164	163	pm2.21d 122	. . 3 ⊢ (¬ 𝐴 ∈ On → (Lim (cf‘𝐴) → Lim 𝐴))
165	156, 164	pm2.61i 184	. 2 ⊢ (Lim (cf‘𝐴) → Lim 𝐴)
166	131, 165	impbii 212	1 ⊢ (Lim 𝐴 ↔ Lim (cf‘𝐴))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∨ w3o 1102   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144  {cab 2738   ≠ wne 2955  ∀wral 3076  ∃wrex 3086  {crab 3412  Vcvv 3450   ⊆ wss 3895  ∅c0 4278  𝒫 cpw 4556  ∪ cuni 4866  ∩ cint 4906  ∩ ciin 4951   class class class wbr 5102   E cep 5549   Or wor 5557   Fr wfr 5600   We wwe 5602  ^◡ccnv 5649  dom cdm 5650  Ord word 6361  Oncon0 6362  Lim wlim 6363  suc csuc 6364  ‘cfv 6538  ωcom 7877  1_oc1o 8472   ≈ cen 8973   ≺ csdm 8975  Fincfn 8976  cardccrd 10019  cfccf 10021

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-inf2 9645

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-int 4907  df-iun 4952  df-iin 4953  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-se 5604  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-isom 6547  df-riota 7377  df-ov 7423  df-om 7878  df-2nd 8002  df-frecs 8302  df-wrecs 8333  df-recs 8382  df-rdg 8421  df-1o 8479  df-er 8720  df-en 8977  df-dom 8978  df-sdom 8979  df-fin 8980  df-card 10023  df-cf 10025

This theorem is used by:  cfom  10345