Theorem cflim2 10282

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 3442	. . . . . . 7 ⊢ (𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} ↔ (𝑦 ∈ 𝒫 𝐴 ∧ ∪ 𝑦 = 𝐴))
2		velpw 4585	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴)
3		limord 6418	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Lim 𝐴 → Ord 𝐴)
4		ordsson 7782	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Ord 𝐴 → 𝐴 ⊆ On)
5		sstr 3972	. . . . . . . . . . . . . . . . . . . . 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 1132	. . . . . . . . . . . . . . . . 17 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → 𝑦 ⊆ On)
10		ssel2 3958	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → 𝑠 ∈ On)
11		eloni 6367	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ On → Ord 𝑠)
12		ordirr 6375	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord 𝑠 → ¬ 𝑠 ∈ 𝑠)
13	10, 11, 12	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → ¬ 𝑠 ∈ 𝑠)
14		ssel 3957	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ⊆ 𝑠 → (𝑠 ∈ 𝑦 → 𝑠 ∈ 𝑠))
15	14	com12 32	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ 𝑦 → (𝑦 ⊆ 𝑠 → 𝑠 ∈ 𝑠))
16	15	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → (𝑦 ⊆ 𝑠 → 𝑠 ∈ 𝑠))
17	13, 16	mtod 198	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → ¬ 𝑦 ⊆ 𝑠)
18	9, 17	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ¬ 𝑦 ⊆ 𝑠)
19		simpl2 1193	. . . . . . . . . . . . . . . . 17 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → 𝑦 ⊆ 𝐴)
20		sstr 3972	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑠) → 𝑦 ⊆ 𝑠)
21	19, 20	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ ((((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) ∧ 𝐴 ⊆ 𝑠) → 𝑦 ⊆ 𝑠)
22	18, 21	mtand 815	. . . . . . . . . . . . . . 15 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ¬ 𝐴 ⊆ 𝑠)
23		simpl3 1194	. . . . . . . . . . . . . . . 16 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ∪ 𝑦 = 𝐴)
24	23	sseq1d 3995	. . . . . . . . . . . . . . 15 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → (∪ 𝑦 ⊆ 𝑠 ↔ 𝐴 ⊆ 𝑠))
25	22, 24	mtbird 325	. . . . . . . . . . . . . 14 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ¬ ∪ 𝑦 ⊆ 𝑠)
26		unissb 4920	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑦 ⊆ 𝑠 ↔ ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠)
27	25, 26	sylnib 328	. . . . . . . . . . . . 13 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ¬ ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠)
28	27	nrexdv 3136	. . . . . . . . . . . 12 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → ¬ ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠)
29		ssel 3957	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ On → (𝑠 ∈ 𝑦 → 𝑠 ∈ On))
30		ssel 3957	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ On → (𝑡 ∈ 𝑦 → 𝑡 ∈ On))
31		ontri1 6391	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ On ∧ 𝑠 ∈ On) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑠 ∈ 𝑡))
32	31	ancoms 458	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ∈ On ∧ 𝑡 ∈ On) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑠 ∈ 𝑡))
33		vex 3468	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑡 ∈ V
34		vex 3468	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑠 ∈ V
35	33, 34	brcnv 5867	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡◡ E 𝑠 ↔ 𝑠 E 𝑡)
36		epel 5561	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 E 𝑡 ↔ 𝑠 ∈ 𝑡)
37	35, 36	bitri 275	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡◡ E 𝑠 ↔ 𝑠 ∈ 𝑡)
38	37	notbii 320	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑡◡ E 𝑠 ↔ ¬ 𝑠 ∈ 𝑡)
39	32, 38	bitr4di 289	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑠 ∈ On ∧ 𝑡 ∈ On) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑡◡ E 𝑠))
40	39	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ On → ((𝑠 ∈ On ∧ 𝑡 ∈ On) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑡◡ E 𝑠)))
41	29, 30, 40	syl2and 608	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ⊆ On → ((𝑠 ∈ 𝑦 ∧ 𝑡 ∈ 𝑦) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑡◡ E 𝑠)))
42	41	impl 455	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) ∧ 𝑡 ∈ 𝑦) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑡◡ E 𝑠))
43	42	ralbidva 3162	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → (∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠 ↔ ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E 𝑠))
44	43	rexbidva 3163	. . . . . . . . . . . . 13 ⊢ (𝑦 ⊆ On → (∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠 ↔ ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E 𝑠))
45	9, 44	syl 17	. . . . . . . . . . . 12 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → (∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠 ↔ ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E 𝑠))
46	28, 45	mtbid 324	. . . . . . . . . . 11 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → ¬ ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E 𝑠)
47		vex 3468	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
48	47	a1i 11	. . . . . . . . . . . 12 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦 ∈ V)
49		epweon 7774	. . . . . . . . . . . . . . . . . 18 ⊢ E We On
50		wess 5645	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ⊆ On → ( E We On → E We 𝑦))
51	49, 50	mpi 20	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ On → E We 𝑦)
52		weso 5650	. . . . . . . . . . . . . . . . 17 ⊢ ( E We 𝑦 → E Or 𝑦)
53	51, 52	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ⊆ On → E Or 𝑦)
54		cnvso 6282	. . . . . . . . . . . . . . . 16 ⊢ ( E Or 𝑦 ↔ ◡ E Or 𝑦)
55	53, 54	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ⊆ On → ◡ E Or 𝑦)
56		onssnum 10059	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ V ∧ 𝑦 ⊆ On) → 𝑦 ∈ dom card)
57	47, 56	mpan 690	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ⊆ On → 𝑦 ∈ dom card)
58		cardid2 9972	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ dom card → (card‘𝑦) ≈ 𝑦)
59		ensym 9022	. . . . . . . . . . . . . . . . . 18 ⊢ ((card‘𝑦) ≈ 𝑦 → 𝑦 ≈ (card‘𝑦))
60	57, 58, 59	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ On → 𝑦 ≈ (card‘𝑦))
61		nnsdom 9673	. . . . . . . . . . . . . . . . 17 ⊢ ((card‘𝑦) ∈ ω → (card‘𝑦) ≺ ω)
62		ensdomtr 9132	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ≈ (card‘𝑦) ∧ (card‘𝑦) ≺ ω) → 𝑦 ≺ ω)
63	60, 61, 62	syl2an 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ⊆ On ∧ (card‘𝑦) ∈ ω) → 𝑦 ≺ ω)
64		isfinite 9671	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ Fin ↔ 𝑦 ≺ ω)
65	63, 64	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ⊆ On ∧ (card‘𝑦) ∈ ω) → 𝑦 ∈ Fin)
66		wofi 9302	. . . . . . . . . . . . . . 15 ⊢ ((◡ E Or 𝑦 ∧ 𝑦 ∈ Fin) → ◡ E We 𝑦)
67	55, 65, 66	syl2an2r 685	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ⊆ On ∧ (card‘𝑦) ∈ ω) → ◡ E We 𝑦)
68	9, 67	sylan 580	. . . . . . . . . . . . 13 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → ◡ E We 𝑦)
69		wefr 5649	. . . . . . . . . . . . 13 ⊢ (◡ E We 𝑦 → ◡ E Fr 𝑦)
70	68, 69	syl 17	. . . . . . . . . . . 12 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → ◡ E Fr 𝑦)
71		ssidd 3987	. . . . . . . . . . . 12 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦 ⊆ 𝑦)
72		unieq 4899	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ∅ → ∪ 𝑦 = ∪ ∅)
73		uni0 4916	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ ∅ = ∅
74	72, 73	eqtrdi 2787	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ∅ → ∪ 𝑦 = ∅)
75		eqeq1 2740	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑦 = 𝐴 → (∪ 𝑦 = ∅ ↔ 𝐴 = ∅))
76	74, 75	imbitrid 244	. . . . . . . . . . . . . . . . 17 ⊢ (∪ 𝑦 = 𝐴 → (𝑦 = ∅ → 𝐴 = ∅))
77		nlim0 6417	. . . . . . . . . . . . . . . . . 18 ⊢ ¬ Lim ∅
78		limeq 6369	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 = ∅ → (Lim 𝐴 ↔ Lim ∅))
79	77, 78	mtbiri 327	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 = ∅ → ¬ Lim 𝐴)
80	76, 79	syl6 35	. . . . . . . . . . . . . . . 16 ⊢ (∪ 𝑦 = 𝐴 → (𝑦 = ∅ → ¬ Lim 𝐴))
81	80	necon2ad 2948	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑦 = 𝐴 → (Lim 𝐴 → 𝑦 ≠ ∅))
82	81	impcom 407	. . . . . . . . . . . . . 14 ⊢ ((Lim 𝐴 ∧ ∪ 𝑦 = 𝐴) → 𝑦 ≠ ∅)
83	82	3adant2 1131	. . . . . . . . . . . . 13 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → 𝑦 ≠ ∅)
84	83	adantr 480	. . . . . . . . . . . 12 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦 ≠ ∅)
85		fri 5616	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ V ∧ ◡ E Fr 𝑦) ∧ (𝑦 ⊆ 𝑦 ∧ 𝑦 ≠ ∅)) → ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E 𝑠)
86	48, 70, 71, 84, 85	syl22anc 838	. . . . . . . . . . 11 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E 𝑠)
87	46, 86	mtand 815	. . . . . . . . . 10 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → ¬ (card‘𝑦) ∈ ω)
88		cardon 9963	. . . . . . . . . . 11 ⊢ (card‘𝑦) ∈ On
89		eloni 6367	. . . . . . . . . . 11 ⊢ ((card‘𝑦) ∈ On → Ord (card‘𝑦))
90		ordom 7876	. . . . . . . . . . . 12 ⊢ Ord ω
91		ordtri1 6390	. . . . . . . . . . . 12 ⊢ ((Ord ω ∧ Ord (card‘𝑦)) → (ω ⊆ (card‘𝑦) ↔ ¬ (card‘𝑦) ∈ ω))
92	90, 91	mpan 690	. . . . . . . . . . 11 ⊢ (Ord (card‘𝑦) → (ω ⊆ (card‘𝑦) ↔ ¬ (card‘𝑦) ∈ ω))
93	88, 89, 92	mp2b 10	. . . . . . . . . 10 ⊢ (ω ⊆ (card‘𝑦) ↔ ¬ (card‘𝑦) ∈ ω)
94	87, 93	sylibr 234	. . . . . . . . 9 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → ω ⊆ (card‘𝑦))
95	2, 94	syl3an2b 1406	. . . . . . . 8 ⊢ ((Lim 𝐴 ∧ 𝑦 ∈ 𝒫 𝐴 ∧ ∪ 𝑦 = 𝐴) → ω ⊆ (card‘𝑦))
96	95	3expb 1120	. . . . . . 7 ⊢ ((Lim 𝐴 ∧ (𝑦 ∈ 𝒫 𝐴 ∧ ∪ 𝑦 = 𝐴)) → ω ⊆ (card‘𝑦))
97	1, 96	sylan2b 594	. . . . . 6 ⊢ ((Lim 𝐴 ∧ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}) → ω ⊆ (card‘𝑦))
98	97	ralrimiva 3133	. . . . 5 ⊢ (Lim 𝐴 → ∀𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}ω ⊆ (card‘𝑦))
99		ssiin 5036	. . . . 5 ⊢ (ω ⊆ ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} (card‘𝑦) ↔ ∀𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}ω ⊆ (card‘𝑦))
100	98, 99	sylibr 234	. . . 4 ⊢ (Lim 𝐴 → ω ⊆ ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} (card‘𝑦))
101		cflim2.1	. . . . 5 ⊢ 𝐴 ∈ V
102	101	cflim3 10281	. . . 4 ⊢ (Lim 𝐴 → (cf‘𝐴) = ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} (card‘𝑦))
103	100, 102	sseqtrrd 4001	. . 3 ⊢ (Lim 𝐴 → ω ⊆ (cf‘𝐴))
104		fvex 6894	. . . . . . 7 ⊢ (card‘𝑦) ∈ V
105	104	dfiin2 5015	. . . . . 6 ⊢ ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} (card‘𝑦) = ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)}
106	102, 105	eqtrdi 2787	. . . . 5 ⊢ (Lim 𝐴 → (cf‘𝐴) = ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)})
107		cardlim 9991	. . . . . . . . 9 ⊢ (ω ⊆ (card‘𝑦) ↔ Lim (card‘𝑦))
108		sseq2 3990	. . . . . . . . . 10 ⊢ (𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ ω ⊆ (card‘𝑦)))
109		limeq 6369	. . . . . . . . . 10 ⊢ (𝑥 = (card‘𝑦) → (Lim 𝑥 ↔ Lim (card‘𝑦)))
110	108, 109	bibi12d 345	. . . . . . . . 9 ⊢ (𝑥 = (card‘𝑦) → ((ω ⊆ 𝑥 ↔ Lim 𝑥) ↔ (ω ⊆ (card‘𝑦) ↔ Lim (card‘𝑦))))
111	107, 110	mpbiri 258	. . . . . . . 8 ⊢ (𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ Lim 𝑥))
112	111	rexlimivw 3138	. . . . . . 7 ⊢ (∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ Lim 𝑥))
113	112	ss2abi 4047	. . . . . 6 ⊢ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)}
114		eleq1 2823	. . . . . . . . . 10 ⊢ (𝑥 = (card‘𝑦) → (𝑥 ∈ On ↔ (card‘𝑦) ∈ On))
115	88, 114	mpbiri 258	. . . . . . . . 9 ⊢ (𝑥 = (card‘𝑦) → 𝑥 ∈ On)
116	115	rexlimivw 3138	. . . . . . . 8 ⊢ (∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦) → 𝑥 ∈ On)
117	116	abssi 4050	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ On
118		fvex 6894	. . . . . . . . 9 ⊢ (cf‘𝐴) ∈ V
119	106, 118	eqeltrrdi 2844	. . . . . . . 8 ⊢ (Lim 𝐴 → ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ V)
120		intex 5319	. . . . . . . 8 ⊢ ({𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅ ↔ ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ V)
121	119, 120	sylibr 234	. . . . . . 7 ⊢ (Lim 𝐴 → {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅)
122		onint 7789	. . . . . . 7 ⊢ (({𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ On ∧ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅) → ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)})
123	117, 121, 122	sylancr 587	. . . . . 6 ⊢ (Lim 𝐴 → ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)})
124	113, 123	sselid 3961	. . . . 5 ⊢ (Lim 𝐴 → ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)})
125	106, 124	eqeltrd 2835	. . . 4 ⊢ (Lim 𝐴 → (cf‘𝐴) ∈ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)})
126		sseq2 3990	. . . . . 6 ⊢ (𝑥 = (cf‘𝐴) → (ω ⊆ 𝑥 ↔ ω ⊆ (cf‘𝐴)))
127		limeq 6369	. . . . . 6 ⊢ (𝑥 = (cf‘𝐴) → (Lim 𝑥 ↔ Lim (cf‘𝐴)))
128	126, 127	bibi12d 345	. . . . 5 ⊢ (𝑥 = (cf‘𝐴) → ((ω ⊆ 𝑥 ↔ Lim 𝑥) ↔ (ω ⊆ (cf‘𝐴) ↔ Lim (cf‘𝐴))))
129	118, 128	elab 3663	. . . 4 ⊢ ((cf‘𝐴) ∈ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)} ↔ (ω ⊆ (cf‘𝐴) ↔ Lim (cf‘𝐴)))
130	125, 129	sylib 218	. . 3 ⊢ (Lim 𝐴 → (ω ⊆ (cf‘𝐴) ↔ Lim (cf‘𝐴)))
131	103, 130	mpbid 232	. 2 ⊢ (Lim 𝐴 → Lim (cf‘𝐴))
132		eloni 6367	. . . . . . 7 ⊢ (𝐴 ∈ On → Ord 𝐴)
133		ordzsl 7845	. . . . . . 7 ⊢ (Ord 𝐴 ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴))
134	132, 133	sylib 218	. . . . . 6 ⊢ (𝐴 ∈ On → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴))
135		df-3or 1087	. . . . . . 7 ⊢ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴) ↔ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥) ∨ Lim 𝐴))
136		orcom 870	. . . . . . 7 ⊢ (((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥) ∨ Lim 𝐴) ↔ (Lim 𝐴 ∨ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)))
137		df-or 848	. . . . . . 7 ⊢ ((Lim 𝐴 ∨ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)) ↔ (¬ Lim 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)))
138	135, 136, 137	3bitri 297	. . . . . 6 ⊢ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴) ↔ (¬ Lim 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)))
139	134, 138	sylib 218	. . . . 5 ⊢ (𝐴 ∈ On → (¬ Lim 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)))
140		fveq2 6881	. . . . . . . . 9 ⊢ (𝐴 = ∅ → (cf‘𝐴) = (cf‘∅))
141		cf0 10270	. . . . . . . . 9 ⊢ (cf‘∅) = ∅
142	140, 141	eqtrdi 2787	. . . . . . . 8 ⊢ (𝐴 = ∅ → (cf‘𝐴) = ∅)
143		limeq 6369	. . . . . . . 8 ⊢ ((cf‘𝐴) = ∅ → (Lim (cf‘𝐴) ↔ Lim ∅))
144	142, 143	syl 17	. . . . . . 7 ⊢ (𝐴 = ∅ → (Lim (cf‘𝐴) ↔ Lim ∅))
145	77, 144	mtbiri 327	. . . . . 6 ⊢ (𝐴 = ∅ → ¬ Lim (cf‘𝐴))
146		1n0 8505	. . . . . . . . . 10 ⊢ 1o ≠ ∅
147		df1o2 8492	. . . . . . . . . . . 12 ⊢ 1o = {∅}
148	147	unieqi 4900	. . . . . . . . . . 11 ⊢ ∪ 1o = ∪ {∅}
149		0ex 5282	. . . . . . . . . . . 12 ⊢ ∅ ∈ V
150	149	unisn 4907	. . . . . . . . . . 11 ⊢ ∪ {∅} = ∅
151	148, 150	eqtri 2759	. . . . . . . . . 10 ⊢ ∪ 1o = ∅
152	146, 151	neeqtrri 3006	. . . . . . . . 9 ⊢ 1o ≠ ∪ 1o
153		limuni 6419	. . . . . . . . . 10 ⊢ (Lim 1o → 1o = ∪ 1o)
154	153	necon3ai 2958	. . . . . . . . 9 ⊢ (1o ≠ ∪ 1o → ¬ Lim 1o)
155	152, 154	ax-mp 5	. . . . . . . 8 ⊢ ¬ Lim 1o
156		fveq2 6881	. . . . . . . . . 10 ⊢ (𝐴 = suc 𝑥 → (cf‘𝐴) = (cf‘suc 𝑥))
157		cfsuc 10276	. . . . . . . . . 10 ⊢ (𝑥 ∈ On → (cf‘suc 𝑥) = 1o)
158	156, 157	sylan9eqr 2793	. . . . . . . . 9 ⊢ ((𝑥 ∈ On ∧ 𝐴 = suc 𝑥) → (cf‘𝐴) = 1o)
159		limeq 6369	. . . . . . . . 9 ⊢ ((cf‘𝐴) = 1o → (Lim (cf‘𝐴) ↔ Lim 1o))
160	158, 159	syl 17	. . . . . . . 8 ⊢ ((𝑥 ∈ On ∧ 𝐴 = suc 𝑥) → (Lim (cf‘𝐴) ↔ Lim 1o))
161	155, 160	mtbiri 327	. . . . . . 7 ⊢ ((𝑥 ∈ On ∧ 𝐴 = suc 𝑥) → ¬ Lim (cf‘𝐴))
162	161	rexlimiva 3134	. . . . . 6 ⊢ (∃𝑥 ∈ On 𝐴 = suc 𝑥 → ¬ Lim (cf‘𝐴))
163	145, 162	jaoi 857	. . . . 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 10267	. . . . . . . . 9 ⊢ cf:On⟶On
167	166	fdmi 6722	. . . . . . . 8 ⊢ dom cf = On
168	167	eleq2i 2827	. . . . . . 7 ⊢ (𝐴 ∈ dom cf ↔ 𝐴 ∈ On)
169		ndmfv 6916	. . . . . . 7 ⊢ (¬ 𝐴 ∈ dom cf → (cf‘𝐴) = ∅)
170	168, 169	sylnbir 331	. . . . . 6 ⊢ (¬ 𝐴 ∈ On → (cf‘𝐴) = ∅)
171	170, 143	syl 17	. . . . 5 ⊢ (¬ 𝐴 ∈ On → (Lim (cf‘𝐴) ↔ Lim ∅))
172	77, 171	mtbiri 327	. . . 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 209	1 ⊢ (Lim 𝐴 ↔ Lim (cf‘𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∨ w3o 1085   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  {cab 2714   ≠ wne 2933  ∀wral 3052  ∃wrex 3061  {crab 3420  Vcvv 3464   ⊆ wss 3931  ∅c0 4313  𝒫 cpw 4580  {csn 4606  ∪ cuni 4888  ∩ cint 4927  ∩ ciin 4973   class class class wbr 5124   E cep 5557   Or wor 5565   Fr wfr 5608   We wwe 5610  ^◡ccnv 5658  dom cdm 5659  Ord word 6356  Oncon0 6357  Lim wlim 6358  suc csuc 6359  ‘cfv 6536  ωcom 7866  1_oc1o 8478   ≈ cen 8961   ≺ csdm 8963  Fincfn 8964  cardccrd 9954  cfccf 9956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-rep 5254  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-inf2 9660

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rmo 3364  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-int 4928  df-iun 4974  df-iin 4975  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-se 5612  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7367  df-ov 7413  df-om 7867  df-2nd 7994  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-card 9958  df-cf 9960

This theorem is referenced by:  cfom  10283