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

Theorem cflim2 9277
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 3254 . . . . . . 7 (𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴} ↔ (𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴))
2 selpw 4309 . . . . . . . . 9 (𝑦 ∈ 𝒫 𝐴𝑦𝐴)
3 limord 5945 . . . . . . . . . . . . . . . . . . . 20 (Lim 𝐴 → Ord 𝐴)
4 ordsson 7154 . . . . . . . . . . . . . . . . . . . 20 (Ord 𝐴𝐴 ⊆ On)
5 sstr 3752 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦𝐴𝐴 ⊆ On) → 𝑦 ⊆ On)
65expcom 450 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ⊆ On → (𝑦𝐴𝑦 ⊆ On))
73, 4, 63syl 18 . . . . . . . . . . . . . . . . . . 19 (Lim 𝐴 → (𝑦𝐴𝑦 ⊆ On))
87imp 444 . . . . . . . . . . . . . . . . . 18 ((Lim 𝐴𝑦𝐴) → 𝑦 ⊆ On)
983adant3 1127 . . . . . . . . . . . . . . . . 17 ((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) → 𝑦 ⊆ On)
10 ssel2 3739 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ⊆ On ∧ 𝑠𝑦) → 𝑠 ∈ On)
11 eloni 5894 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ On → Ord 𝑠)
12 ordirr 5902 . . . . . . . . . . . . . . . . . . 19 (Ord 𝑠 → ¬ 𝑠𝑠)
1310, 11, 123syl 18 . . . . . . . . . . . . . . . . . 18 ((𝑦 ⊆ On ∧ 𝑠𝑦) → ¬ 𝑠𝑠)
14 ssel 3738 . . . . . . . . . . . . . . . . . . . 20 (𝑦𝑠 → (𝑠𝑦𝑠𝑠))
1514com12 32 . . . . . . . . . . . . . . . . . . 19 (𝑠𝑦 → (𝑦𝑠𝑠𝑠))
1615adantl 473 . . . . . . . . . . . . . . . . . 18 ((𝑦 ⊆ On ∧ 𝑠𝑦) → (𝑦𝑠𝑠𝑠))
1713, 16mtod 189 . . . . . . . . . . . . . . . . 17 ((𝑦 ⊆ On ∧ 𝑠𝑦) → ¬ 𝑦𝑠)
189, 17sylan 489 . . . . . . . . . . . . . . . 16 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ 𝑠𝑦) → ¬ 𝑦𝑠)
19 simpl2 1230 . . . . . . . . . . . . . . . . 17 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ 𝑠𝑦) → 𝑦𝐴)
20 sstr 3752 . . . . . . . . . . . . . . . . 17 ((𝑦𝐴𝐴𝑠) → 𝑦𝑠)
2119, 20sylan 489 . . . . . . . . . . . . . . . 16 ((((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ 𝑠𝑦) ∧ 𝐴𝑠) → 𝑦𝑠)
2218, 21mtand 694 . . . . . . . . . . . . . . 15 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ 𝑠𝑦) → ¬ 𝐴𝑠)
23 simpl3 1232 . . . . . . . . . . . . . . . 16 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ 𝑠𝑦) → 𝑦 = 𝐴)
2423sseq1d 3773 . . . . . . . . . . . . . . 15 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ 𝑠𝑦) → ( 𝑦𝑠𝐴𝑠))
2522, 24mtbird 314 . . . . . . . . . . . . . 14 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ 𝑠𝑦) → ¬ 𝑦𝑠)
26 unissb 4621 . . . . . . . . . . . . . 14 ( 𝑦𝑠 ↔ ∀𝑡𝑦 𝑡𝑠)
2725, 26sylnib 317 . . . . . . . . . . . . 13 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ 𝑠𝑦) → ¬ ∀𝑡𝑦 𝑡𝑠)
2827nrexdv 3139 . . . . . . . . . . . 12 ((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) → ¬ ∃𝑠𝑦𝑡𝑦 𝑡𝑠)
29 ssel 3738 . . . . . . . . . . . . . . . . 17 (𝑦 ⊆ On → (𝑠𝑦𝑠 ∈ On))
30 ssel 3738 . . . . . . . . . . . . . . . . 17 (𝑦 ⊆ On → (𝑡𝑦𝑡 ∈ On))
31 ontri1 5918 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ On ∧ 𝑠 ∈ On) → (𝑡𝑠 ↔ ¬ 𝑠𝑡))
3231ancoms 468 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ On ∧ 𝑡 ∈ On) → (𝑡𝑠 ↔ ¬ 𝑠𝑡))
33 vex 3343 . . . . . . . . . . . . . . . . . . . . . 22 𝑡 ∈ V
34 vex 3343 . . . . . . . . . . . . . . . . . . . . . 22 𝑠 ∈ V
3533, 34brcnv 5460 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 E 𝑠𝑠 E 𝑡)
36 epel 5182 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 E 𝑡𝑠𝑡)
3735, 36bitri 264 . . . . . . . . . . . . . . . . . . . 20 (𝑡 E 𝑠𝑠𝑡)
3837notbii 309 . . . . . . . . . . . . . . . . . . 19 𝑡 E 𝑠 ↔ ¬ 𝑠𝑡)
3932, 38syl6bbr 278 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ On ∧ 𝑡 ∈ On) → (𝑡𝑠 ↔ ¬ 𝑡 E 𝑠))
4039a1i 11 . . . . . . . . . . . . . . . . 17 (𝑦 ⊆ On → ((𝑠 ∈ On ∧ 𝑡 ∈ On) → (𝑡𝑠 ↔ ¬ 𝑡 E 𝑠)))
4129, 30, 40syl2and 501 . . . . . . . . . . . . . . . 16 (𝑦 ⊆ On → ((𝑠𝑦𝑡𝑦) → (𝑡𝑠 ↔ ¬ 𝑡 E 𝑠)))
4241impl 651 . . . . . . . . . . . . . . 15 (((𝑦 ⊆ On ∧ 𝑠𝑦) ∧ 𝑡𝑦) → (𝑡𝑠 ↔ ¬ 𝑡 E 𝑠))
4342ralbidva 3123 . . . . . . . . . . . . . 14 ((𝑦 ⊆ On ∧ 𝑠𝑦) → (∀𝑡𝑦 𝑡𝑠 ↔ ∀𝑡𝑦 ¬ 𝑡 E 𝑠))
4443rexbidva 3187 . . . . . . . . . . . . 13 (𝑦 ⊆ On → (∃𝑠𝑦𝑡𝑦 𝑡𝑠 ↔ ∃𝑠𝑦𝑡𝑦 ¬ 𝑡 E 𝑠))
459, 44syl 17 . . . . . . . . . . . 12 ((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) → (∃𝑠𝑦𝑡𝑦 𝑡𝑠 ↔ ∃𝑠𝑦𝑡𝑦 ¬ 𝑡 E 𝑠))
4628, 45mtbid 313 . . . . . . . . . . 11 ((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) → ¬ ∃𝑠𝑦𝑡𝑦 ¬ 𝑡 E 𝑠)
47 vex 3343 . . . . . . . . . . . . 13 𝑦 ∈ V
4847a1i 11 . . . . . . . . . . . 12 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦 ∈ V)
49 epweon 7148 . . . . . . . . . . . . . . . . . . 19 E We On
50 wess 5253 . . . . . . . . . . . . . . . . . . 19 (𝑦 ⊆ On → ( E We On → E We 𝑦))
5149, 50mpi 20 . . . . . . . . . . . . . . . . . 18 (𝑦 ⊆ On → E We 𝑦)
52 weso 5257 . . . . . . . . . . . . . . . . . 18 ( E We 𝑦 → E Or 𝑦)
5351, 52syl 17 . . . . . . . . . . . . . . . . 17 (𝑦 ⊆ On → E Or 𝑦)
54 cnvso 5835 . . . . . . . . . . . . . . . . 17 ( E Or 𝑦 E Or 𝑦)
5553, 54sylib 208 . . . . . . . . . . . . . . . 16 (𝑦 ⊆ On → E Or 𝑦)
5655adantr 472 . . . . . . . . . . . . . . 15 ((𝑦 ⊆ On ∧ (card‘𝑦) ∈ ω) → E Or 𝑦)
57 onssnum 9053 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ V ∧ 𝑦 ⊆ On) → 𝑦 ∈ dom card)
5847, 57mpan 708 . . . . . . . . . . . . . . . . . 18 (𝑦 ⊆ On → 𝑦 ∈ dom card)
59 cardid2 8969 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ dom card → (card‘𝑦) ≈ 𝑦)
60 ensym 8170 . . . . . . . . . . . . . . . . . 18 ((card‘𝑦) ≈ 𝑦𝑦 ≈ (card‘𝑦))
6158, 59, 603syl 18 . . . . . . . . . . . . . . . . 17 (𝑦 ⊆ On → 𝑦 ≈ (card‘𝑦))
62 nnsdom 8724 . . . . . . . . . . . . . . . . 17 ((card‘𝑦) ∈ ω → (card‘𝑦) ≺ ω)
63 ensdomtr 8261 . . . . . . . . . . . . . . . . 17 ((𝑦 ≈ (card‘𝑦) ∧ (card‘𝑦) ≺ ω) → 𝑦 ≺ ω)
6461, 62, 63syl2an 495 . . . . . . . . . . . . . . . 16 ((𝑦 ⊆ On ∧ (card‘𝑦) ∈ ω) → 𝑦 ≺ ω)
65 isfinite 8722 . . . . . . . . . . . . . . . 16 (𝑦 ∈ Fin ↔ 𝑦 ≺ ω)
6664, 65sylibr 224 . . . . . . . . . . . . . . 15 ((𝑦 ⊆ On ∧ (card‘𝑦) ∈ ω) → 𝑦 ∈ Fin)
67 wofi 8374 . . . . . . . . . . . . . . 15 (( E Or 𝑦𝑦 ∈ Fin) → E We 𝑦)
6856, 66, 67syl2anc 696 . . . . . . . . . . . . . 14 ((𝑦 ⊆ On ∧ (card‘𝑦) ∈ ω) → E We 𝑦)
699, 68sylan 489 . . . . . . . . . . . . 13 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → E We 𝑦)
70 wefr 5256 . . . . . . . . . . . . 13 ( E We 𝑦 E Fr 𝑦)
7169, 70syl 17 . . . . . . . . . . . 12 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → E Fr 𝑦)
72 ssid 3765 . . . . . . . . . . . . 13 𝑦𝑦
7372a1i 11 . . . . . . . . . . . 12 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦𝑦)
74 unieq 4596 . . . . . . . . . . . . . . . . . . 19 (𝑦 = ∅ → 𝑦 = ∅)
75 uni0 4617 . . . . . . . . . . . . . . . . . . 19 ∅ = ∅
7674, 75syl6eq 2810 . . . . . . . . . . . . . . . . . 18 (𝑦 = ∅ → 𝑦 = ∅)
77 eqeq1 2764 . . . . . . . . . . . . . . . . . 18 ( 𝑦 = 𝐴 → ( 𝑦 = ∅ ↔ 𝐴 = ∅))
7876, 77syl5ib 234 . . . . . . . . . . . . . . . . 17 ( 𝑦 = 𝐴 → (𝑦 = ∅ → 𝐴 = ∅))
79 nlim0 5944 . . . . . . . . . . . . . . . . . 18 ¬ Lim ∅
80 limeq 5896 . . . . . . . . . . . . . . . . . 18 (𝐴 = ∅ → (Lim 𝐴 ↔ Lim ∅))
8179, 80mtbiri 316 . . . . . . . . . . . . . . . . 17 (𝐴 = ∅ → ¬ Lim 𝐴)
8278, 81syl6 35 . . . . . . . . . . . . . . . 16 ( 𝑦 = 𝐴 → (𝑦 = ∅ → ¬ Lim 𝐴))
8382necon2ad 2947 . . . . . . . . . . . . . . 15 ( 𝑦 = 𝐴 → (Lim 𝐴𝑦 ≠ ∅))
8483impcom 445 . . . . . . . . . . . . . 14 ((Lim 𝐴 𝑦 = 𝐴) → 𝑦 ≠ ∅)
85843adant2 1126 . . . . . . . . . . . . 13 ((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) → 𝑦 ≠ ∅)
8685adantr 472 . . . . . . . . . . . 12 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦 ≠ ∅)
87 fri 5228 . . . . . . . . . . . 12 (((𝑦 ∈ V ∧ E Fr 𝑦) ∧ (𝑦𝑦𝑦 ≠ ∅)) → ∃𝑠𝑦𝑡𝑦 ¬ 𝑡 E 𝑠)
8848, 71, 73, 86, 87syl22anc 1478 . . . . . . . . . . 11 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → ∃𝑠𝑦𝑡𝑦 ¬ 𝑡 E 𝑠)
8946, 88mtand 694 . . . . . . . . . 10 ((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) → ¬ (card‘𝑦) ∈ ω)
90 cardon 8960 . . . . . . . . . . 11 (card‘𝑦) ∈ On
91 eloni 5894 . . . . . . . . . . 11 ((card‘𝑦) ∈ On → Ord (card‘𝑦))
92 ordom 7239 . . . . . . . . . . . 12 Ord ω
93 ordtri1 5917 . . . . . . . . . . . 12 ((Ord ω ∧ Ord (card‘𝑦)) → (ω ⊆ (card‘𝑦) ↔ ¬ (card‘𝑦) ∈ ω))
9492, 93mpan 708 . . . . . . . . . . 11 (Ord (card‘𝑦) → (ω ⊆ (card‘𝑦) ↔ ¬ (card‘𝑦) ∈ ω))
9590, 91, 94mp2b 10 . . . . . . . . . 10 (ω ⊆ (card‘𝑦) ↔ ¬ (card‘𝑦) ∈ ω)
9689, 95sylibr 224 . . . . . . . . 9 ((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) → ω ⊆ (card‘𝑦))
972, 96syl3an2b 1511 . . . . . . . 8 ((Lim 𝐴𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴) → ω ⊆ (card‘𝑦))
98973expb 1114 . . . . . . 7 ((Lim 𝐴 ∧ (𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴)) → ω ⊆ (card‘𝑦))
991, 98sylan2b 493 . . . . . 6 ((Lim 𝐴𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}) → ω ⊆ (card‘𝑦))
10099ralrimiva 3104 . . . . 5 (Lim 𝐴 → ∀𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}ω ⊆ (card‘𝑦))
101 ssiin 4722 . . . . 5 (ω ⊆ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴} (card‘𝑦) ↔ ∀𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}ω ⊆ (card‘𝑦))
102100, 101sylibr 224 . . . 4 (Lim 𝐴 → ω ⊆ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴} (card‘𝑦))
103 cflim2.1 . . . . 5 𝐴 ∈ V
104103cflim3 9276 . . . 4 (Lim 𝐴 → (cf‘𝐴) = 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴} (card‘𝑦))
105102, 104sseqtr4d 3783 . . 3 (Lim 𝐴 → ω ⊆ (cf‘𝐴))
106 fvex 6362 . . . . . . 7 (card‘𝑦) ∈ V
107106dfiin2 4707 . . . . . 6 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴} (card‘𝑦) = {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)}
108104, 107syl6eq 2810 . . . . 5 (Lim 𝐴 → (cf‘𝐴) = {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)})
109 cardlim 8988 . . . . . . . . 9 (ω ⊆ (card‘𝑦) ↔ Lim (card‘𝑦))
110 sseq2 3768 . . . . . . . . . 10 (𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ ω ⊆ (card‘𝑦)))
111 limeq 5896 . . . . . . . . . 10 (𝑥 = (card‘𝑦) → (Lim 𝑥 ↔ Lim (card‘𝑦)))
112110, 111bibi12d 334 . . . . . . . . 9 (𝑥 = (card‘𝑦) → ((ω ⊆ 𝑥 ↔ Lim 𝑥) ↔ (ω ⊆ (card‘𝑦) ↔ Lim (card‘𝑦))))
113109, 112mpbiri 248 . . . . . . . 8 (𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ Lim 𝑥))
114113rexlimivw 3167 . . . . . . 7 (∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ Lim 𝑥))
115114ss2abi 3815 . . . . . 6 {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)}
116 eleq1 2827 . . . . . . . . . 10 (𝑥 = (card‘𝑦) → (𝑥 ∈ On ↔ (card‘𝑦) ∈ On))
11790, 116mpbiri 248 . . . . . . . . 9 (𝑥 = (card‘𝑦) → 𝑥 ∈ On)
118117rexlimivw 3167 . . . . . . . 8 (∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦) → 𝑥 ∈ On)
119118abssi 3818 . . . . . . 7 {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ On
120 fvex 6362 . . . . . . . . 9 (cf‘𝐴) ∈ V
121108, 120syl6eqelr 2848 . . . . . . . 8 (Lim 𝐴 {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ V)
122 intex 4969 . . . . . . . 8 ({𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅ ↔ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ V)
123121, 122sylibr 224 . . . . . . 7 (Lim 𝐴 → {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅)
124 onint 7160 . . . . . . 7 (({𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ On ∧ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅) → {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)})
125119, 123, 124sylancr 698 . . . . . 6 (Lim 𝐴 {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)})
126115, 125sseldi 3742 . . . . 5 (Lim 𝐴 {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)})
127108, 126eqeltrd 2839 . . . 4 (Lim 𝐴 → (cf‘𝐴) ∈ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)})
128 sseq2 3768 . . . . . 6 (𝑥 = (cf‘𝐴) → (ω ⊆ 𝑥 ↔ ω ⊆ (cf‘𝐴)))
129 limeq 5896 . . . . . 6 (𝑥 = (cf‘𝐴) → (Lim 𝑥 ↔ Lim (cf‘𝐴)))
130128, 129bibi12d 334 . . . . 5 (𝑥 = (cf‘𝐴) → ((ω ⊆ 𝑥 ↔ Lim 𝑥) ↔ (ω ⊆ (cf‘𝐴) ↔ Lim (cf‘𝐴))))
131120, 130elab 3490 . . . 4 ((cf‘𝐴) ∈ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)} ↔ (ω ⊆ (cf‘𝐴) ↔ Lim (cf‘𝐴)))
132127, 131sylib 208 . . 3 (Lim 𝐴 → (ω ⊆ (cf‘𝐴) ↔ Lim (cf‘𝐴)))
133105, 132mpbid 222 . 2 (Lim 𝐴 → Lim (cf‘𝐴))
134 eloni 5894 . . . . . . 7 (𝐴 ∈ On → Ord 𝐴)
135 ordzsl 7210 . . . . . . 7 (Ord 𝐴 ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴))
136134, 135sylib 208 . . . . . 6 (𝐴 ∈ On → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴))
137 df-3or 1073 . . . . . . 7 ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴) ↔ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥) ∨ Lim 𝐴))
138 orcom 401 . . . . . . 7 (((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥) ∨ Lim 𝐴) ↔ (Lim 𝐴 ∨ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)))
139 df-or 384 . . . . . . 7 ((Lim 𝐴 ∨ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)) ↔ (¬ Lim 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)))
140137, 138, 1393bitri 286 . . . . . 6 ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴) ↔ (¬ Lim 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)))
141136, 140sylib 208 . . . . 5 (𝐴 ∈ On → (¬ Lim 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)))
142 fveq2 6352 . . . . . . . . 9 (𝐴 = ∅ → (cf‘𝐴) = (cf‘∅))
143 cf0 9265 . . . . . . . . 9 (cf‘∅) = ∅
144142, 143syl6eq 2810 . . . . . . . 8 (𝐴 = ∅ → (cf‘𝐴) = ∅)
145 limeq 5896 . . . . . . . 8 ((cf‘𝐴) = ∅ → (Lim (cf‘𝐴) ↔ Lim ∅))
146144, 145syl 17 . . . . . . 7 (𝐴 = ∅ → (Lim (cf‘𝐴) ↔ Lim ∅))
14779, 146mtbiri 316 . . . . . 6 (𝐴 = ∅ → ¬ Lim (cf‘𝐴))
148 1n0 7744 . . . . . . . . . 10 1𝑜 ≠ ∅
149 df1o2 7741 . . . . . . . . . . . 12 1𝑜 = {∅}
150149unieqi 4597 . . . . . . . . . . 11 1𝑜 = {∅}
151 0ex 4942 . . . . . . . . . . . 12 ∅ ∈ V
152151unisn 4603 . . . . . . . . . . 11 {∅} = ∅
153150, 152eqtri 2782 . . . . . . . . . 10 1𝑜 = ∅
154148, 153neeqtrri 3005 . . . . . . . . 9 1𝑜 1𝑜
155 limuni 5946 . . . . . . . . . 10 (Lim 1𝑜 → 1𝑜 = 1𝑜)
156155necon3ai 2957 . . . . . . . . 9 (1𝑜 1𝑜 → ¬ Lim 1𝑜)
157154, 156ax-mp 5 . . . . . . . 8 ¬ Lim 1𝑜
158 fveq2 6352 . . . . . . . . . 10 (𝐴 = suc 𝑥 → (cf‘𝐴) = (cf‘suc 𝑥))
159 cfsuc 9271 . . . . . . . . . 10 (𝑥 ∈ On → (cf‘suc 𝑥) = 1𝑜)
160158, 159sylan9eqr 2816 . . . . . . . . 9 ((𝑥 ∈ On ∧ 𝐴 = suc 𝑥) → (cf‘𝐴) = 1𝑜)
161 limeq 5896 . . . . . . . . 9 ((cf‘𝐴) = 1𝑜 → (Lim (cf‘𝐴) ↔ Lim 1𝑜))
162160, 161syl 17 . . . . . . . 8 ((𝑥 ∈ On ∧ 𝐴 = suc 𝑥) → (Lim (cf‘𝐴) ↔ Lim 1𝑜))
163157, 162mtbiri 316 . . . . . . 7 ((𝑥 ∈ On ∧ 𝐴 = suc 𝑥) → ¬ Lim (cf‘𝐴))
164163rexlimiva 3166 . . . . . 6 (∃𝑥 ∈ On 𝐴 = suc 𝑥 → ¬ Lim (cf‘𝐴))
165147, 164jaoi 393 . . . . 5 ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥) → ¬ Lim (cf‘𝐴))
166141, 165syl6 35 . . . 4 (𝐴 ∈ On → (¬ Lim 𝐴 → ¬ Lim (cf‘𝐴)))
167166con4d 114 . . 3 (𝐴 ∈ On → (Lim (cf‘𝐴) → Lim 𝐴))
168 cff 9262 . . . . . . . . 9 cf:On⟶On
169168fdmi 6213 . . . . . . . 8 dom cf = On
170169eleq2i 2831 . . . . . . 7 (𝐴 ∈ dom cf ↔ 𝐴 ∈ On)
171 ndmfv 6379 . . . . . . 7 𝐴 ∈ dom cf → (cf‘𝐴) = ∅)
172170, 171sylnbir 320 . . . . . 6 𝐴 ∈ On → (cf‘𝐴) = ∅)
173172, 145syl 17 . . . . 5 𝐴 ∈ On → (Lim (cf‘𝐴) ↔ Lim ∅))
17479, 173mtbiri 316 . . . 4 𝐴 ∈ On → ¬ Lim (cf‘𝐴))
175174pm2.21d 118 . . 3 𝐴 ∈ On → (Lim (cf‘𝐴) → Lim 𝐴))
176167, 175pm2.61i 176 . 2 (Lim (cf‘𝐴) → Lim 𝐴)
177133, 176impbii 199 1 (Lim 𝐴 ↔ Lim (cf‘𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3o 1071  w3a 1072   = wceq 1632  wcel 2139  {cab 2746  wne 2932  wral 3050  wrex 3051  {crab 3054  Vcvv 3340  wss 3715  c0 4058  𝒫 cpw 4302  {csn 4321   cuni 4588   cint 4627   ciin 4673   class class class wbr 4804   E cep 5178   Or wor 5186   Fr wfr 5222   We wwe 5224  ccnv 5265  dom cdm 5266  Ord word 5883  Oncon0 5884  Lim wlim 5885  suc csuc 5886  cfv 6049  ωcom 7230  1𝑜c1o 7722  cen 8118  csdm 8120  Fincfn 8121  cardccrd 8951  cfccf 8953
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-inf2 8711
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-iin 4675  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6774  df-om 7231  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-er 7911  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-card 8955  df-cf 8957
This theorem is referenced by:  cfom  9278
  Copyright terms: Public domain W3C validator