Theorem cflim2 10019

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 3310	. . . . . . 7 ⊢ (𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} ↔ (𝑦 ∈ 𝒫 𝐴 ∧ ∪ 𝑦 = 𝐴))
2		velpw 4538	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴)
3		limord 6325	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Lim 𝐴 → Ord 𝐴)
4		ordsson 7633	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Ord 𝐴 → 𝐴 ⊆ On)
5		sstr 3929	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ On) → 𝑦 ⊆ On)
6	5	expcom 414	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ⊆ On → (𝑦 ⊆ 𝐴 → 𝑦 ⊆ On))
7	3, 4, 6	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (Lim 𝐴 → (𝑦 ⊆ 𝐴 → 𝑦 ⊆ On))
8	7	imp 407	. . . . . . . . . . . . . . . . . 18 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴) → 𝑦 ⊆ On)
9	8	3adant3 1131	. . . . . . . . . . . . . . . . 17 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → 𝑦 ⊆ On)
10		ssel2 3916	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → 𝑠 ∈ On)
11		eloni 6276	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ On → Ord 𝑠)
12		ordirr 6284	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord 𝑠 → ¬ 𝑠 ∈ 𝑠)
13	10, 11, 12	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → ¬ 𝑠 ∈ 𝑠)
14		ssel 3914	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ⊆ 𝑠 → (𝑠 ∈ 𝑦 → 𝑠 ∈ 𝑠))
15	14	com12 32	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ 𝑦 → (𝑦 ⊆ 𝑠 → 𝑠 ∈ 𝑠))
16	15	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → (𝑦 ⊆ 𝑠 → 𝑠 ∈ 𝑠))
17	13, 16	mtod 197	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → ¬ 𝑦 ⊆ 𝑠)
18	9, 17	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ¬ 𝑦 ⊆ 𝑠)
19		simpl2 1191	. . . . . . . . . . . . . . . . 17 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → 𝑦 ⊆ 𝐴)
20		sstr 3929	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑠) → 𝑦 ⊆ 𝑠)
21	19, 20	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ ((((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) ∧ 𝐴 ⊆ 𝑠) → 𝑦 ⊆ 𝑠)
22	18, 21	mtand 813	. . . . . . . . . . . . . . 15 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ¬ 𝐴 ⊆ 𝑠)
23		simpl3 1192	. . . . . . . . . . . . . . . 16 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ∪ 𝑦 = 𝐴)
24	23	sseq1d 3952	. . . . . . . . . . . . . . 15 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → (∪ 𝑦 ⊆ 𝑠 ↔ 𝐴 ⊆ 𝑠))
25	22, 24	mtbird 325	. . . . . . . . . . . . . 14 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ¬ ∪ 𝑦 ⊆ 𝑠)
26		unissb 4873	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑦 ⊆ 𝑠 ↔ ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠)
27	25, 26	sylnib 328	. . . . . . . . . . . . 13 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ¬ ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠)
28	27	nrexdv 3198	. . . . . . . . . . . 12 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → ¬ ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠)
29		ssel 3914	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ On → (𝑠 ∈ 𝑦 → 𝑠 ∈ On))
30		ssel 3914	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ On → (𝑡 ∈ 𝑦 → 𝑡 ∈ On))
31		ontri1 6300	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ On ∧ 𝑠 ∈ On) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑠 ∈ 𝑡))
32	31	ancoms 459	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ∈ On ∧ 𝑡 ∈ On) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑠 ∈ 𝑡))
33		vex 3436	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑡 ∈ V
34		vex 3436	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑠 ∈ V
35	33, 34	brcnv 5791	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡◡ E 𝑠 ↔ 𝑠 E 𝑡)
36		epel 5498	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 E 𝑡 ↔ 𝑠 ∈ 𝑡)
37	35, 36	bitri 274	. . . . . . . . . . . . . . . . . . . 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 456	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) ∧ 𝑡 ∈ 𝑦) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑡◡ E 𝑠))
43	42	ralbidva 3111	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → (∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠 ↔ ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E 𝑠))
44	43	rexbidva 3225	. . . . . . . . . . . . 13 ⊢ (𝑦 ⊆ On → (∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠 ↔ ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E 𝑠))
45	9, 44	syl 17	. . . . . . . . . . . 12 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → (∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠 ↔ ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E 𝑠))
46	28, 45	mtbid 324	. . . . . . . . . . 11 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → ¬ ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E 𝑠)
47		vex 3436	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
48	47	a1i 11	. . . . . . . . . . . 12 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦 ∈ V)
49		epweon 7625	. . . . . . . . . . . . . . . . . 18 ⊢ E We On
50		wess 5576	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ⊆ On → ( E We On → E We 𝑦))
51	49, 50	mpi 20	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ On → E We 𝑦)
52		weso 5580	. . . . . . . . . . . . . . . . 17 ⊢ ( E We 𝑦 → E Or 𝑦)
53	51, 52	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ⊆ On → E Or 𝑦)
54		cnvso 6191	. . . . . . . . . . . . . . . 16 ⊢ ( E Or 𝑦 ↔ ◡ E Or 𝑦)
55	53, 54	sylib 217	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ⊆ On → ◡ E Or 𝑦)
56		onssnum 9796	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ V ∧ 𝑦 ⊆ On) → 𝑦 ∈ dom card)
57	47, 56	mpan 687	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ⊆ On → 𝑦 ∈ dom card)
58		cardid2 9711	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ dom card → (card‘𝑦) ≈ 𝑦)
59		ensym 8789	. . . . . . . . . . . . . . . . . 18 ⊢ ((card‘𝑦) ≈ 𝑦 → 𝑦 ≈ (card‘𝑦))
60	57, 58, 59	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ On → 𝑦 ≈ (card‘𝑦))
61		nnsdom 9412	. . . . . . . . . . . . . . . . 17 ⊢ ((card‘𝑦) ∈ ω → (card‘𝑦) ≺ ω)
62		ensdomtr 8900	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ≈ (card‘𝑦) ∧ (card‘𝑦) ≺ ω) → 𝑦 ≺ ω)
63	60, 61, 62	syl2an 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ⊆ On ∧ (card‘𝑦) ∈ ω) → 𝑦 ≺ ω)
64		isfinite 9410	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ Fin ↔ 𝑦 ≺ ω)
65	63, 64	sylibr 233	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ⊆ On ∧ (card‘𝑦) ∈ ω) → 𝑦 ∈ Fin)
66		wofi 9063	. . . . . . . . . . . . . . 15 ⊢ ((◡ E Or 𝑦 ∧ 𝑦 ∈ Fin) → ◡ E We 𝑦)
67	55, 65, 66	syl2an2r 682	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ⊆ On ∧ (card‘𝑦) ∈ ω) → ◡ E We 𝑦)
68	9, 67	sylan 580	. . . . . . . . . . . . 13 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → ◡ E We 𝑦)
69		wefr 5579	. . . . . . . . . . . . 13 ⊢ (◡ E We 𝑦 → ◡ E Fr 𝑦)
70	68, 69	syl 17	. . . . . . . . . . . 12 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → ◡ E Fr 𝑦)
71		ssidd 3944	. . . . . . . . . . . 12 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦 ⊆ 𝑦)
72		unieq 4850	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ∅ → ∪ 𝑦 = ∪ ∅)
73		uni0 4869	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ ∅ = ∅
74	72, 73	eqtrdi 2794	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ∅ → ∪ 𝑦 = ∅)
75		eqeq1 2742	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑦 = 𝐴 → (∪ 𝑦 = ∅ ↔ 𝐴 = ∅))
76	74, 75	syl5ib 243	. . . . . . . . . . . . . . . . 17 ⊢ (∪ 𝑦 = 𝐴 → (𝑦 = ∅ → 𝐴 = ∅))
77		nlim0 6324	. . . . . . . . . . . . . . . . . 18 ⊢ ¬ Lim ∅
78		limeq 6278	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 = ∅ → (Lim 𝐴 ↔ Lim ∅))
79	77, 78	mtbiri 327	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 = ∅ → ¬ Lim 𝐴)
80	76, 79	syl6 35	. . . . . . . . . . . . . . . 16 ⊢ (∪ 𝑦 = 𝐴 → (𝑦 = ∅ → ¬ Lim 𝐴))
81	80	necon2ad 2958	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑦 = 𝐴 → (Lim 𝐴 → 𝑦 ≠ ∅))
82	81	impcom 408	. . . . . . . . . . . . . 14 ⊢ ((Lim 𝐴 ∧ ∪ 𝑦 = 𝐴) → 𝑦 ≠ ∅)
83	82	3adant2 1130	. . . . . . . . . . . . 13 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → 𝑦 ≠ ∅)
84	83	adantr 481	. . . . . . . . . . . 12 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦 ≠ ∅)
85		fri 5549	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ V ∧ ◡ E Fr 𝑦) ∧ (𝑦 ⊆ 𝑦 ∧ 𝑦 ≠ ∅)) → ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E 𝑠)
86	48, 70, 71, 84, 85	syl22anc 836	. . . . . . . . . . 11 ⊢ (((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E 𝑠)
87	46, 86	mtand 813	. . . . . . . . . 10 ⊢ ((Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → ¬ (card‘𝑦) ∈ ω)
88		cardon 9702	. . . . . . . . . . 11 ⊢ (card‘𝑦) ∈ On
89		eloni 6276	. . . . . . . . . . 11 ⊢ ((card‘𝑦) ∈ On → Ord (card‘𝑦))
90		ordom 7722	. . . . . . . . . . . 12 ⊢ Ord ω
91		ordtri1 6299	. . . . . . . . . . . 12 ⊢ ((Ord ω ∧ Ord (card‘𝑦)) → (ω ⊆ (card‘𝑦) ↔ ¬ (card‘𝑦) ∈ ω))
92	90, 91	mpan 687	. . . . . . . . . . 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 1403	. . . . . . . 8 ⊢ ((Lim 𝐴 ∧ 𝑦 ∈ 𝒫 𝐴 ∧ ∪ 𝑦 = 𝐴) → ω ⊆ (card‘𝑦))
96	95	3expb 1119	. . . . . . 7 ⊢ ((Lim 𝐴 ∧ (𝑦 ∈ 𝒫 𝐴 ∧ ∪ 𝑦 = 𝐴)) → ω ⊆ (card‘𝑦))
97	1, 96	sylan2b 594	. . . . . 6 ⊢ ((Lim 𝐴 ∧ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}) → ω ⊆ (card‘𝑦))
98	97	ralrimiva 3103	. . . . 5 ⊢ (Lim 𝐴 → ∀𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}ω ⊆ (card‘𝑦))
99		ssiin 4985	. . . . 5 ⊢ (ω ⊆ ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} (card‘𝑦) ↔ ∀𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}ω ⊆ (card‘𝑦))
100	98, 99	sylibr 233	. . . 4 ⊢ (Lim 𝐴 → ω ⊆ ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} (card‘𝑦))
101		cflim2.1	. . . . 5 ⊢ 𝐴 ∈ V
102	101	cflim3 10018	. . . 4 ⊢ (Lim 𝐴 → (cf‘𝐴) = ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} (card‘𝑦))
103	100, 102	sseqtrrd 3962	. . 3 ⊢ (Lim 𝐴 → ω ⊆ (cf‘𝐴))
104		fvex 6787	. . . . . . 7 ⊢ (card‘𝑦) ∈ V
105	104	dfiin2 4964	. . . . . 6 ⊢ ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} (card‘𝑦) = ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)}
106	102, 105	eqtrdi 2794	. . . . 5 ⊢ (Lim 𝐴 → (cf‘𝐴) = ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)})
107		cardlim 9730	. . . . . . . . 9 ⊢ (ω ⊆ (card‘𝑦) ↔ Lim (card‘𝑦))
108		sseq2 3947	. . . . . . . . . 10 ⊢ (𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ ω ⊆ (card‘𝑦)))
109		limeq 6278	. . . . . . . . . 10 ⊢ (𝑥 = (card‘𝑦) → (Lim 𝑥 ↔ Lim (card‘𝑦)))
110	108, 109	bibi12d 346	. . . . . . . . 9 ⊢ (𝑥 = (card‘𝑦) → ((ω ⊆ 𝑥 ↔ Lim 𝑥) ↔ (ω ⊆ (card‘𝑦) ↔ Lim (card‘𝑦))))
111	107, 110	mpbiri 257	. . . . . . . 8 ⊢ (𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ Lim 𝑥))
112	111	rexlimivw 3211	. . . . . . 7 ⊢ (∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ Lim 𝑥))
113	112	ss2abi 4000	. . . . . 6 ⊢ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)}
114		eleq1 2826	. . . . . . . . . 10 ⊢ (𝑥 = (card‘𝑦) → (𝑥 ∈ On ↔ (card‘𝑦) ∈ On))
115	88, 114	mpbiri 257	. . . . . . . . 9 ⊢ (𝑥 = (card‘𝑦) → 𝑥 ∈ On)
116	115	rexlimivw 3211	. . . . . . . 8 ⊢ (∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦) → 𝑥 ∈ On)
117	116	abssi 4003	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ On
118		fvex 6787	. . . . . . . . 9 ⊢ (cf‘𝐴) ∈ V
119	106, 118	eqeltrrdi 2848	. . . . . . . 8 ⊢ (Lim 𝐴 → ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ V)
120		intex 5261	. . . . . . . 8 ⊢ ({𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅ ↔ ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ V)
121	119, 120	sylibr 233	. . . . . . 7 ⊢ (Lim 𝐴 → {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅)
122		onint 7640	. . . . . . 7 ⊢ (({𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ On ∧ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅) → ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)})
123	117, 121, 122	sylancr 587	. . . . . 6 ⊢ (Lim 𝐴 → ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)})
124	113, 123	sselid 3919	. . . . 5 ⊢ (Lim 𝐴 → ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)})
125	106, 124	eqeltrd 2839	. . . 4 ⊢ (Lim 𝐴 → (cf‘𝐴) ∈ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)})
126		sseq2 3947	. . . . . 6 ⊢ (𝑥 = (cf‘𝐴) → (ω ⊆ 𝑥 ↔ ω ⊆ (cf‘𝐴)))
127		limeq 6278	. . . . . 6 ⊢ (𝑥 = (cf‘𝐴) → (Lim 𝑥 ↔ Lim (cf‘𝐴)))
128	126, 127	bibi12d 346	. . . . 5 ⊢ (𝑥 = (cf‘𝐴) → ((ω ⊆ 𝑥 ↔ Lim 𝑥) ↔ (ω ⊆ (cf‘𝐴) ↔ Lim (cf‘𝐴))))
129	118, 128	elab 3609	. . . 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 6276	. . . . . . 7 ⊢ (𝐴 ∈ On → Ord 𝐴)
133		ordzsl 7692	. . . . . . 7 ⊢ (Ord 𝐴 ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴))
134	132, 133	sylib 217	. . . . . 6 ⊢ (𝐴 ∈ On → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴))
135		df-3or 1087	. . . . . . 7 ⊢ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴) ↔ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥) ∨ Lim 𝐴))
136		orcom 867	. . . . . . 7 ⊢ (((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥) ∨ Lim 𝐴) ↔ (Lim 𝐴 ∨ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)))
137		df-or 845	. . . . . . 7 ⊢ ((Lim 𝐴 ∨ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)) ↔ (¬ Lim 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)))
138	135, 136, 137	3bitri 297	. . . . . 6 ⊢ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴) ↔ (¬ Lim 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)))
139	134, 138	sylib 217	. . . . 5 ⊢ (𝐴 ∈ On → (¬ Lim 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)))
140		fveq2 6774	. . . . . . . . 9 ⊢ (𝐴 = ∅ → (cf‘𝐴) = (cf‘∅))
141		cf0 10007	. . . . . . . . 9 ⊢ (cf‘∅) = ∅
142	140, 141	eqtrdi 2794	. . . . . . . 8 ⊢ (𝐴 = ∅ → (cf‘𝐴) = ∅)
143		limeq 6278	. . . . . . . 8 ⊢ ((cf‘𝐴) = ∅ → (Lim (cf‘𝐴) ↔ Lim ∅))
144	142, 143	syl 17	. . . . . . 7 ⊢ (𝐴 = ∅ → (Lim (cf‘𝐴) ↔ Lim ∅))
145	77, 144	mtbiri 327	. . . . . 6 ⊢ (𝐴 = ∅ → ¬ Lim (cf‘𝐴))
146		1n0 8318	. . . . . . . . . 10 ⊢ 1o ≠ ∅
147		df1o2 8304	. . . . . . . . . . . 12 ⊢ 1o = {∅}
148	147	unieqi 4852	. . . . . . . . . . 11 ⊢ ∪ 1o = ∪ {∅}
149		0ex 5231	. . . . . . . . . . . 12 ⊢ ∅ ∈ V
150	149	unisn 4861	. . . . . . . . . . 11 ⊢ ∪ {∅} = ∅
151	148, 150	eqtri 2766	. . . . . . . . . 10 ⊢ ∪ 1o = ∅
152	146, 151	neeqtrri 3017	. . . . . . . . 9 ⊢ 1o ≠ ∪ 1o
153		limuni 6326	. . . . . . . . . 10 ⊢ (Lim 1o → 1o = ∪ 1o)
154	153	necon3ai 2968	. . . . . . . . 9 ⊢ (1o ≠ ∪ 1o → ¬ Lim 1o)
155	152, 154	ax-mp 5	. . . . . . . 8 ⊢ ¬ Lim 1o
156		fveq2 6774	. . . . . . . . . 10 ⊢ (𝐴 = suc 𝑥 → (cf‘𝐴) = (cf‘suc 𝑥))
157		cfsuc 10013	. . . . . . . . . 10 ⊢ (𝑥 ∈ On → (cf‘suc 𝑥) = 1o)
158	156, 157	sylan9eqr 2800	. . . . . . . . 9 ⊢ ((𝑥 ∈ On ∧ 𝐴 = suc 𝑥) → (cf‘𝐴) = 1o)
159		limeq 6278	. . . . . . . . 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 3210	. . . . . 6 ⊢ (∃𝑥 ∈ On 𝐴 = suc 𝑥 → ¬ Lim (cf‘𝐴))
163	145, 162	jaoi 854	. . . . 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 10004	. . . . . . . . 9 ⊢ cf:On⟶On
167	166	fdmi 6612	. . . . . . . 8 ⊢ dom cf = On
168	167	eleq2i 2830	. . . . . . 7 ⊢ (𝐴 ∈ dom cf ↔ 𝐴 ∈ On)
169		ndmfv 6804	. . . . . . 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 208	1 ⊢ (Lim 𝐴 ↔ Lim (cf‘𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844   ∨ w3o 1085   ∧ w3a 1086   = wceq 1539   ∈ wcel 2106  {cab 2715   ≠ wne 2943  ∀wral 3064  ∃wrex 3065  {crab 3068  Vcvv 3432   ⊆ wss 3887  ∅c0 4256  𝒫 cpw 4533  {csn 4561  ∪ cuni 4839  ∩ cint 4879  ∩ ciin 4925   class class class wbr 5074   E cep 5494   Or wor 5502   Fr wfr 5541   We wwe 5543  ^◡ccnv 5588  dom cdm 5589  Ord word 6265  Oncon0 6266  Lim wlim 6267  suc csuc 6268  ‘cfv 6433  ωcom 7712  1_oc1o 8290   ≈ cen 8730   ≺ csdm 8732  Fincfn 8733  cardccrd 9693  cfccf 9695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-inf2 9399

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-iin 4927  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-isom 6442  df-riota 7232  df-ov 7278  df-om 7713  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-card 9697  df-cf 9699

This theorem is referenced by:  cfom  10020