MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cflim2 Structured version   Visualization version   GIF version
Theorem cflim2 10258
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 3453 . . . . . . 7 (𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴} ↔ (𝑦 ∈ 𝒫 𝐴 ∧ βˆͺ 𝑦 = 𝐴))
2 velpw 4608 . . . . . . . . 9 (𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 βŠ† 𝐴)
3 limord 6425 . . . . . . . . . . . . . . . . . . . 20 (Lim 𝐴 β†’ Ord 𝐴)
4 ordsson 7770 . . . . . . . . . . . . . . . . . . . 20 (Ord 𝐴 β†’ 𝐴 βŠ† On)
5 sstr 3991 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 βŠ† 𝐴 ∧ 𝐴 βŠ† On) β†’ 𝑦 βŠ† On)
65expcom 415 . . . . . . . . . . . . . . . . . . . 20 (𝐴 βŠ† On β†’ (𝑦 βŠ† 𝐴 β†’ 𝑦 βŠ† On))
73, 4, 63syl 18 . . . . . . . . . . . . . . . . . . 19 (Lim 𝐴 β†’ (𝑦 βŠ† 𝐴 β†’ 𝑦 βŠ† On))
87imp 408 . . . . . . . . . . . . . . . . . 18 ((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴) β†’ 𝑦 βŠ† On)
983adant3 1133 . . . . . . . . . . . . . . . . 17 ((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) β†’ 𝑦 βŠ† On)
10 ssel2 3978 . . . . . . . . . . . . . . . . . . 19 ((𝑦 βŠ† On ∧ 𝑠 ∈ 𝑦) β†’ 𝑠 ∈ On)
11 eloni 6375 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ On β†’ Ord 𝑠)
12 ordirr 6383 . . . . . . . . . . . . . . . . . . 19 (Ord 𝑠 β†’ Β¬ 𝑠 ∈ 𝑠)
1310, 11, 123syl 18 . . . . . . . . . . . . . . . . . 18 ((𝑦 βŠ† On ∧ 𝑠 ∈ 𝑦) β†’ Β¬ 𝑠 ∈ 𝑠)
14 ssel 3976 . . . . . . . . . . . . . . . . . . . 20 (𝑦 βŠ† 𝑠 β†’ (𝑠 ∈ 𝑦 β†’ 𝑠 ∈ 𝑠))
1514com12 32 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ 𝑦 β†’ (𝑦 βŠ† 𝑠 β†’ 𝑠 ∈ 𝑠))
1615adantl 483 . . . . . . . . . . . . . . . . . 18 ((𝑦 βŠ† On ∧ 𝑠 ∈ 𝑦) β†’ (𝑦 βŠ† 𝑠 β†’ 𝑠 ∈ 𝑠))
1713, 16mtod 197 . . . . . . . . . . . . . . . . 17 ((𝑦 βŠ† On ∧ 𝑠 ∈ 𝑦) β†’ Β¬ 𝑦 βŠ† 𝑠)
189, 17sylan 581 . . . . . . . . . . . . . . . 16 (((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) β†’ Β¬ 𝑦 βŠ† 𝑠)
19 simpl2 1193 . . . . . . . . . . . . . . . . 17 (((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) β†’ 𝑦 βŠ† 𝐴)
20 sstr 3991 . . . . . . . . . . . . . . . . 17 ((𝑦 βŠ† 𝐴 ∧ 𝐴 βŠ† 𝑠) β†’ 𝑦 βŠ† 𝑠)
2119, 20sylan 581 . . . . . . . . . . . . . . . 16 ((((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) ∧ 𝐴 βŠ† 𝑠) β†’ 𝑦 βŠ† 𝑠)
2218, 21mtand 815 . . . . . . . . . . . . . . 15 (((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) β†’ Β¬ 𝐴 βŠ† 𝑠)
23 simpl3 1194 . . . . . . . . . . . . . . . 16 (((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) β†’ βˆͺ 𝑦 = 𝐴)
2423sseq1d 4014 . . . . . . . . . . . . . . 15 (((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) β†’ (βˆͺ 𝑦 βŠ† 𝑠 ↔ 𝐴 βŠ† 𝑠))
2522, 24mtbird 325 . . . . . . . . . . . . . 14 (((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) β†’ Β¬ βˆͺ 𝑦 βŠ† 𝑠)
26 unissb 4944 . . . . . . . . . . . . . 14 (βˆͺ 𝑦 βŠ† 𝑠 ↔ βˆ€π‘‘ ∈ 𝑦 𝑑 βŠ† 𝑠)
2725, 26sylnib 328 . . . . . . . . . . . . 13 (((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) β†’ Β¬ βˆ€π‘‘ ∈ 𝑦 𝑑 βŠ† 𝑠)
2827nrexdv 3150 . . . . . . . . . . . 12 ((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) β†’ Β¬ βˆƒπ‘  ∈ 𝑦 βˆ€π‘‘ ∈ 𝑦 𝑑 βŠ† 𝑠)
29 ssel 3976 . . . . . . . . . . . . . . . . 17 (𝑦 βŠ† On β†’ (𝑠 ∈ 𝑦 β†’ 𝑠 ∈ On))
30 ssel 3976 . . . . . . . . . . . . . . . . 17 (𝑦 βŠ† On β†’ (𝑑 ∈ 𝑦 β†’ 𝑑 ∈ On))
31 ontri1 6399 . . . . . . . . . . . . . . . . . . . 20 ((𝑑 ∈ On ∧ 𝑠 ∈ On) β†’ (𝑑 βŠ† 𝑠 ↔ Β¬ 𝑠 ∈ 𝑑))
3231ancoms 460 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ On ∧ 𝑑 ∈ On) β†’ (𝑑 βŠ† 𝑠 ↔ Β¬ 𝑠 ∈ 𝑑))
33 vex 3479 . . . . . . . . . . . . . . . . . . . . . 22 𝑑 ∈ V
34 vex 3479 . . . . . . . . . . . . . . . . . . . . . 22 𝑠 ∈ V
3533, 34brcnv 5883 . . . . . . . . . . . . . . . . . . . . 21 (𝑑◑ E 𝑠 ↔ 𝑠 E 𝑑)
36 epel 5584 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 E 𝑑 ↔ 𝑠 ∈ 𝑑)
3735, 36bitri 275 . . . . . . . . . . . . . . . . . . . 20 (𝑑◑ E 𝑠 ↔ 𝑠 ∈ 𝑑)
3837notbii 320 . . . . . . . . . . . . . . . . . . 19 (Β¬ 𝑑◑ E 𝑠 ↔ Β¬ 𝑠 ∈ 𝑑)
3932, 38bitr4di 289 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ On ∧ 𝑑 ∈ On) β†’ (𝑑 βŠ† 𝑠 ↔ Β¬ 𝑑◑ E 𝑠))
4039a1i 11 . . . . . . . . . . . . . . . . 17 (𝑦 βŠ† On β†’ ((𝑠 ∈ On ∧ 𝑑 ∈ On) β†’ (𝑑 βŠ† 𝑠 ↔ Β¬ 𝑑◑ E 𝑠)))
4129, 30, 40syl2and 609 . . . . . . . . . . . . . . . 16 (𝑦 βŠ† On β†’ ((𝑠 ∈ 𝑦 ∧ 𝑑 ∈ 𝑦) β†’ (𝑑 βŠ† 𝑠 ↔ Β¬ 𝑑◑ E 𝑠)))
4241impl 457 . . . . . . . . . . . . . . 15 (((𝑦 βŠ† On ∧ 𝑠 ∈ 𝑦) ∧ 𝑑 ∈ 𝑦) β†’ (𝑑 βŠ† 𝑠 ↔ Β¬ 𝑑◑ E 𝑠))
4342ralbidva 3176 . . . . . . . . . . . . . 14 ((𝑦 βŠ† On ∧ 𝑠 ∈ 𝑦) β†’ (βˆ€π‘‘ ∈ 𝑦 𝑑 βŠ† 𝑠 ↔ βˆ€π‘‘ ∈ 𝑦 Β¬ 𝑑◑ E 𝑠))
4443rexbidva 3177 . . . . . . . . . . . . 13 (𝑦 βŠ† On β†’ (βˆƒπ‘  ∈ 𝑦 βˆ€π‘‘ ∈ 𝑦 𝑑 βŠ† 𝑠 ↔ βˆƒπ‘  ∈ 𝑦 βˆ€π‘‘ ∈ 𝑦 Β¬ 𝑑◑ E 𝑠))
459, 44syl 17 . . . . . . . . . . . 12 ((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) β†’ (βˆƒπ‘  ∈ 𝑦 βˆ€π‘‘ ∈ 𝑦 𝑑 βŠ† 𝑠 ↔ βˆƒπ‘  ∈ 𝑦 βˆ€π‘‘ ∈ 𝑦 Β¬ 𝑑◑ E 𝑠))
4628, 45mtbid 324 . . . . . . . . . . 11 ((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) β†’ Β¬ βˆƒπ‘  ∈ 𝑦 βˆ€π‘‘ ∈ 𝑦 Β¬ 𝑑◑ E 𝑠)
47 vex 3479 . . . . . . . . . . . . 13 𝑦 ∈ V
4847a1i 11 . . . . . . . . . . . 12 (((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) ∧ (cardβ€˜π‘¦) ∈ Ο‰) β†’ 𝑦 ∈ V)
49 epweon 7762 . . . . . . . . . . . . . . . . . 18 E We On
50 wess 5664 . . . . . . . . . . . . . . . . . 18 (𝑦 βŠ† On β†’ ( E We On β†’ E We 𝑦))
5149, 50mpi 20 . . . . . . . . . . . . . . . . 17 (𝑦 βŠ† On β†’ E We 𝑦)
52 weso 5668 . . . . . . . . . . . . . . . . 17 ( E We 𝑦 β†’ E Or 𝑦)
5351, 52syl 17 . . . . . . . . . . . . . . . 16 (𝑦 βŠ† On β†’ E Or 𝑦)
54 cnvso 6288 . . . . . . . . . . . . . . . 16 ( E Or 𝑦 ↔ β—‘ E Or 𝑦)
5553, 54sylib 217 . . . . . . . . . . . . . . 15 (𝑦 βŠ† On β†’ β—‘ E Or 𝑦)
56 onssnum 10035 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ V ∧ 𝑦 βŠ† On) β†’ 𝑦 ∈ dom card)
5747, 56mpan 689 . . . . . . . . . . . . . . . . . 18 (𝑦 βŠ† On β†’ 𝑦 ∈ dom card)
58 cardid2 9948 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ dom card β†’ (cardβ€˜π‘¦) β‰ˆ 𝑦)
59 ensym 8999 . . . . . . . . . . . . . . . . . 18 ((cardβ€˜π‘¦) β‰ˆ 𝑦 β†’ 𝑦 β‰ˆ (cardβ€˜π‘¦))
6057, 58, 593syl 18 . . . . . . . . . . . . . . . . 17 (𝑦 βŠ† On β†’ 𝑦 β‰ˆ (cardβ€˜π‘¦))
61 nnsdom 9649 . . . . . . . . . . . . . . . . 17 ((cardβ€˜π‘¦) ∈ Ο‰ β†’ (cardβ€˜π‘¦) β‰Ί Ο‰)
62 ensdomtr 9113 . . . . . . . . . . . . . . . . 17 ((𝑦 β‰ˆ (cardβ€˜π‘¦) ∧ (cardβ€˜π‘¦) β‰Ί Ο‰) β†’ 𝑦 β‰Ί Ο‰)
6360, 61, 62syl2an 597 . . . . . . . . . . . . . . . 16 ((𝑦 βŠ† On ∧ (cardβ€˜π‘¦) ∈ Ο‰) β†’ 𝑦 β‰Ί Ο‰)
64 isfinite 9647 . . . . . . . . . . . . . . . 16 (𝑦 ∈ Fin ↔ 𝑦 β‰Ί Ο‰)
6563, 64sylibr 233 . . . . . . . . . . . . . . 15 ((𝑦 βŠ† On ∧ (cardβ€˜π‘¦) ∈ Ο‰) β†’ 𝑦 ∈ Fin)
66 wofi 9292 . . . . . . . . . . . . . . 15 ((β—‘ E Or 𝑦 ∧ 𝑦 ∈ Fin) β†’ β—‘ E We 𝑦)
6755, 65, 66syl2an2r 684 . . . . . . . . . . . . . 14 ((𝑦 βŠ† On ∧ (cardβ€˜π‘¦) ∈ Ο‰) β†’ β—‘ E We 𝑦)
689, 67sylan 581 . . . . . . . . . . . . 13 (((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) ∧ (cardβ€˜π‘¦) ∈ Ο‰) β†’ β—‘ E We 𝑦)
69 wefr 5667 . . . . . . . . . . . . 13 (β—‘ E We 𝑦 β†’ β—‘ E Fr 𝑦)
7068, 69syl 17 . . . . . . . . . . . 12 (((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) ∧ (cardβ€˜π‘¦) ∈ Ο‰) β†’ β—‘ E Fr 𝑦)
71 ssidd 4006 . . . . . . . . . . . 12 (((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) ∧ (cardβ€˜π‘¦) ∈ Ο‰) β†’ 𝑦 βŠ† 𝑦)
72 unieq 4920 . . . . . . . . . . . . . . . . . . 19 (𝑦 = βˆ… β†’ βˆͺ 𝑦 = βˆͺ βˆ…)
73 uni0 4940 . . . . . . . . . . . . . . . . . . 19 βˆͺ βˆ… = βˆ…
7472, 73eqtrdi 2789 . . . . . . . . . . . . . . . . . 18 (𝑦 = βˆ… β†’ βˆͺ 𝑦 = βˆ…)
75 eqeq1 2737 . . . . . . . . . . . . . . . . . 18 (βˆͺ 𝑦 = 𝐴 β†’ (βˆͺ 𝑦 = βˆ… ↔ 𝐴 = βˆ…))
7674, 75imbitrid 243 . . . . . . . . . . . . . . . . 17 (βˆͺ 𝑦 = 𝐴 β†’ (𝑦 = βˆ… β†’ 𝐴 = βˆ…))
77 nlim0 6424 . . . . . . . . . . . . . . . . . 18 Β¬ Lim βˆ…
78 limeq 6377 . . . . . . . . . . . . . . . . . 18 (𝐴 = βˆ… β†’ (Lim 𝐴 ↔ Lim βˆ…))
7977, 78mtbiri 327 . . . . . . . . . . . . . . . . 17 (𝐴 = βˆ… β†’ Β¬ Lim 𝐴)
8076, 79syl6 35 . . . . . . . . . . . . . . . 16 (βˆͺ 𝑦 = 𝐴 β†’ (𝑦 = βˆ… β†’ Β¬ Lim 𝐴))
8180necon2ad 2956 . . . . . . . . . . . . . . 15 (βˆͺ 𝑦 = 𝐴 β†’ (Lim 𝐴 β†’ 𝑦 β‰  βˆ…))
8281impcom 409 . . . . . . . . . . . . . 14 ((Lim 𝐴 ∧ βˆͺ 𝑦 = 𝐴) β†’ 𝑦 β‰  βˆ…)
83823adant2 1132 . . . . . . . . . . . . 13 ((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) β†’ 𝑦 β‰  βˆ…)
8483adantr 482 . . . . . . . . . . . 12 (((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) ∧ (cardβ€˜π‘¦) ∈ Ο‰) β†’ 𝑦 β‰  βˆ…)
85 fri 5637 . . . . . . . . . . . 12 (((𝑦 ∈ V ∧ β—‘ E Fr 𝑦) ∧ (𝑦 βŠ† 𝑦 ∧ 𝑦 β‰  βˆ…)) β†’ βˆƒπ‘  ∈ 𝑦 βˆ€π‘‘ ∈ 𝑦 Β¬ 𝑑◑ E 𝑠)
8648, 70, 71, 84, 85syl22anc 838 . . . . . . . . . . 11 (((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) ∧ (cardβ€˜π‘¦) ∈ Ο‰) β†’ βˆƒπ‘  ∈ 𝑦 βˆ€π‘‘ ∈ 𝑦 Β¬ 𝑑◑ E 𝑠)
8746, 86mtand 815 . . . . . . . . . 10 ((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) β†’ Β¬ (cardβ€˜π‘¦) ∈ Ο‰)
88 cardon 9939 . . . . . . . . . . 11 (cardβ€˜π‘¦) ∈ On
89 eloni 6375 . . . . . . . . . . 11 ((cardβ€˜π‘¦) ∈ On β†’ Ord (cardβ€˜π‘¦))
90 ordom 7865 . . . . . . . . . . . 12 Ord Ο‰
91 ordtri1 6398 . . . . . . . . . . . 12 ((Ord Ο‰ ∧ Ord (cardβ€˜π‘¦)) β†’ (Ο‰ βŠ† (cardβ€˜π‘¦) ↔ Β¬ (cardβ€˜π‘¦) ∈ Ο‰))
9290, 91mpan 689 . . . . . . . . . . 11 (Ord (cardβ€˜π‘¦) β†’ (Ο‰ βŠ† (cardβ€˜π‘¦) ↔ Β¬ (cardβ€˜π‘¦) ∈ Ο‰))
9388, 89, 92mp2b 10 . . . . . . . . . 10 (Ο‰ βŠ† (cardβ€˜π‘¦) ↔ Β¬ (cardβ€˜π‘¦) ∈ Ο‰)
9487, 93sylibr 233 . . . . . . . . 9 ((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) β†’ Ο‰ βŠ† (cardβ€˜π‘¦))
952, 94syl3an2b 1405 . . . . . . . 8 ((Lim 𝐴 ∧ 𝑦 ∈ 𝒫 𝐴 ∧ βˆͺ 𝑦 = 𝐴) β†’ Ο‰ βŠ† (cardβ€˜π‘¦))
96953expb 1121 . . . . . . 7 ((Lim 𝐴 ∧ (𝑦 ∈ 𝒫 𝐴 ∧ βˆͺ 𝑦 = 𝐴)) β†’ Ο‰ βŠ† (cardβ€˜π‘¦))
971, 96sylan2b 595 . . . . . 6 ((Lim 𝐴 ∧ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}) β†’ Ο‰ βŠ† (cardβ€˜π‘¦))
9897ralrimiva 3147 . . . . 5 (Lim 𝐴 β†’ βˆ€π‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}Ο‰ βŠ† (cardβ€˜π‘¦))
99 ssiin 5059 . . . . 5 (Ο‰ βŠ† ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴} (cardβ€˜π‘¦) ↔ βˆ€π‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}Ο‰ βŠ† (cardβ€˜π‘¦))
10098, 99sylibr 233 . . . 4 (Lim 𝐴 β†’ Ο‰ βŠ† ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴} (cardβ€˜π‘¦))
101 cflim2.1 . . . . 5 𝐴 ∈ V
102101cflim3 10257 . . . 4 (Lim 𝐴 β†’ (cfβ€˜π΄) = ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴} (cardβ€˜π‘¦))
103100, 102sseqtrrd 4024 . . 3 (Lim 𝐴 β†’ Ο‰ βŠ† (cfβ€˜π΄))
104 fvex 6905 . . . . . . 7 (cardβ€˜π‘¦) ∈ V
105104dfiin2 5038 . . . . . 6 ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴} (cardβ€˜π‘¦) = ∩ {π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)}
106102, 105eqtrdi 2789 . . . . 5 (Lim 𝐴 β†’ (cfβ€˜π΄) = ∩ {π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)})
107 cardlim 9967 . . . . . . . . 9 (Ο‰ βŠ† (cardβ€˜π‘¦) ↔ Lim (cardβ€˜π‘¦))
108 sseq2 4009 . . . . . . . . . 10 (π‘₯ = (cardβ€˜π‘¦) β†’ (Ο‰ βŠ† π‘₯ ↔ Ο‰ βŠ† (cardβ€˜π‘¦)))
109 limeq 6377 . . . . . . . . . 10 (π‘₯ = (cardβ€˜π‘¦) β†’ (Lim π‘₯ ↔ Lim (cardβ€˜π‘¦)))
110108, 109bibi12d 346 . . . . . . . . 9 (π‘₯ = (cardβ€˜π‘¦) β†’ ((Ο‰ βŠ† π‘₯ ↔ Lim π‘₯) ↔ (Ο‰ βŠ† (cardβ€˜π‘¦) ↔ Lim (cardβ€˜π‘¦))))
111107, 110mpbiri 258 . . . . . . . 8 (π‘₯ = (cardβ€˜π‘¦) β†’ (Ο‰ βŠ† π‘₯ ↔ Lim π‘₯))
112111rexlimivw 3152 . . . . . . 7 (βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦) β†’ (Ο‰ βŠ† π‘₯ ↔ Lim π‘₯))
113112ss2abi 4064 . . . . . 6 {π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)} βŠ† {π‘₯ ∣ (Ο‰ βŠ† π‘₯ ↔ Lim π‘₯)}
114 eleq1 2822 . . . . . . . . . 10 (π‘₯ = (cardβ€˜π‘¦) β†’ (π‘₯ ∈ On ↔ (cardβ€˜π‘¦) ∈ On))
11588, 114mpbiri 258 . . . . . . . . 9 (π‘₯ = (cardβ€˜π‘¦) β†’ π‘₯ ∈ On)
116115rexlimivw 3152 . . . . . . . 8 (βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦) β†’ π‘₯ ∈ On)
117116abssi 4068 . . . . . . 7 {π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)} βŠ† On
118 fvex 6905 . . . . . . . . 9 (cfβ€˜π΄) ∈ V
119106, 118eqeltrrdi 2843 . . . . . . . 8 (Lim 𝐴 β†’ ∩ {π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)} ∈ V)
120 intex 5338 . . . . . . . 8 ({π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)} β‰  βˆ… ↔ ∩ {π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)} ∈ V)
121119, 120sylibr 233 . . . . . . 7 (Lim 𝐴 β†’ {π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)} β‰  βˆ…)
122 onint 7778 . . . . . . 7 (({π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)} βŠ† On ∧ {π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)} β‰  βˆ…) β†’ ∩ {π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)} ∈ {π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)})
123117, 121, 122sylancr 588 . . . . . 6 (Lim 𝐴 β†’ ∩ {π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)} ∈ {π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)})
124113, 123sselid 3981 . . . . 5 (Lim 𝐴 β†’ ∩ {π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)} ∈ {π‘₯ ∣ (Ο‰ βŠ† π‘₯ ↔ Lim π‘₯)})
125106, 124eqeltrd 2834 . . . 4 (Lim 𝐴 β†’ (cfβ€˜π΄) ∈ {π‘₯ ∣ (Ο‰ βŠ† π‘₯ ↔ Lim π‘₯)})
126 sseq2 4009 . . . . . 6 (π‘₯ = (cfβ€˜π΄) β†’ (Ο‰ βŠ† π‘₯ ↔ Ο‰ βŠ† (cfβ€˜π΄)))
127 limeq 6377 . . . . . 6 (π‘₯ = (cfβ€˜π΄) β†’ (Lim π‘₯ ↔ Lim (cfβ€˜π΄)))
128126, 127bibi12d 346 . . . . 5 (π‘₯ = (cfβ€˜π΄) β†’ ((Ο‰ βŠ† π‘₯ ↔ Lim π‘₯) ↔ (Ο‰ βŠ† (cfβ€˜π΄) ↔ Lim (cfβ€˜π΄))))
129118, 128elab 3669 . . . 4 ((cfβ€˜π΄) ∈ {π‘₯ ∣ (Ο‰ βŠ† π‘₯ ↔ Lim π‘₯)} ↔ (Ο‰ βŠ† (cfβ€˜π΄) ↔ Lim (cfβ€˜π΄)))
130125, 129sylib 217 . . 3 (Lim 𝐴 β†’ (Ο‰ βŠ† (cfβ€˜π΄) ↔ Lim (cfβ€˜π΄)))
131103, 130mpbid 231 . 2 (Lim 𝐴 β†’ Lim (cfβ€˜π΄))
132 eloni 6375 . . . . . . 7 (𝐴 ∈ On β†’ Ord 𝐴)
133 ordzsl 7834 . . . . . . 7 (Ord 𝐴 ↔ (𝐴 = βˆ… ∨ βˆƒπ‘₯ ∈ On 𝐴 = suc π‘₯ ∨ Lim 𝐴))
134132, 133sylib 217 . . . . . 6 (𝐴 ∈ On β†’ (𝐴 = βˆ… ∨ βˆƒπ‘₯ ∈ On 𝐴 = suc π‘₯ ∨ Lim 𝐴))
135 df-3or 1089 . . . . . . 7 ((𝐴 = βˆ… ∨ βˆƒπ‘₯ ∈ On 𝐴 = suc π‘₯ ∨ Lim 𝐴) ↔ ((𝐴 = βˆ… ∨ βˆƒπ‘₯ ∈ On 𝐴 = suc π‘₯) ∨ Lim 𝐴))
136 orcom 869 . . . . . . 7 (((𝐴 = βˆ… ∨ βˆƒπ‘₯ ∈ On 𝐴 = suc π‘₯) ∨ Lim 𝐴) ↔ (Lim 𝐴 ∨ (𝐴 = βˆ… ∨ βˆƒπ‘₯ ∈ On 𝐴 = suc π‘₯)))
137 df-or 847 . . . . . . 7 ((Lim 𝐴 ∨ (𝐴 = βˆ… ∨ βˆƒπ‘₯ ∈ On 𝐴 = suc π‘₯)) ↔ (Β¬ Lim 𝐴 β†’ (𝐴 = βˆ… ∨ βˆƒπ‘₯ ∈ On 𝐴 = suc π‘₯)))
138135, 136, 1373bitri 297 . . . . . 6 ((𝐴 = βˆ… ∨ βˆƒπ‘₯ ∈ On 𝐴 = suc π‘₯ ∨ Lim 𝐴) ↔ (Β¬ Lim 𝐴 β†’ (𝐴 = βˆ… ∨ βˆƒπ‘₯ ∈ On 𝐴 = suc π‘₯)))
139134, 138sylib 217 . . . . 5 (𝐴 ∈ On β†’ (Β¬ Lim 𝐴 β†’ (𝐴 = βˆ… ∨ βˆƒπ‘₯ ∈ On 𝐴 = suc π‘₯)))
140 fveq2 6892 . . . . . . . . 9 (𝐴 = βˆ… β†’ (cfβ€˜π΄) = (cfβ€˜βˆ…))
141 cf0 10246 . . . . . . . . 9 (cfβ€˜βˆ…) = βˆ…
142140, 141eqtrdi 2789 . . . . . . . 8 (𝐴 = βˆ… β†’ (cfβ€˜π΄) = βˆ…)
143 limeq 6377 . . . . . . . 8 ((cfβ€˜π΄) = βˆ… β†’ (Lim (cfβ€˜π΄) ↔ Lim βˆ…))
144142, 143syl 17 . . . . . . 7 (𝐴 = βˆ… β†’ (Lim (cfβ€˜π΄) ↔ Lim βˆ…))
14577, 144mtbiri 327 . . . . . 6 (𝐴 = βˆ… β†’ Β¬ Lim (cfβ€˜π΄))
146 1n0 8488 . . . . . . . . . 10 1o β‰  βˆ…
147 df1o2 8473 . . . . . . . . . . . 12 1o = {βˆ…}
148147unieqi 4922 . . . . . . . . . . 11 βˆͺ 1o = βˆͺ {βˆ…}
149 0ex 5308 . . . . . . . . . . . 12 βˆ… ∈ V
150149unisn 4931 . . . . . . . . . . 11 βˆͺ {βˆ…} = βˆ…
151148, 150eqtri 2761 . . . . . . . . . 10 βˆͺ 1o = βˆ…
152146, 151neeqtrri 3015 . . . . . . . . 9 1o β‰  βˆͺ 1o
153 limuni 6426 . . . . . . . . . 10 (Lim 1o β†’ 1o = βˆͺ 1o)
154153necon3ai 2966 . . . . . . . . 9 (1o β‰  βˆͺ 1o β†’ Β¬ Lim 1o)
155152, 154ax-mp 5 . . . . . . . 8 Β¬ Lim 1o
156 fveq2 6892 . . . . . . . . . 10 (𝐴 = suc π‘₯ β†’ (cfβ€˜π΄) = (cfβ€˜suc π‘₯))
157 cfsuc 10252 . . . . . . . . . 10 (π‘₯ ∈ On β†’ (cfβ€˜suc π‘₯) = 1o)
158156, 157sylan9eqr 2795 . . . . . . . . 9 ((π‘₯ ∈ On ∧ 𝐴 = suc π‘₯) β†’ (cfβ€˜π΄) = 1o)
159 limeq 6377 . . . . . . . . 9 ((cfβ€˜π΄) = 1o β†’ (Lim (cfβ€˜π΄) ↔ Lim 1o))
160158, 159syl 17 . . . . . . . 8 ((π‘₯ ∈ On ∧ 𝐴 = suc π‘₯) β†’ (Lim (cfβ€˜π΄) ↔ Lim 1o))
161155, 160mtbiri 327 . . . . . . 7 ((π‘₯ ∈ On ∧ 𝐴 = suc π‘₯) β†’ Β¬ Lim (cfβ€˜π΄))
162161rexlimiva 3148 . . . . . 6 (βˆƒπ‘₯ ∈ On 𝐴 = suc π‘₯ β†’ Β¬ Lim (cfβ€˜π΄))
163145, 162jaoi 856 . . . . 5 ((𝐴 = βˆ… ∨ βˆƒπ‘₯ ∈ On 𝐴 = suc π‘₯) β†’ Β¬ Lim (cfβ€˜π΄))
164139, 163syl6 35 . . . 4 (𝐴 ∈ On β†’ (Β¬ Lim 𝐴 β†’ Β¬ Lim (cfβ€˜π΄)))
165164con4d 115 . . 3 (𝐴 ∈ On β†’ (Lim (cfβ€˜π΄) β†’ Lim 𝐴))
166 cff 10243 . . . . . . . . 9 cf:On⟢On
167166fdmi 6730 . . . . . . . 8 dom cf = On
168167eleq2i 2826 . . . . . . 7 (𝐴 ∈ dom cf ↔ 𝐴 ∈ On)
169 ndmfv 6927 . . . . . . 7 (Β¬ 𝐴 ∈ dom cf β†’ (cfβ€˜π΄) = βˆ…)
170168, 169sylnbir 331 . . . . . 6 (Β¬ 𝐴 ∈ On β†’ (cfβ€˜π΄) = βˆ…)
171170, 143syl 17 . . . . 5 (Β¬ 𝐴 ∈ On β†’ (Lim (cfβ€˜π΄) ↔ Lim βˆ…))
17277, 171mtbiri 327 . . . 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 397   ∨ wo 846   ∨ w3o 1087   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  {cab 2710   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  {crab 3433  Vcvv 3475   βŠ† wss 3949  βˆ…c0 4323  π’« cpw 4603  {csn 4629  βˆͺ cuni 4909  βˆ© cint 4951  βˆ© ciin 4999   class class class wbr 5149   E cep 5580   Or wor 5588   Fr wfr 5629   We wwe 5631  β—‘ccnv 5676  dom cdm 5677  Ord word 6364  Oncon0 6365  Lim wlim 6366  suc csuc 6367  β€˜cfv 6544  Ο‰com 7855  1oc1o 8459   β‰ˆ cen 8936   β‰Ί csdm 8938  Fincfn 8939  cardccrd 9930  cfccf 9932
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-inf2 9636
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-card 9934  df-cf 9936
This theorem is referenced by:  cfom  10259
  Copyright terms: Public domain W3C validator