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

Theorem cflim2 10199
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 3427 . . . . . . 7 (𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴} ↔ (𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴))
2 velpw 4565 . . . . . . . . 9 (𝑦 ∈ 𝒫 𝐴𝑦𝐴)
3 limord 6377 . . . . . . . . . . . . . . . . . . . 20 (Lim 𝐴 → Ord 𝐴)
4 ordsson 7717 . . . . . . . . . . . . . . . . . . . 20 (Ord 𝐴𝐴 ⊆ On)
5 sstr 3952 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦𝐴𝐴 ⊆ On) → 𝑦 ⊆ On)
65expcom 414 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ⊆ On → (𝑦𝐴𝑦 ⊆ On))
73, 4, 63syl 18 . . . . . . . . . . . . . . . . . . 19 (Lim 𝐴 → (𝑦𝐴𝑦 ⊆ On))
87imp 407 . . . . . . . . . . . . . . . . . 18 ((Lim 𝐴𝑦𝐴) → 𝑦 ⊆ On)
983adant3 1132 . . . . . . . . . . . . . . . . 17 ((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) → 𝑦 ⊆ On)
10 ssel2 3939 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ⊆ On ∧ 𝑠𝑦) → 𝑠 ∈ On)
11 eloni 6327 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ On → Ord 𝑠)
12 ordirr 6335 . . . . . . . . . . . . . . . . . . 19 (Ord 𝑠 → ¬ 𝑠𝑠)
1310, 11, 123syl 18 . . . . . . . . . . . . . . . . . 18 ((𝑦 ⊆ On ∧ 𝑠𝑦) → ¬ 𝑠𝑠)
14 ssel 3937 . . . . . . . . . . . . . . . . . . . 20 (𝑦𝑠 → (𝑠𝑦𝑠𝑠))
1514com12 32 . . . . . . . . . . . . . . . . . . 19 (𝑠𝑦 → (𝑦𝑠𝑠𝑠))
1615adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝑦 ⊆ On ∧ 𝑠𝑦) → (𝑦𝑠𝑠𝑠))
1713, 16mtod 197 . . . . . . . . . . . . . . . . 17 ((𝑦 ⊆ On ∧ 𝑠𝑦) → ¬ 𝑦𝑠)
189, 17sylan 580 . . . . . . . . . . . . . . . 16 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ 𝑠𝑦) → ¬ 𝑦𝑠)
19 simpl2 1192 . . . . . . . . . . . . . . . . 17 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ 𝑠𝑦) → 𝑦𝐴)
20 sstr 3952 . . . . . . . . . . . . . . . . 17 ((𝑦𝐴𝐴𝑠) → 𝑦𝑠)
2119, 20sylan 580 . . . . . . . . . . . . . . . 16 ((((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ 𝑠𝑦) ∧ 𝐴𝑠) → 𝑦𝑠)
2218, 21mtand 814 . . . . . . . . . . . . . . 15 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ 𝑠𝑦) → ¬ 𝐴𝑠)
23 simpl3 1193 . . . . . . . . . . . . . . . 16 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ 𝑠𝑦) → 𝑦 = 𝐴)
2423sseq1d 3975 . . . . . . . . . . . . . . 15 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ 𝑠𝑦) → ( 𝑦𝑠𝐴𝑠))
2522, 24mtbird 324 . . . . . . . . . . . . . 14 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ 𝑠𝑦) → ¬ 𝑦𝑠)
26 unissb 4900 . . . . . . . . . . . . . 14 ( 𝑦𝑠 ↔ ∀𝑡𝑦 𝑡𝑠)
2725, 26sylnib 327 . . . . . . . . . . . . 13 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ 𝑠𝑦) → ¬ ∀𝑡𝑦 𝑡𝑠)
2827nrexdv 3146 . . . . . . . . . . . 12 ((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) → ¬ ∃𝑠𝑦𝑡𝑦 𝑡𝑠)
29 ssel 3937 . . . . . . . . . . . . . . . . 17 (𝑦 ⊆ On → (𝑠𝑦𝑠 ∈ On))
30 ssel 3937 . . . . . . . . . . . . . . . . 17 (𝑦 ⊆ On → (𝑡𝑦𝑡 ∈ On))
31 ontri1 6351 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ On ∧ 𝑠 ∈ On) → (𝑡𝑠 ↔ ¬ 𝑠𝑡))
3231ancoms 459 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ On ∧ 𝑡 ∈ On) → (𝑡𝑠 ↔ ¬ 𝑠𝑡))
33 vex 3449 . . . . . . . . . . . . . . . . . . . . . 22 𝑡 ∈ V
34 vex 3449 . . . . . . . . . . . . . . . . . . . . . 22 𝑠 ∈ V
3533, 34brcnv 5838 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 E 𝑠𝑠 E 𝑡)
36 epel 5540 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 E 𝑡𝑠𝑡)
3735, 36bitri 274 . . . . . . . . . . . . . . . . . . . 20 (𝑡 E 𝑠𝑠𝑡)
3837notbii 319 . . . . . . . . . . . . . . . . . . 19 𝑡 E 𝑠 ↔ ¬ 𝑠𝑡)
3932, 38bitr4di 288 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ On ∧ 𝑡 ∈ On) → (𝑡𝑠 ↔ ¬ 𝑡 E 𝑠))
4039a1i 11 . . . . . . . . . . . . . . . . 17 (𝑦 ⊆ On → ((𝑠 ∈ On ∧ 𝑡 ∈ On) → (𝑡𝑠 ↔ ¬ 𝑡 E 𝑠)))
4129, 30, 40syl2and 608 . . . . . . . . . . . . . . . 16 (𝑦 ⊆ On → ((𝑠𝑦𝑡𝑦) → (𝑡𝑠 ↔ ¬ 𝑡 E 𝑠)))
4241impl 456 . . . . . . . . . . . . . . 15 (((𝑦 ⊆ On ∧ 𝑠𝑦) ∧ 𝑡𝑦) → (𝑡𝑠 ↔ ¬ 𝑡 E 𝑠))
4342ralbidva 3172 . . . . . . . . . . . . . 14 ((𝑦 ⊆ On ∧ 𝑠𝑦) → (∀𝑡𝑦 𝑡𝑠 ↔ ∀𝑡𝑦 ¬ 𝑡 E 𝑠))
4443rexbidva 3173 . . . . . . . . . . . . 13 (𝑦 ⊆ On → (∃𝑠𝑦𝑡𝑦 𝑡𝑠 ↔ ∃𝑠𝑦𝑡𝑦 ¬ 𝑡 E 𝑠))
459, 44syl 17 . . . . . . . . . . . 12 ((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) → (∃𝑠𝑦𝑡𝑦 𝑡𝑠 ↔ ∃𝑠𝑦𝑡𝑦 ¬ 𝑡 E 𝑠))
4628, 45mtbid 323 . . . . . . . . . . 11 ((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) → ¬ ∃𝑠𝑦𝑡𝑦 ¬ 𝑡 E 𝑠)
47 vex 3449 . . . . . . . . . . . . 13 𝑦 ∈ V
4847a1i 11 . . . . . . . . . . . 12 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦 ∈ V)
49 epweon 7709 . . . . . . . . . . . . . . . . . 18 E We On
50 wess 5620 . . . . . . . . . . . . . . . . . 18 (𝑦 ⊆ On → ( E We On → E We 𝑦))
5149, 50mpi 20 . . . . . . . . . . . . . . . . 17 (𝑦 ⊆ On → E We 𝑦)
52 weso 5624 . . . . . . . . . . . . . . . . 17 ( E We 𝑦 → E Or 𝑦)
5351, 52syl 17 . . . . . . . . . . . . . . . 16 (𝑦 ⊆ On → E Or 𝑦)
54 cnvso 6240 . . . . . . . . . . . . . . . 16 ( E Or 𝑦 E Or 𝑦)
5553, 54sylib 217 . . . . . . . . . . . . . . 15 (𝑦 ⊆ On → E Or 𝑦)
56 onssnum 9976 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ V ∧ 𝑦 ⊆ On) → 𝑦 ∈ dom card)
5747, 56mpan 688 . . . . . . . . . . . . . . . . . 18 (𝑦 ⊆ On → 𝑦 ∈ dom card)
58 cardid2 9889 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ dom card → (card‘𝑦) ≈ 𝑦)
59 ensym 8943 . . . . . . . . . . . . . . . . . 18 ((card‘𝑦) ≈ 𝑦𝑦 ≈ (card‘𝑦))
6057, 58, 593syl 18 . . . . . . . . . . . . . . . . 17 (𝑦 ⊆ On → 𝑦 ≈ (card‘𝑦))
61 nnsdom 9590 . . . . . . . . . . . . . . . . 17 ((card‘𝑦) ∈ ω → (card‘𝑦) ≺ ω)
62 ensdomtr 9057 . . . . . . . . . . . . . . . . 17 ((𝑦 ≈ (card‘𝑦) ∧ (card‘𝑦) ≺ ω) → 𝑦 ≺ ω)
6360, 61, 62syl2an 596 . . . . . . . . . . . . . . . 16 ((𝑦 ⊆ On ∧ (card‘𝑦) ∈ ω) → 𝑦 ≺ ω)
64 isfinite 9588 . . . . . . . . . . . . . . . 16 (𝑦 ∈ Fin ↔ 𝑦 ≺ ω)
6563, 64sylibr 233 . . . . . . . . . . . . . . 15 ((𝑦 ⊆ On ∧ (card‘𝑦) ∈ ω) → 𝑦 ∈ Fin)
66 wofi 9236 . . . . . . . . . . . . . . 15 (( E Or 𝑦𝑦 ∈ Fin) → E We 𝑦)
6755, 65, 66syl2an2r 683 . . . . . . . . . . . . . 14 ((𝑦 ⊆ On ∧ (card‘𝑦) ∈ ω) → E We 𝑦)
689, 67sylan 580 . . . . . . . . . . . . 13 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → E We 𝑦)
69 wefr 5623 . . . . . . . . . . . . 13 ( E We 𝑦 E Fr 𝑦)
7068, 69syl 17 . . . . . . . . . . . 12 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → E Fr 𝑦)
71 ssidd 3967 . . . . . . . . . . . 12 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦𝑦)
72 unieq 4876 . . . . . . . . . . . . . . . . . . 19 (𝑦 = ∅ → 𝑦 = ∅)
73 uni0 4896 . . . . . . . . . . . . . . . . . . 19 ∅ = ∅
7472, 73eqtrdi 2792 . . . . . . . . . . . . . . . . . 18 (𝑦 = ∅ → 𝑦 = ∅)
75 eqeq1 2740 . . . . . . . . . . . . . . . . . 18 ( 𝑦 = 𝐴 → ( 𝑦 = ∅ ↔ 𝐴 = ∅))
7674, 75imbitrid 243 . . . . . . . . . . . . . . . . 17 ( 𝑦 = 𝐴 → (𝑦 = ∅ → 𝐴 = ∅))
77 nlim0 6376 . . . . . . . . . . . . . . . . . 18 ¬ Lim ∅
78 limeq 6329 . . . . . . . . . . . . . . . . . 18 (𝐴 = ∅ → (Lim 𝐴 ↔ Lim ∅))
7977, 78mtbiri 326 . . . . . . . . . . . . . . . . 17 (𝐴 = ∅ → ¬ Lim 𝐴)
8076, 79syl6 35 . . . . . . . . . . . . . . . 16 ( 𝑦 = 𝐴 → (𝑦 = ∅ → ¬ Lim 𝐴))
8180necon2ad 2958 . . . . . . . . . . . . . . 15 ( 𝑦 = 𝐴 → (Lim 𝐴𝑦 ≠ ∅))
8281impcom 408 . . . . . . . . . . . . . 14 ((Lim 𝐴 𝑦 = 𝐴) → 𝑦 ≠ ∅)
83823adant2 1131 . . . . . . . . . . . . 13 ((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) → 𝑦 ≠ ∅)
8483adantr 481 . . . . . . . . . . . 12 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦 ≠ ∅)
85 fri 5593 . . . . . . . . . . . 12 (((𝑦 ∈ V ∧ E Fr 𝑦) ∧ (𝑦𝑦𝑦 ≠ ∅)) → ∃𝑠𝑦𝑡𝑦 ¬ 𝑡 E 𝑠)
8648, 70, 71, 84, 85syl22anc 837 . . . . . . . . . . 11 (((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → ∃𝑠𝑦𝑡𝑦 ¬ 𝑡 E 𝑠)
8746, 86mtand 814 . . . . . . . . . 10 ((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) → ¬ (card‘𝑦) ∈ ω)
88 cardon 9880 . . . . . . . . . . 11 (card‘𝑦) ∈ On
89 eloni 6327 . . . . . . . . . . 11 ((card‘𝑦) ∈ On → Ord (card‘𝑦))
90 ordom 7812 . . . . . . . . . . . 12 Ord ω
91 ordtri1 6350 . . . . . . . . . . . 12 ((Ord ω ∧ Ord (card‘𝑦)) → (ω ⊆ (card‘𝑦) ↔ ¬ (card‘𝑦) ∈ ω))
9290, 91mpan 688 . . . . . . . . . . 11 (Ord (card‘𝑦) → (ω ⊆ (card‘𝑦) ↔ ¬ (card‘𝑦) ∈ ω))
9388, 89, 92mp2b 10 . . . . . . . . . 10 (ω ⊆ (card‘𝑦) ↔ ¬ (card‘𝑦) ∈ ω)
9487, 93sylibr 233 . . . . . . . . 9 ((Lim 𝐴𝑦𝐴 𝑦 = 𝐴) → ω ⊆ (card‘𝑦))
952, 94syl3an2b 1404 . . . . . . . 8 ((Lim 𝐴𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴) → ω ⊆ (card‘𝑦))
96953expb 1120 . . . . . . 7 ((Lim 𝐴 ∧ (𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴)) → ω ⊆ (card‘𝑦))
971, 96sylan2b 594 . . . . . 6 ((Lim 𝐴𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}) → ω ⊆ (card‘𝑦))
9897ralrimiva 3143 . . . . 5 (Lim 𝐴 → ∀𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}ω ⊆ (card‘𝑦))
99 ssiin 5015 . . . . 5 (ω ⊆ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴} (card‘𝑦) ↔ ∀𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}ω ⊆ (card‘𝑦))
10098, 99sylibr 233 . . . 4 (Lim 𝐴 → ω ⊆ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴} (card‘𝑦))
101 cflim2.1 . . . . 5 𝐴 ∈ V
102101cflim3 10198 . . . 4 (Lim 𝐴 → (cf‘𝐴) = 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴} (card‘𝑦))
103100, 102sseqtrrd 3985 . . 3 (Lim 𝐴 → ω ⊆ (cf‘𝐴))
104 fvex 6855 . . . . . . 7 (card‘𝑦) ∈ V
105104dfiin2 4994 . . . . . 6 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴} (card‘𝑦) = {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)}
106102, 105eqtrdi 2792 . . . . 5 (Lim 𝐴 → (cf‘𝐴) = {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)})
107 cardlim 9908 . . . . . . . . 9 (ω ⊆ (card‘𝑦) ↔ Lim (card‘𝑦))
108 sseq2 3970 . . . . . . . . . 10 (𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ ω ⊆ (card‘𝑦)))
109 limeq 6329 . . . . . . . . . 10 (𝑥 = (card‘𝑦) → (Lim 𝑥 ↔ Lim (card‘𝑦)))
110108, 109bibi12d 345 . . . . . . . . 9 (𝑥 = (card‘𝑦) → ((ω ⊆ 𝑥 ↔ Lim 𝑥) ↔ (ω ⊆ (card‘𝑦) ↔ Lim (card‘𝑦))))
111107, 110mpbiri 257 . . . . . . . 8 (𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ Lim 𝑥))
112111rexlimivw 3148 . . . . . . 7 (∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ Lim 𝑥))
113112ss2abi 4023 . . . . . 6 {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)}
114 eleq1 2825 . . . . . . . . . 10 (𝑥 = (card‘𝑦) → (𝑥 ∈ On ↔ (card‘𝑦) ∈ On))
11588, 114mpbiri 257 . . . . . . . . 9 (𝑥 = (card‘𝑦) → 𝑥 ∈ On)
116115rexlimivw 3148 . . . . . . . 8 (∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦) → 𝑥 ∈ On)
117116abssi 4027 . . . . . . 7 {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ On
118 fvex 6855 . . . . . . . . 9 (cf‘𝐴) ∈ V
119106, 118eqeltrrdi 2847 . . . . . . . 8 (Lim 𝐴 {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ V)
120 intex 5294 . . . . . . . 8 ({𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅ ↔ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ V)
121119, 120sylibr 233 . . . . . . 7 (Lim 𝐴 → {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅)
122 onint 7725 . . . . . . 7 (({𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ On ∧ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅) → {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)})
123117, 121, 122sylancr 587 . . . . . 6 (Lim 𝐴 {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)})
124113, 123sselid 3942 . . . . 5 (Lim 𝐴 {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)})
125106, 124eqeltrd 2838 . . . 4 (Lim 𝐴 → (cf‘𝐴) ∈ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)})
126 sseq2 3970 . . . . . 6 (𝑥 = (cf‘𝐴) → (ω ⊆ 𝑥 ↔ ω ⊆ (cf‘𝐴)))
127 limeq 6329 . . . . . 6 (𝑥 = (cf‘𝐴) → (Lim 𝑥 ↔ Lim (cf‘𝐴)))
128126, 127bibi12d 345 . . . . 5 (𝑥 = (cf‘𝐴) → ((ω ⊆ 𝑥 ↔ Lim 𝑥) ↔ (ω ⊆ (cf‘𝐴) ↔ Lim (cf‘𝐴))))
129118, 128elab 3630 . . . 4 ((cf‘𝐴) ∈ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)} ↔ (ω ⊆ (cf‘𝐴) ↔ Lim (cf‘𝐴)))
130125, 129sylib 217 . . 3 (Lim 𝐴 → (ω ⊆ (cf‘𝐴) ↔ Lim (cf‘𝐴)))
131103, 130mpbid 231 . 2 (Lim 𝐴 → Lim (cf‘𝐴))
132 eloni 6327 . . . . . . 7 (𝐴 ∈ On → Ord 𝐴)
133 ordzsl 7781 . . . . . . 7 (Ord 𝐴 ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴))
134132, 133sylib 217 . . . . . 6 (𝐴 ∈ On → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴))
135 df-3or 1088 . . . . . . 7 ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴) ↔ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥) ∨ Lim 𝐴))
136 orcom 868 . . . . . . 7 (((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥) ∨ Lim 𝐴) ↔ (Lim 𝐴 ∨ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)))
137 df-or 846 . . . . . . 7 ((Lim 𝐴 ∨ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)) ↔ (¬ Lim 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)))
138135, 136, 1373bitri 296 . . . . . 6 ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴) ↔ (¬ Lim 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)))
139134, 138sylib 217 . . . . 5 (𝐴 ∈ On → (¬ Lim 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)))
140 fveq2 6842 . . . . . . . . 9 (𝐴 = ∅ → (cf‘𝐴) = (cf‘∅))
141 cf0 10187 . . . . . . . . 9 (cf‘∅) = ∅
142140, 141eqtrdi 2792 . . . . . . . 8 (𝐴 = ∅ → (cf‘𝐴) = ∅)
143 limeq 6329 . . . . . . . 8 ((cf‘𝐴) = ∅ → (Lim (cf‘𝐴) ↔ Lim ∅))
144142, 143syl 17 . . . . . . 7 (𝐴 = ∅ → (Lim (cf‘𝐴) ↔ Lim ∅))
14577, 144mtbiri 326 . . . . . 6 (𝐴 = ∅ → ¬ Lim (cf‘𝐴))
146 1n0 8434 . . . . . . . . . 10 1o ≠ ∅
147 df1o2 8419 . . . . . . . . . . . 12 1o = {∅}
148147unieqi 4878 . . . . . . . . . . 11 1o = {∅}
149 0ex 5264 . . . . . . . . . . . 12 ∅ ∈ V
150149unisn 4887 . . . . . . . . . . 11 {∅} = ∅
151148, 150eqtri 2764 . . . . . . . . . 10 1o = ∅
152146, 151neeqtrri 3017 . . . . . . . . 9 1o 1o
153 limuni 6378 . . . . . . . . . 10 (Lim 1o → 1o = 1o)
154153necon3ai 2968 . . . . . . . . 9 (1o 1o → ¬ Lim 1o)
155152, 154ax-mp 5 . . . . . . . 8 ¬ Lim 1o
156 fveq2 6842 . . . . . . . . . 10 (𝐴 = suc 𝑥 → (cf‘𝐴) = (cf‘suc 𝑥))
157 cfsuc 10193 . . . . . . . . . 10 (𝑥 ∈ On → (cf‘suc 𝑥) = 1o)
158156, 157sylan9eqr 2798 . . . . . . . . 9 ((𝑥 ∈ On ∧ 𝐴 = suc 𝑥) → (cf‘𝐴) = 1o)
159 limeq 6329 . . . . . . . . 9 ((cf‘𝐴) = 1o → (Lim (cf‘𝐴) ↔ Lim 1o))
160158, 159syl 17 . . . . . . . 8 ((𝑥 ∈ On ∧ 𝐴 = suc 𝑥) → (Lim (cf‘𝐴) ↔ Lim 1o))
161155, 160mtbiri 326 . . . . . . 7 ((𝑥 ∈ On ∧ 𝐴 = suc 𝑥) → ¬ Lim (cf‘𝐴))
162161rexlimiva 3144 . . . . . 6 (∃𝑥 ∈ On 𝐴 = suc 𝑥 → ¬ Lim (cf‘𝐴))
163145, 162jaoi 855 . . . . 5 ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥) → ¬ Lim (cf‘𝐴))
164139, 163syl6 35 . . . 4 (𝐴 ∈ On → (¬ Lim 𝐴 → ¬ Lim (cf‘𝐴)))
165164con4d 115 . . 3 (𝐴 ∈ On → (Lim (cf‘𝐴) → Lim 𝐴))
166 cff 10184 . . . . . . . . 9 cf:On⟶On
167166fdmi 6680 . . . . . . . 8 dom cf = On
168167eleq2i 2829 . . . . . . 7 (𝐴 ∈ dom cf ↔ 𝐴 ∈ On)
169 ndmfv 6877 . . . . . . 7 𝐴 ∈ dom cf → (cf‘𝐴) = ∅)
170168, 169sylnbir 330 . . . . . 6 𝐴 ∈ On → (cf‘𝐴) = ∅)
171170, 143syl 17 . . . . 5 𝐴 ∈ On → (Lim (cf‘𝐴) ↔ Lim ∅))
17277, 171mtbiri 326 . . . 4 𝐴 ∈ On → ¬ Lim (cf‘𝐴))
173172pm2.21d 121 . . 3 𝐴 ∈ On → (Lim (cf‘𝐴) → Lim 𝐴))
174165, 173pm2.61i 182 . 2 (Lim (cf‘𝐴) → Lim 𝐴)
175131, 174impbii 208 1 (Lim 𝐴 ↔ Lim (cf‘𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3o 1086  w3a 1087   = wceq 1541  wcel 2106  {cab 2713  wne 2943  wral 3064  wrex 3073  {crab 3407  Vcvv 3445  wss 3910  c0 4282  𝒫 cpw 4560  {csn 4586   cuni 4865   cint 4907   ciin 4955   class class class wbr 5105   E cep 5536   Or wor 5544   Fr wfr 5585   We wwe 5587  ccnv 5632  dom cdm 5633  Ord word 6316  Oncon0 6317  Lim wlim 6318  suc csuc 6319  cfv 6496  ωcom 7802  1oc1o 8405  cen 8880  csdm 8882  Fincfn 8883  cardccrd 9871  cfccf 9873
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  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 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-om 7803  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-card 9875  df-cf 9877
This theorem is referenced by:  cfom  10200
  Copyright terms: Public domain W3C validator