MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cflim2 Structured version   Visualization version   GIF version

Theorem cflim2 9400
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.
StepHypRef Expression
1 rabid 3326 . . . . . . 7 (𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴} ↔ (𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴))
2 selpw 4385 . . . . . . . . 9 (𝑦 ∈ 𝒫 𝐴𝑦𝐴)
3 limord 6022 . . . . . . . . . . . . . . . . . . . 20 (Lim 𝐴 → Ord 𝐴)
4 ordsson 7250 . . . . . . . . . . . . . . . . . . . 20 (Ord 𝐴𝐴 ⊆ On)
5 sstr 3835 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦𝐴𝐴 ⊆ On) → 𝑦 ⊆ On)
65expcom 404 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ⊆ On → (𝑦𝐴𝑦 ⊆ On))
73, 4, 63syl 18 . . . . . . . . . . . . . . . . . . 19 (Lim 𝐴 → (𝑦𝐴𝑦 ⊆ On))
87imp 397 . . . . . . . . . . . . . . . . . 18 ((Lim 𝐴𝑦𝐴) → 𝑦 ⊆ On)
983adant3 1166 . . . . . . . . . . . . . . . . 17 ((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) → 𝑦 ⊆ On)
10 ssel2 3822 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ⊆ On ∧ 𝑠𝑦) → 𝑠 ∈ On)
11 eloni 5973 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ On → Ord 𝑠)
12 ordirr 5981 . . . . . . . . . . . . . . . . . . 19 (Ord 𝑠 → ¬ 𝑠𝑠)
1310, 11, 123syl 18 . . . . . . . . . . . . . . . . . 18 ((𝑦 ⊆ On ∧ 𝑠𝑦) → ¬ 𝑠𝑠)
14 ssel 3821 . . . . . . . . . . . . . . . . . . . 20 (𝑦𝑠 → (𝑠𝑦𝑠𝑠))
1514com12 32 . . . . . . . . . . . . . . . . . . 19 (𝑠𝑦 → (𝑦𝑠𝑠𝑠))
1615adantl 475 . . . . . . . . . . . . . . . . . 18 ((𝑦 ⊆ On ∧ 𝑠𝑦) → (𝑦𝑠𝑠𝑠))
1713, 16mtod 190 . . . . . . . . . . . . . . . . 17 ((𝑦 ⊆ On ∧ 𝑠𝑦) → ¬ 𝑦𝑠)
189, 17sylan 575 . . . . . . . . . . . . . . . 16 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ 𝑠𝑦) → ¬ 𝑦𝑠)
19 simpl2 1248 . . . . . . . . . . . . . . . . 17 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ 𝑠𝑦) → 𝑦𝐴)
20 sstr 3835 . . . . . . . . . . . . . . . . 17 ((𝑦𝐴𝐴𝑠) → 𝑦𝑠)
2119, 20sylan 575 . . . . . . . . . . . . . . . 16 ((((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ 𝑠𝑦) ∧ 𝐴𝑠) → 𝑦𝑠)
2218, 21mtand 850 . . . . . . . . . . . . . . 15 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ 𝑠𝑦) → ¬ 𝐴𝑠)
23 simpl3 1250 . . . . . . . . . . . . . . . 16 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ 𝑠𝑦) → 𝑦 = 𝐴)
2423sseq1d 3857 . . . . . . . . . . . . . . 15 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ 𝑠𝑦) → ( 𝑦𝑠𝐴𝑠))
2522, 24mtbird 317 . . . . . . . . . . . . . 14 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ 𝑠𝑦) → ¬ 𝑦𝑠)
26 unissb 4691 . . . . . . . . . . . . . 14 ( 𝑦𝑠 ↔ ∀𝑡𝑦 𝑡𝑠)
2725, 26sylnib 320 . . . . . . . . . . . . 13 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ 𝑠𝑦) → ¬ ∀𝑡𝑦 𝑡𝑠)
2827nrexdv 3209 . . . . . . . . . . . 12 ((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) → ¬ ∃𝑠𝑦𝑡𝑦 𝑡𝑠)
29 ssel 3821 . . . . . . . . . . . . . . . . 17 (𝑦 ⊆ On → (𝑠𝑦𝑠 ∈ On))
30 ssel 3821 . . . . . . . . . . . . . . . . 17 (𝑦 ⊆ On → (𝑡𝑦𝑡 ∈ On))
31 ontri1 5997 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ On ∧ 𝑠 ∈ On) → (𝑡𝑠 ↔ ¬ 𝑠𝑡))
3231ancoms 452 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ On ∧ 𝑡 ∈ On) → (𝑡𝑠 ↔ ¬ 𝑠𝑡))
33 vex 3417 . . . . . . . . . . . . . . . . . . . . . 22 𝑡 ∈ V
34 vex 3417 . . . . . . . . . . . . . . . . . . . . . 22 𝑠 ∈ V
3533, 34brcnv 5537 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 E 𝑠𝑠 E 𝑡)
36 epel 5258 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 E 𝑡𝑠𝑡)
3735, 36bitri 267 . . . . . . . . . . . . . . . . . . . 20 (𝑡 E 𝑠𝑠𝑡)
3837notbii 312 . . . . . . . . . . . . . . . . . . 19 𝑡 E 𝑠 ↔ ¬ 𝑠𝑡)
3932, 38syl6bbr 281 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ On ∧ 𝑡 ∈ On) → (𝑡𝑠 ↔ ¬ 𝑡 E 𝑠))
4039a1i 11 . . . . . . . . . . . . . . . . 17 (𝑦 ⊆ On → ((𝑠 ∈ On ∧ 𝑡 ∈ On) → (𝑡𝑠 ↔ ¬ 𝑡 E 𝑠)))
4129, 30, 40syl2and 601 . . . . . . . . . . . . . . . 16 (𝑦 ⊆ On → ((𝑠𝑦𝑡𝑦) → (𝑡𝑠 ↔ ¬ 𝑡 E 𝑠)))
4241impl 449 . . . . . . . . . . . . . . 15 (((𝑦 ⊆ On ∧ 𝑠𝑦) ∧ 𝑡𝑦) → (𝑡𝑠 ↔ ¬ 𝑡 E 𝑠))
4342ralbidva 3194 . . . . . . . . . . . . . 14 ((𝑦 ⊆ On ∧ 𝑠𝑦) → (∀𝑡𝑦 𝑡𝑠 ↔ ∀𝑡𝑦 ¬ 𝑡 E 𝑠))
4443rexbidva 3259 . . . . . . . . . . . . 13 (𝑦 ⊆ On → (∃𝑠𝑦𝑡𝑦 𝑡𝑠 ↔ ∃𝑠𝑦𝑡𝑦 ¬ 𝑡 E 𝑠))
459, 44syl 17 . . . . . . . . . . . 12 ((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) → (∃𝑠𝑦𝑡𝑦 𝑡𝑠 ↔ ∃𝑠𝑦𝑡𝑦 ¬ 𝑡 E 𝑠))
4628, 45mtbid 316 . . . . . . . . . . 11 ((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) → ¬ ∃𝑠𝑦𝑡𝑦 ¬ 𝑡 E 𝑠)
47 vex 3417 . . . . . . . . . . . . 13 𝑦 ∈ V
4847a1i 11 . . . . . . . . . . . 12 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦 ∈ V)
49 epweon 7243 . . . . . . . . . . . . . . . . . . 19 E We On
50 wess 5329 . . . . . . . . . . . . . . . . . . 19 (𝑦 ⊆ On → ( E We On → E We 𝑦))
5149, 50mpi 20 . . . . . . . . . . . . . . . . . 18 (𝑦 ⊆ On → E We 𝑦)
52 weso 5333 . . . . . . . . . . . . . . . . . 18 ( E We 𝑦 → E Or 𝑦)
5351, 52syl 17 . . . . . . . . . . . . . . . . 17 (𝑦 ⊆ On → E Or 𝑦)
54 cnvso 5915 . . . . . . . . . . . . . . . . 17 ( E Or 𝑦 E Or 𝑦)
5553, 54sylib 210 . . . . . . . . . . . . . . . 16 (𝑦 ⊆ On → E Or 𝑦)
5655adantr 474 . . . . . . . . . . . . . . 15 ((𝑦 ⊆ On ∧ (card‘𝑦) ∈ ω) → E Or 𝑦)
57 onssnum 9176 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ V ∧ 𝑦 ⊆ On) → 𝑦 ∈ dom card)
5847, 57mpan 681 . . . . . . . . . . . . . . . . . 18 (𝑦 ⊆ On → 𝑦 ∈ dom card)
59 cardid2 9092 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ dom card → (card‘𝑦) ≈ 𝑦)
60 ensym 8271 . . . . . . . . . . . . . . . . . 18 ((card‘𝑦) ≈ 𝑦𝑦 ≈ (card‘𝑦))
6158, 59, 603syl 18 . . . . . . . . . . . . . . . . 17 (𝑦 ⊆ On → 𝑦 ≈ (card‘𝑦))
62 nnsdom 8828 . . . . . . . . . . . . . . . . 17 ((card‘𝑦) ∈ ω → (card‘𝑦) ≺ ω)
63 ensdomtr 8365 . . . . . . . . . . . . . . . . 17 ((𝑦 ≈ (card‘𝑦) ∧ (card‘𝑦) ≺ ω) → 𝑦 ≺ ω)
6461, 62, 63syl2an 589 . . . . . . . . . . . . . . . 16 ((𝑦 ⊆ On ∧ (card‘𝑦) ∈ ω) → 𝑦 ≺ ω)
65 isfinite 8826 . . . . . . . . . . . . . . . 16 (𝑦 ∈ Fin ↔ 𝑦 ≺ ω)
6664, 65sylibr 226 . . . . . . . . . . . . . . 15 ((𝑦 ⊆ On ∧ (card‘𝑦) ∈ ω) → 𝑦 ∈ Fin)
67 wofi 8478 . . . . . . . . . . . . . . 15 (( E Or 𝑦𝑦 ∈ Fin) → E We 𝑦)
6856, 66, 67syl2anc 579 . . . . . . . . . . . . . 14 ((𝑦 ⊆ On ∧ (card‘𝑦) ∈ ω) → E We 𝑦)
699, 68sylan 575 . . . . . . . . . . . . 13 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → E We 𝑦)
70 wefr 5332 . . . . . . . . . . . . 13 ( E We 𝑦 E Fr 𝑦)
7169, 70syl 17 . . . . . . . . . . . 12 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → E Fr 𝑦)
72 ssidd 3849 . . . . . . . . . . . 12 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦𝑦)
73 unieq 4666 . . . . . . . . . . . . . . . . . . 19 (𝑦 = ∅ → 𝑦 = ∅)
74 uni0 4687 . . . . . . . . . . . . . . . . . . 19 ∅ = ∅
7573, 74syl6eq 2877 . . . . . . . . . . . . . . . . . 18 (𝑦 = ∅ → 𝑦 = ∅)
76 eqeq1 2829 . . . . . . . . . . . . . . . . . 18 ( 𝑦 = 𝐴 → ( 𝑦 = ∅ ↔ 𝐴 = ∅))
7775, 76syl5ib 236 . . . . . . . . . . . . . . . . 17 ( 𝑦 = 𝐴 → (𝑦 = ∅ → 𝐴 = ∅))
78 nlim0 6021 . . . . . . . . . . . . . . . . . 18 ¬ Lim ∅
79 limeq 5975 . . . . . . . . . . . . . . . . . 18 (𝐴 = ∅ → (Lim 𝐴 ↔ Lim ∅))
8078, 79mtbiri 319 . . . . . . . . . . . . . . . . 17 (𝐴 = ∅ → ¬ Lim 𝐴)
8177, 80syl6 35 . . . . . . . . . . . . . . . 16 ( 𝑦 = 𝐴 → (𝑦 = ∅ → ¬ Lim 𝐴))
8281necon2ad 3014 . . . . . . . . . . . . . . 15 ( 𝑦 = 𝐴 → (Lim 𝐴𝑦 ≠ ∅))
8382impcom 398 . . . . . . . . . . . . . 14 ((Lim 𝐴 𝑦 = 𝐴) → 𝑦 ≠ ∅)
84833adant2 1165 . . . . . . . . . . . . 13 ((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) → 𝑦 ≠ ∅)
8584adantr 474 . . . . . . . . . . . 12 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦 ≠ ∅)
86 fri 5304 . . . . . . . . . . . 12 (((𝑦 ∈ V ∧ E Fr 𝑦) ∧ (𝑦𝑦𝑦 ≠ ∅)) → ∃𝑠𝑦𝑡𝑦 ¬ 𝑡 E 𝑠)
8748, 71, 72, 85, 86syl22anc 872 . . . . . . . . . . 11 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → ∃𝑠𝑦𝑡𝑦 ¬ 𝑡 E 𝑠)
8846, 87mtand 850 . . . . . . . . . 10 ((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) → ¬ (card‘𝑦) ∈ ω)
89 cardon 9083 . . . . . . . . . . 11 (card‘𝑦) ∈ On
90 eloni 5973 . . . . . . . . . . 11 ((card‘𝑦) ∈ On → Ord (card‘𝑦))
91 ordom 7335 . . . . . . . . . . . 12 Ord ω
92 ordtri1 5996 . . . . . . . . . . . 12 ((Ord ω ∧ Ord (card‘𝑦)) → (ω ⊆ (card‘𝑦) ↔ ¬ (card‘𝑦) ∈ ω))
9391, 92mpan 681 . . . . . . . . . . 11 (Ord (card‘𝑦) → (ω ⊆ (card‘𝑦) ↔ ¬ (card‘𝑦) ∈ ω))
9489, 90, 93mp2b 10 . . . . . . . . . 10 (ω ⊆ (card‘𝑦) ↔ ¬ (card‘𝑦) ∈ ω)
9588, 94sylibr 226 . . . . . . . . 9 ((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) → ω ⊆ (card‘𝑦))
962, 95syl3an2b 1527 . . . . . . . 8 ((Lim 𝐴𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴) → ω ⊆ (card‘𝑦))
97963expb 1153 . . . . . . 7 ((Lim 𝐴 ∧ (𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴)) → ω ⊆ (card‘𝑦))
981, 97sylan2b 587 . . . . . 6 ((Lim 𝐴𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}) → ω ⊆ (card‘𝑦))
9998ralrimiva 3175 . . . . 5 (Lim 𝐴 → ∀𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}ω ⊆ (card‘𝑦))
100 ssiin 4790 . . . . 5 (ω ⊆ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴} (card‘𝑦) ↔ ∀𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}ω ⊆ (card‘𝑦))
10199, 100sylibr 226 . . . 4 (Lim 𝐴 → ω ⊆ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴} (card‘𝑦))
102 cflim2.1 . . . . 5 𝐴 ∈ V
103102cflim3 9399 . . . 4 (Lim 𝐴 → (cf‘𝐴) = 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴} (card‘𝑦))
104101, 103sseqtr4d 3867 . . 3 (Lim 𝐴 → ω ⊆ (cf‘𝐴))
105 fvex 6446 . . . . . . 7 (card‘𝑦) ∈ V
106105dfiin2 4775 . . . . . 6 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴} (card‘𝑦) = {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)}
107103, 106syl6eq 2877 . . . . 5 (Lim 𝐴 → (cf‘𝐴) = {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)})
108 cardlim 9111 . . . . . . . . 9 (ω ⊆ (card‘𝑦) ↔ Lim (card‘𝑦))
109 sseq2 3852 . . . . . . . . . 10 (𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ ω ⊆ (card‘𝑦)))
110 limeq 5975 . . . . . . . . . 10 (𝑥 = (card‘𝑦) → (Lim 𝑥 ↔ Lim (card‘𝑦)))
111109, 110bibi12d 337 . . . . . . . . 9 (𝑥 = (card‘𝑦) → ((ω ⊆ 𝑥 ↔ Lim 𝑥) ↔ (ω ⊆ (card‘𝑦) ↔ Lim (card‘𝑦))))
112108, 111mpbiri 250 . . . . . . . 8 (𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ Lim 𝑥))
113112rexlimivw 3238 . . . . . . 7 (∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ Lim 𝑥))
114113ss2abi 3899 . . . . . 6 {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)}
115 eleq1 2894 . . . . . . . . . 10 (𝑥 = (card‘𝑦) → (𝑥 ∈ On ↔ (card‘𝑦) ∈ On))
11689, 115mpbiri 250 . . . . . . . . 9 (𝑥 = (card‘𝑦) → 𝑥 ∈ On)
117116rexlimivw 3238 . . . . . . . 8 (∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦) → 𝑥 ∈ On)
118117abssi 3902 . . . . . . 7 {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ On
119 fvex 6446 . . . . . . . . 9 (cf‘𝐴) ∈ V
120107, 119syl6eqelr 2915 . . . . . . . 8 (Lim 𝐴 {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ V)
121 intex 5042 . . . . . . . 8 ({𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅ ↔ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ V)
122120, 121sylibr 226 . . . . . . 7 (Lim 𝐴 → {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅)
123 onint 7256 . . . . . . 7 (({𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ On ∧ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅) → {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)})
124118, 122, 123sylancr 581 . . . . . 6 (Lim 𝐴 {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)})
125114, 124sseldi 3825 . . . . 5 (Lim 𝐴 {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)})
126107, 125eqeltrd 2906 . . . 4 (Lim 𝐴 → (cf‘𝐴) ∈ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)})
127 sseq2 3852 . . . . . 6 (𝑥 = (cf‘𝐴) → (ω ⊆ 𝑥 ↔ ω ⊆ (cf‘𝐴)))
128 limeq 5975 . . . . . 6 (𝑥 = (cf‘𝐴) → (Lim 𝑥 ↔ Lim (cf‘𝐴)))
129127, 128bibi12d 337 . . . . 5 (𝑥 = (cf‘𝐴) → ((ω ⊆ 𝑥 ↔ Lim 𝑥) ↔ (ω ⊆ (cf‘𝐴) ↔ Lim (cf‘𝐴))))
130119, 129elab 3571 . . . 4 ((cf‘𝐴) ∈ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)} ↔ (ω ⊆ (cf‘𝐴) ↔ Lim (cf‘𝐴)))
131126, 130sylib 210 . . 3 (Lim 𝐴 → (ω ⊆ (cf‘𝐴) ↔ Lim (cf‘𝐴)))
132104, 131mpbid 224 . 2 (Lim 𝐴 → Lim (cf‘𝐴))
133 eloni 5973 . . . . . . 7 (𝐴 ∈ On → Ord 𝐴)
134 ordzsl 7306 . . . . . . 7 (Ord 𝐴 ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴))
135133, 134sylib 210 . . . . . 6 (𝐴 ∈ On → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴))
136 df-3or 1112 . . . . . . 7 ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴) ↔ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥) ∨ Lim 𝐴))
137 orcom 901 . . . . . . 7 (((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥) ∨ Lim 𝐴) ↔ (Lim 𝐴 ∨ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)))
138 df-or 879 . . . . . . 7 ((Lim 𝐴 ∨ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)) ↔ (¬ Lim 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)))
139136, 137, 1383bitri 289 . . . . . 6 ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴) ↔ (¬ Lim 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)))
140135, 139sylib 210 . . . . 5 (𝐴 ∈ On → (¬ Lim 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)))
141 fveq2 6433 . . . . . . . . 9 (𝐴 = ∅ → (cf‘𝐴) = (cf‘∅))
142 cf0 9388 . . . . . . . . 9 (cf‘∅) = ∅
143141, 142syl6eq 2877 . . . . . . . 8 (𝐴 = ∅ → (cf‘𝐴) = ∅)
144 limeq 5975 . . . . . . . 8 ((cf‘𝐴) = ∅ → (Lim (cf‘𝐴) ↔ Lim ∅))
145143, 144syl 17 . . . . . . 7 (𝐴 = ∅ → (Lim (cf‘𝐴) ↔ Lim ∅))
14678, 145mtbiri 319 . . . . . 6 (𝐴 = ∅ → ¬ Lim (cf‘𝐴))
147 1n0 7842 . . . . . . . . . 10 1o ≠ ∅
148 df1o2 7839 . . . . . . . . . . . 12 1o = {∅}
149148unieqi 4667 . . . . . . . . . . 11 1o = {∅}
150 0ex 5014 . . . . . . . . . . . 12 ∅ ∈ V
151150unisn 4674 . . . . . . . . . . 11 {∅} = ∅
152149, 151eqtri 2849 . . . . . . . . . 10 1o = ∅
153147, 152neeqtrri 3072 . . . . . . . . 9 1o 1o
154 limuni 6023 . . . . . . . . . 10 (Lim 1o → 1o = 1o)
155154necon3ai 3024 . . . . . . . . 9 (1o 1o → ¬ Lim 1o)
156153, 155ax-mp 5 . . . . . . . 8 ¬ Lim 1o
157 fveq2 6433 . . . . . . . . . 10 (𝐴 = suc 𝑥 → (cf‘𝐴) = (cf‘suc 𝑥))
158 cfsuc 9394 . . . . . . . . . 10 (𝑥 ∈ On → (cf‘suc 𝑥) = 1o)
159157, 158sylan9eqr 2883 . . . . . . . . 9 ((𝑥 ∈ On ∧ 𝐴 = suc 𝑥) → (cf‘𝐴) = 1o)
160 limeq 5975 . . . . . . . . 9 ((cf‘𝐴) = 1o → (Lim (cf‘𝐴) ↔ Lim 1o))
161159, 160syl 17 . . . . . . . 8 ((𝑥 ∈ On ∧ 𝐴 = suc 𝑥) → (Lim (cf‘𝐴) ↔ Lim 1o))
162156, 161mtbiri 319 . . . . . . 7 ((𝑥 ∈ On ∧ 𝐴 = suc 𝑥) → ¬ Lim (cf‘𝐴))
163162rexlimiva 3237 . . . . . 6 (∃𝑥 ∈ On 𝐴 = suc 𝑥 → ¬ Lim (cf‘𝐴))
164146, 163jaoi 888 . . . . 5 ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥) → ¬ Lim (cf‘𝐴))
165140, 164syl6 35 . . . 4 (𝐴 ∈ On → (¬ Lim 𝐴 → ¬ Lim (cf‘𝐴)))
166165con4d 115 . . 3 (𝐴 ∈ On → (Lim (cf‘𝐴) → Lim 𝐴))
167 cff 9385 . . . . . . . . 9 cf:On⟶On
168167fdmi 6288 . . . . . . . 8 dom cf = On
169168eleq2i 2898 . . . . . . 7 (𝐴 ∈ dom cf ↔ 𝐴 ∈ On)
170 ndmfv 6463 . . . . . . 7 𝐴 ∈ dom cf → (cf‘𝐴) = ∅)
171169, 170sylnbir 323 . . . . . 6 𝐴 ∈ On → (cf‘𝐴) = ∅)
172171, 144syl 17 . . . . 5 𝐴 ∈ On → (Lim (cf‘𝐴) ↔ Lim ∅))
17378, 172mtbiri 319 . . . 4 𝐴 ∈ On → ¬ Lim (cf‘𝐴))
174173pm2.21d 119 . . 3 𝐴 ∈ On → (Lim (cf‘𝐴) → Lim 𝐴))
175166, 174pm2.61i 177 . 2 (Lim (cf‘𝐴) → Lim 𝐴)
176132, 175impbii 201 1 (Lim 𝐴 ↔ Lim (cf‘𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  wo 878  w3o 1110  w3a 1111   = wceq 1656  wcel 2164  {cab 2811  wne 2999  wral 3117  wrex 3118  {crab 3121  Vcvv 3414  wss 3798  c0 4144  𝒫 cpw 4378  {csn 4397   cuni 4658   cint 4697   ciin 4741   class class class wbr 4873   E cep 5254   Or wor 5262   Fr wfr 5298   We wwe 5300  ccnv 5341  dom cdm 5342  Ord word 5962  Oncon0 5963  Lim wlim 5964  suc csuc 5965  cfv 6123  ωcom 7326  1oc1o 7819  cen 8219  csdm 8221  Fincfn 8222  cardccrd 9074  cfccf 9076
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-rep 4994  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209  ax-inf2 8815
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-int 4698  df-iun 4742  df-iin 4743  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-se 5302  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-pred 5920  df-ord 5966  df-on 5967  df-lim 5968  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-isom 6132  df-riota 6866  df-om 7327  df-wrecs 7672  df-recs 7734  df-rdg 7772  df-1o 7826  df-er 8009  df-en 8223  df-dom 8224  df-sdom 8225  df-fin 8226  df-card 9078  df-cf 9080
This theorem is referenced by:  cfom  9401
  Copyright terms: Public domain W3C validator