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