Theorem cflim2 10265

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 3440	. . . . . . 7 ⊢ (𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} ↔ (𝑦 ∈ 𝒫 𝐴 ∧ ∪ 𝑦 = 𝐴))
2		velpw 4572	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴)
3		limord 6429	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Lim 𝐴 → Ord 𝐴)
4		ordsson 7791	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Ord 𝐴 → 𝐴 ⊆ On)
5		sstr 3948	. . . . . . . . . . . . . . . . . . . . 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 3935	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → 𝑠 ∈ On)
11		eloni 6377	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ On → Ord 𝑠)
12		ordirr 6385	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord 𝑠 → ¬ 𝑠 ∈ 𝑠)
13	10, 11, 12	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → ¬ 𝑠 ∈ 𝑠)
14		ssel 3934	. . . . . . . . . . . . . . . . . . . 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 3948	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑠) → 𝑦 ⊆ 𝑠)
21	19, 20	sylan 592	. . . . . . . . . . . . . . . 16 ⊢ ((((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) ∧ 𝐴 ⊆ 𝑠) → 𝑦 ⊆ 𝑠)
22	18, 21	mtand 828	. . . . . . . . . . . . . . 15 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ¬ 𝐴 ⊆ 𝑠)
23		simpl3 1212	. . . . . . . . . . . . . . . 16 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ∪ 𝑦 = 𝐴)
24	23	sseq1d 3971	. . . . . . . . . . . . . . 15 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → (∪ 𝑦 ⊆ 𝑠 ↔ 𝐴 ⊆ 𝑠))
25	22, 24	mtbird 328	. . . . . . . . . . . . . 14 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ¬ ∪ 𝑦 ⊆ 𝑠)
26		unissb 4911	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑦 ⊆ 𝑠 ↔ ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠)
27	25, 26	sylnib 331	. . . . . . . . . . . . 13 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ¬ ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠)
28	27	nrexdv 3163	. . . . . . . . . . . 12 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → ¬ ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠)
29		ssel 3934	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ On → (𝑠 ∈ 𝑦 → 𝑠 ∈ On))
30		ssel 3934	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ On → (𝑡 ∈ 𝑦 → 𝑡 ∈ On))
31		ontri1 6402	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ On ∧ 𝑠 ∈ On) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑠 ∈ 𝑡))
32	31	ancoms 464	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ∈ On ∧ 𝑡 ∈ On) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑠 ∈ 𝑡))
33		vex 3462	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑡 ∈ V
34		vex 3462	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑠 ∈ V
35	33, 34	brcnv 5873	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡◡ E 𝑠 ↔ 𝑠 E 𝑡)
36		epel 5569	. . . . . . . . . . . . . . . . . . . . 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 3189	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → (∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠 ↔ ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E 𝑠))
44	43	rexbidva 3190	. . . . . . . . . . . . 13 ⊢ (𝑦 ⊆ On → (∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠 ↔ ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E 𝑠))
45	9, 44	syl 18	. . . . . . . . . . . 12 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → (∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠 ↔ ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E 𝑠))
46	28, 45	mtbid 327	. . . . . . . . . . 11 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → ¬ ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E 𝑠)
47		vex 3462	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
48	47	a1i 11	. . . . . . . . . . . 12 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦 ∈ V)
49		epweon 7783	. . . . . . . . . . . . . . . . . 18 ⊢ E We On
50		wess 5652	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ⊆ On → ( E We On → E We 𝑦))
51	49, 50	mpi 21	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ On → E We 𝑦)
52		weso 5657	. . . . . . . . . . . . . . . . 17 ⊢ ( E We 𝑦 → E Or 𝑦)
53	51, 52	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ⊆ On → E Or 𝑦)
54		cnvso 6296	. . . . . . . . . . . . . . . 16 ⊢ ( E Or 𝑦 ↔ ◡ E Or 𝑦)
55	53, 54	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ⊆ On → ◡ E Or 𝑦)
56		onssnum 10043	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ V ∧ 𝑦 ⊆ On) → 𝑦 ∈ dom card)
57	47, 56	mpan 703	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ⊆ On → 𝑦 ∈ dom card)
58		cardid2 9958	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ dom card → (card‘𝑦) ≈ 𝑦)
59		ensym 9009	. . . . . . . . . . . . . . . . . 18 ⊢ ((card‘𝑦) ≈ 𝑦 → 𝑦 ≈ (card‘𝑦))
60	57, 58, 59	3syl 19	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ On → 𝑦 ≈ (card‘𝑦))
61		nnsdom 9633	. . . . . . . . . . . . . . . . 17 ⊢ ((card‘𝑦) ∈ ω → (card‘𝑦) ≺ ω)
62		ensdomtr 9111	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ≈ (card‘𝑦) ∧ (card‘𝑦) ≺ ω) → 𝑦 ≺ ω)
63	60, 61, 62	syl2an 608	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ⊆ On ∧ (card‘𝑦) ∈ ω) → 𝑦 ≺ ω)
64		isfinite 9631	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ Fin ↔ 𝑦 ≺ ω)
65	63, 64	sylibr 237	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ⊆ On ∧ (card‘𝑦) ∈ ω) → 𝑦 ∈ Fin)
66		wofi 9259	. . . . . . . . . . . . . . 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 5656	. . . . . . . . . . . . 13 ⊢ (◡ E We 𝑦 → ◡ E Fr 𝑦)
70	68, 69	syl 18	. . . . . . . . . . . 12 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → ◡ E Fr 𝑦)
71		ssidd 3963	. . . . . . . . . . . 12 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦 ⊆ 𝑦)
72		unieq 4888	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ∅ → ∪ 𝑦 = ∪ ∅)
73		uni0 4906	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ ∅ = ∅
74	72, 73	eqtrdi 2817	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ∅ → ∪ 𝑦 = ∅)
75		eqeq1 2770	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑦 = 𝐴 → (∪ 𝑦 = ∅ ↔ 𝐴 = ∅))
76	74, 75	imbitrid 247	. . . . . . . . . . . . . . . . 17 ⊢ (∪ 𝑦 = 𝐴 → (𝑦 = ∅ → 𝐴 = ∅))
77		nlim0 6428	. . . . . . . . . . . . . . . . . 18 ⊢ ¬ Lim ∅
78		limeq 6379	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 = ∅ → (Lim 𝐴 ↔ Lim ∅))
79	77, 78	mtbiri 330	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 = ∅ → ¬ Lim 𝐴)
80	76, 79	syl6 36	. . . . . . . . . . . . . . . 16 ⊢ (∪ 𝑦 = 𝐴 → (𝑦 = ∅ → ¬ Lim 𝐴))
81	80	necon2ad 2976	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑦 = 𝐴 → (Lim 𝐴 → 𝑦 ≠ ∅))
82	81	impcom 413	. . . . . . . . . . . . . 14 ⊢ ((Lim 𝐴 ∧ ∪ 𝑦 = 𝐴) → 𝑦 ≠ ∅)
83	82	3adant2 1149	. . . . . . . . . . . . 13 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → 𝑦 ≠ ∅)
84	83	adantr 486	. . . . . . . . . . . 12 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦 ≠ ∅)
85		fri 5624	. . . . . . . . . . . 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 9949	. . . . . . . . . . 11 ⊢ (card‘𝑦) ∈ On
89		eloni 6377	. . . . . . . . . . 11 ⊢ ((card‘𝑦) ∈ On → Ord (card‘𝑦))
90		ordom 7881	. . . . . . . . . . . 12 ⊢ Ord ω
91		ordtri1 6401	. . . . . . . . . . . 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 3160	. . . . 5 ⊢ (Lim 𝐴 → ∀𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}ω ⊆ (card‘𝑦))
99		ssiin 5025	. . . . 5 ⊢ (ω ⊆ ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} (card‘𝑦) ↔ ∀𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}ω ⊆ (card‘𝑦))
100	98, 99	sylibr 237	. . . 4 ⊢ (Lim 𝐴 → ω ⊆ ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} (card‘𝑦))
101		cflim2.1	. . . . 5 ⊢ 𝐴 ∈ V
102	101	cflim3 10264	. . . 4 ⊢ (Lim 𝐴 → (cf‘𝐴) = ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} (card‘𝑦))
103	100, 102	sseqtrrd 3977	. . 3 ⊢ (Lim 𝐴 → ω ⊆ (cf‘𝐴))
104		fvex 6901	. . . . . . 7 ⊢ (card‘𝑦) ∈ V
105	104	dfiin2 5002	. . . . . 6 ⊢ ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} (card‘𝑦) = ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)}
106	102, 105	eqtrdi 2817	. . . . 5 ⊢ (Lim 𝐴 → (cf‘𝐴) = ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)})
107		cardlim 9977	. . . . . . . . 9 ⊢ (ω ⊆ (card‘𝑦) ↔ Lim (card‘𝑦))
108		sseq2 3966	. . . . . . . . . 10 ⊢ (𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ ω ⊆ (card‘𝑦)))
109		limeq 6379	. . . . . . . . . 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 3165	. . . . . . 7 ⊢ (∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ Lim 𝑥))
113	112	ss2abi 4023	. . . . . 6 ⊢ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)}
114		eleq1 2854	. . . . . . . . . 10 ⊢ (𝑥 = (card‘𝑦) → (𝑥 ∈ On ↔ (card‘𝑦) ∈ On))
115	88, 114	mpbiri 261	. . . . . . . . 9 ⊢ (𝑥 = (card‘𝑦) → 𝑥 ∈ On)
116	115	rexlimivw 3165	. . . . . . . 8 ⊢ (∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦) → 𝑥 ∈ On)
117	116	abssi 4025	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ On
118		fvex 6901	. . . . . . . . 9 ⊢ (cf‘𝐴) ∈ V
119	106, 118	eqeltrrdi 2875	. . . . . . . 8 ⊢ (Lim 𝐴 → ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ V)
120		intex 5319	. . . . . . . 8 ⊢ ({𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅ ↔ ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ V)
121	119, 120	sylibr 237	. . . . . . 7 ⊢ (Lim 𝐴 → {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅)
122		onint 7798	. . . . . . 7 ⊢ (({𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ On ∧ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅) → ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)})
123	117, 121, 122	sylancr 599	. . . . . 6 ⊢ (Lim 𝐴 → ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)})
124	113, 123	sselid 3938	. . . . 5 ⊢ (Lim 𝐴 → ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)})
125	106, 124	eqeltrd 2866	. . . 4 ⊢ (Lim 𝐴 → (cf‘𝐴) ∈ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)})
126		sseq2 3966	. . . . . 6 ⊢ (𝑥 = (cf‘𝐴) → (ω ⊆ 𝑥 ↔ ω ⊆ (cf‘𝐴)))
127		limeq 6379	. . . . . 6 ⊢ (𝑥 = (cf‘𝐴) → (Lim 𝑥 ↔ Lim (cf‘𝐴)))
128	126, 127	bibi12d 348	. . . . 5 ⊢ (𝑥 = (cf‘𝐴) → ((ω ⊆ 𝑥 ↔ Lim 𝑥) ↔ (ω ⊆ (cf‘𝐴) ↔ Lim (cf‘𝐴))))
129	118, 128	elab 3641	. . . 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 6377	. . . . . . 7 ⊢ (𝐴 ∈ On → Ord 𝐴)
133		ordzsl 7850	. . . . . . 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 6888	. . . . . . . . 9 ⊢ (𝐴 = ∅ → (cf‘𝐴) = (cf‘∅))
141		cf0 10252	. . . . . . . . 9 ⊢ (cf‘∅) = ∅
142	140, 141	eqtrdi 2817	. . . . . . . 8 ⊢ (𝐴 = ∅ → (cf‘𝐴) = ∅)
143		limeq 6379	. . . . . . . 8 ⊢ ((cf‘𝐴) = ∅ → (Lim (cf‘𝐴) ↔ Lim ∅))
144	142, 143	syl 18	. . . . . . 7 ⊢ (𝐴 = ∅ → (Lim (cf‘𝐴) ↔ Lim ∅))
145	77, 144	mtbiri 330	. . . . . 6 ⊢ (𝐴 = ∅ → ¬ Lim (cf‘𝐴))
146		1n0 8481	. . . . . . . . . 10 ⊢ 1o ≠ ∅
147		df1o2 8469	. . . . . . . . . . . 12 ⊢ 1o = {∅}
148	147	unieqi 4889	. . . . . . . . . . 11 ⊢ ∪ 1o = ∪ {∅}
149		0ex 5275	. . . . . . . . . . . 12 ⊢ ∅ ∈ V
150	149	unisn 4896	. . . . . . . . . . 11 ⊢ ∪ {∅} = ∅
151	148, 150	eqtri 2789	. . . . . . . . . 10 ⊢ ∪ 1o = ∅
152	146, 151	neeqtrri 3034	. . . . . . . . 9 ⊢ 1o ≠ ∪ 1o
153		limuni 6430	. . . . . . . . . 10 ⊢ (Lim 1o → 1o = ∪ 1o)
154	153	necon3ai 2986	. . . . . . . . 9 ⊢ (1o ≠ ∪ 1o → ¬ Lim 1o)
155	152, 154	ax-mp 5	. . . . . . . 8 ⊢ ¬ Lim 1o
156		fveq2 6888	. . . . . . . . . 10 ⊢ (𝐴 = suc 𝑥 → (cf‘𝐴) = (cf‘suc 𝑥))
157		cfsuc 10259	. . . . . . . . . 10 ⊢ (𝑥 ∈ On → (cf‘suc 𝑥) = 1o)
158	156, 157	sylan9eqr 2823	. . . . . . . . 9 ⊢ ((𝑥 ∈ On ∧ 𝐴 = suc 𝑥) → (cf‘𝐴) = 1o)
159		limeq 6379	. . . . . . . . 9 ⊢ ((cf‘𝐴) = 1o → (Lim (cf‘𝐴) ↔ Lim 1o))
160	158, 159	syl 18	. . . . . . . 8 ⊢ ((𝑥 ∈ On ∧ 𝐴 = suc 𝑥) → (Lim (cf‘𝐴) ↔ Lim 1o))
161	155, 160	mtbiri 330	. . . . . . 7 ⊢ ((𝑥 ∈ On ∧ 𝐴 = suc 𝑥) → ¬ Lim (cf‘𝐴))
162	161	rexlimiva 3161	. . . . . 6 ⊢ (∃𝑥 ∈ On 𝐴 = suc 𝑥 → ¬ Lim (cf‘𝐴))
163	145, 162	jaoi 871	. . . . 5 ⊢ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥) → ¬ Lim (cf‘𝐴))
164	139, 163	syl6 36	. . . 4 ⊢ (𝐴 ∈ On → (¬ Lim 𝐴 → ¬ Lim (cf‘𝐴)))
165	164	con4d 116	. . 3 ⊢ (𝐴 ∈ On → (Lim (cf‘𝐴) → Lim 𝐴))
166		cff 10249	. . . . . . . . 9 ⊢ cf:On⟶On
167	166	fdmi 6724	. . . . . . . 8 ⊢ dom cf = On
168	167	eleq2i 2858	. . . . . . 7 ⊢ (𝐴 ∈ dom cf ↔ 𝐴 ∈ On)
169		ndmfv 6920	. . . . . . 7 ⊢ (¬ 𝐴 ∈ dom cf → (cf‘𝐴) = ∅)
170	168, 169	sylnbir 334	. . . . . 6 ⊢ (¬ 𝐴 ∈ On → (cf‘𝐴) = ∅)
171	170, 143	syl 18	. . . . 5 ⊢ (¬ 𝐴 ∈ On → (Lim (cf‘𝐴) ↔ Lim ∅))
172	77, 171	mtbiri 330	. . . 4 ⊢ (¬ 𝐴 ∈ On → ¬ Lim (cf‘𝐴))
173	172	pm2.21d 122	. . 3 ⊢ (¬ 𝐴 ∈ On → (Lim (cf‘𝐴) → Lim 𝐴))
174	165, 173	pm2.61i 184	. 2 ⊢ (Lim (cf‘𝐴) → Lim 𝐴)
175	131, 174	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 1570   ∈ wcel 2146  {cab 2744   ≠ wne 2961  ∀wral 3082  ∃wrex 3092  {crab 3419  Vcvv 3458   ⊆ wss 3908  ∅c0 4289  𝒫 cpw 4567  {csn 4594  ∪ cuni 4877  ∩ cint 4917  ∩ ciin 4962   class class class wbr 5114   E cep 5565   Or wor 5573   Fr wfr 5616   We wwe 5618  ^◡ccnv 5665  dom cdm 5666  Ord word 6366  Oncon0 6367  Lim wlim 6368  suc csuc 6369  ‘cfv 6543  ωcom 7871  1_oc1o 8455   ≈ cen 8949   ≺ csdm 8951  Fincfn 8952  cardccrd 9940  cfccf 9942

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-rep 5243  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-inf2 9620

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rmo 3372  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-int 4918  df-iun 4963  df-iin 4964  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-se 5620  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7380  df-ov 7426  df-om 7872  df-2nd 7996  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-rdg 8406  df-1o 8462  df-er 8703  df-en 8953  df-dom 8954  df-sdom 8955  df-fin 8956  df-card 9944  df-cf 9946

This theorem is used by:  cfom  10266