MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cflim2 Structured version   Visualization version   GIF version
Theorem cflim2 10255
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 4607 . . . . . . . . 9 (𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 βŠ† 𝐴)
3 limord 6422 . . . . . . . . . . . . . . . . . . . 20 (Lim 𝐴 β†’ Ord 𝐴)
4 ordsson 7767 . . . . . . . . . . . . . . . . . . . 20 (Ord 𝐴 β†’ 𝐴 βŠ† On)
5 sstr 3990 . . . . . . . . . . . . . . . . . . . . 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 3977 . . . . . . . . . . . . . . . . . . 19 ((𝑦 βŠ† On ∧ 𝑠 ∈ 𝑦) β†’ 𝑠 ∈ On)
11 eloni 6372 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ On β†’ Ord 𝑠)
12 ordirr 6380 . . . . . . . . . . . . . . . . . . 19 (Ord 𝑠 β†’ Β¬ 𝑠 ∈ 𝑠)
1310, 11, 123syl 18 . . . . . . . . . . . . . . . . . 18 ((𝑦 βŠ† On ∧ 𝑠 ∈ 𝑦) β†’ Β¬ 𝑠 ∈ 𝑠)
14 ssel 3975 . . . . . . . . . . . . . . . . . . . 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 3990 . . . . . . . . . . . . . . . . 17 ((𝑦 βŠ† 𝐴 ∧ 𝐴 βŠ† 𝑠) β†’ 𝑦 βŠ† 𝑠)
2119, 20sylan 581 . . . . . . . . . . . . . . . 16 ((((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) ∧ 𝐴 βŠ† 𝑠) β†’ 𝑦 βŠ† 𝑠)
2218, 21mtand 815 . . . . . . . . . . . . . . 15 (((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) β†’ Β¬ 𝐴 βŠ† 𝑠)
23 simpl3 1194 . . . . . . . . . . . . . . . 16 (((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) β†’ βˆͺ 𝑦 = 𝐴)
2423sseq1d 4013 . . . . . . . . . . . . . . 15 (((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) β†’ (βˆͺ 𝑦 βŠ† 𝑠 ↔ 𝐴 βŠ† 𝑠))
2522, 24mtbird 325 . . . . . . . . . . . . . 14 (((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) β†’ Β¬ βˆͺ 𝑦 βŠ† 𝑠)
26 unissb 4943 . . . . . . . . . . . . . 14 (βˆͺ 𝑦 βŠ† 𝑠 ↔ βˆ€π‘‘ ∈ 𝑦 𝑑 βŠ† 𝑠)
2725, 26sylnib 328 . . . . . . . . . . . . 13 (((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) β†’ Β¬ βˆ€π‘‘ ∈ 𝑦 𝑑 βŠ† 𝑠)
2827nrexdv 3150 . . . . . . . . . . . 12 ((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) β†’ Β¬ βˆƒπ‘  ∈ 𝑦 βˆ€π‘‘ ∈ 𝑦 𝑑 βŠ† 𝑠)
29 ssel 3975 . . . . . . . . . . . . . . . . 17 (𝑦 βŠ† On β†’ (𝑠 ∈ 𝑦 β†’ 𝑠 ∈ On))
30 ssel 3975 . . . . . . . . . . . . . . . . 17 (𝑦 βŠ† On β†’ (𝑑 ∈ 𝑦 β†’ 𝑑 ∈ On))
31 ontri1 6396 . . . . . . . . . . . . . . . . . . . 20 ((𝑑 ∈ On ∧ 𝑠 ∈ On) β†’ (𝑑 βŠ† 𝑠 ↔ Β¬ 𝑠 ∈ 𝑑))
3231ancoms 460 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ On ∧ 𝑑 ∈ On) β†’ (𝑑 βŠ† 𝑠 ↔ Β¬ 𝑠 ∈ 𝑑))
33 vex 3479 . . . . . . . . . . . . . . . . . . . . . 22 𝑑 ∈ V
34 vex 3479 . . . . . . . . . . . . . . . . . . . . . 22 𝑠 ∈ V
3533, 34brcnv 5881 . . . . . . . . . . . . . . . . . . . . 21 (𝑑◑ E 𝑠 ↔ 𝑠 E 𝑑)
36 epel 5583 . . . . . . . . . . . . . . . . . . . . 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 7759 . . . . . . . . . . . . . . . . . 18 E We On
50 wess 5663 . . . . . . . . . . . . . . . . . 18 (𝑦 βŠ† On β†’ ( E We On β†’ E We 𝑦))
5149, 50mpi 20 . . . . . . . . . . . . . . . . 17 (𝑦 βŠ† On β†’ E We 𝑦)
52 weso 5667 . . . . . . . . . . . . . . . . 17 ( E We 𝑦 β†’ E Or 𝑦)
5351, 52syl 17 . . . . . . . . . . . . . . . 16 (𝑦 βŠ† On β†’ E Or 𝑦)
54 cnvso 6285 . . . . . . . . . . . . . . . 16 ( E Or 𝑦 ↔ β—‘ E Or 𝑦)
5553, 54sylib 217 . . . . . . . . . . . . . . 15 (𝑦 βŠ† On β†’ β—‘ E Or 𝑦)
56 onssnum 10032 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ V ∧ 𝑦 βŠ† On) β†’ 𝑦 ∈ dom card)
5747, 56mpan 689 . . . . . . . . . . . . . . . . . 18 (𝑦 βŠ† On β†’ 𝑦 ∈ dom card)
58 cardid2 9945 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ dom card β†’ (cardβ€˜π‘¦) β‰ˆ 𝑦)
59 ensym 8996 . . . . . . . . . . . . . . . . . 18 ((cardβ€˜π‘¦) β‰ˆ 𝑦 β†’ 𝑦 β‰ˆ (cardβ€˜π‘¦))
6057, 58, 593syl 18 . . . . . . . . . . . . . . . . 17 (𝑦 βŠ† On β†’ 𝑦 β‰ˆ (cardβ€˜π‘¦))
61 nnsdom 9646 . . . . . . . . . . . . . . . . 17 ((cardβ€˜π‘¦) ∈ Ο‰ β†’ (cardβ€˜π‘¦) β‰Ί Ο‰)
62 ensdomtr 9110 . . . . . . . . . . . . . . . . 17 ((𝑦 β‰ˆ (cardβ€˜π‘¦) ∧ (cardβ€˜π‘¦) β‰Ί Ο‰) β†’ 𝑦 β‰Ί Ο‰)
6360, 61, 62syl2an 597 . . . . . . . . . . . . . . . 16 ((𝑦 βŠ† On ∧ (cardβ€˜π‘¦) ∈ Ο‰) β†’ 𝑦 β‰Ί Ο‰)
64 isfinite 9644 . . . . . . . . . . . . . . . 16 (𝑦 ∈ Fin ↔ 𝑦 β‰Ί Ο‰)
6563, 64sylibr 233 . . . . . . . . . . . . . . 15 ((𝑦 βŠ† On ∧ (cardβ€˜π‘¦) ∈ Ο‰) β†’ 𝑦 ∈ Fin)
66 wofi 9289 . . . . . . . . . . . . . . 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 5666 . . . . . . . . . . . . 13 (β—‘ E We 𝑦 β†’ β—‘ E Fr 𝑦)
7068, 69syl 17 . . . . . . . . . . . 12 (((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) ∧ (cardβ€˜π‘¦) ∈ Ο‰) β†’ β—‘ E Fr 𝑦)
71 ssidd 4005 . . . . . . . . . . . 12 (((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) ∧ (cardβ€˜π‘¦) ∈ Ο‰) β†’ 𝑦 βŠ† 𝑦)
72 unieq 4919 . . . . . . . . . . . . . . . . . . 19 (𝑦 = βˆ… β†’ βˆͺ 𝑦 = βˆͺ βˆ…)
73 uni0 4939 . . . . . . . . . . . . . . . . . . 19 βˆͺ βˆ… = βˆ…
7472, 73eqtrdi 2789 . . . . . . . . . . . . . . . . . 18 (𝑦 = βˆ… β†’ βˆͺ 𝑦 = βˆ…)
75 eqeq1 2737 . . . . . . . . . . . . . . . . . 18 (βˆͺ 𝑦 = 𝐴 β†’ (βˆͺ 𝑦 = βˆ… ↔ 𝐴 = βˆ…))
7674, 75imbitrid 243 . . . . . . . . . . . . . . . . 17 (βˆͺ 𝑦 = 𝐴 β†’ (𝑦 = βˆ… β†’ 𝐴 = βˆ…))
77 nlim0 6421 . . . . . . . . . . . . . . . . . 18 Β¬ Lim βˆ…
78 limeq 6374 . . . . . . . . . . . . . . . . . 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 5636 . . . . . . . . . . . 12 (((𝑦 ∈ V ∧ β—‘ E Fr 𝑦) ∧ (𝑦 βŠ† 𝑦 ∧ 𝑦 β‰  βˆ…)) β†’ βˆƒπ‘  ∈ 𝑦 βˆ€π‘‘ ∈ 𝑦 Β¬ 𝑑◑ E 𝑠)
8648, 70, 71, 84, 85syl22anc 838 . . . . . . . . . . 11 (((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) ∧ (cardβ€˜π‘¦) ∈ Ο‰) β†’ βˆƒπ‘  ∈ 𝑦 βˆ€π‘‘ ∈ 𝑦 Β¬ 𝑑◑ E 𝑠)
8746, 86mtand 815 . . . . . . . . . 10 ((Lim 𝐴 ∧ 𝑦 βŠ† 𝐴 ∧ βˆͺ 𝑦 = 𝐴) β†’ Β¬ (cardβ€˜π‘¦) ∈ Ο‰)
88 cardon 9936 . . . . . . . . . . 11 (cardβ€˜π‘¦) ∈ On
89 eloni 6372 . . . . . . . . . . 11 ((cardβ€˜π‘¦) ∈ On β†’ Ord (cardβ€˜π‘¦))
90 ordom 7862 . . . . . . . . . . . 12 Ord Ο‰
91 ordtri1 6395 . . . . . . . . . . . 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 5058 . . . . 5 (Ο‰ βŠ† ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴} (cardβ€˜π‘¦) ↔ βˆ€π‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}Ο‰ βŠ† (cardβ€˜π‘¦))
10098, 99sylibr 233 . . . 4 (Lim 𝐴 β†’ Ο‰ βŠ† ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴} (cardβ€˜π‘¦))
101 cflim2.1 . . . . 5 𝐴 ∈ V
102101cflim3 10254 . . . 4 (Lim 𝐴 β†’ (cfβ€˜π΄) = ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴} (cardβ€˜π‘¦))
103100, 102sseqtrrd 4023 . . 3 (Lim 𝐴 β†’ Ο‰ βŠ† (cfβ€˜π΄))
104 fvex 6902 . . . . . . 7 (cardβ€˜π‘¦) ∈ V
105104dfiin2 5037 . . . . . 6 ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴} (cardβ€˜π‘¦) = ∩ {π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)}
106102, 105eqtrdi 2789 . . . . 5 (Lim 𝐴 β†’ (cfβ€˜π΄) = ∩ {π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)})
107 cardlim 9964 . . . . . . . . 9 (Ο‰ βŠ† (cardβ€˜π‘¦) ↔ Lim (cardβ€˜π‘¦))
108 sseq2 4008 . . . . . . . . . 10 (π‘₯ = (cardβ€˜π‘¦) β†’ (Ο‰ βŠ† π‘₯ ↔ Ο‰ βŠ† (cardβ€˜π‘¦)))
109 limeq 6374 . . . . . . . . . 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 4063 . . . . . 6 {π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)} βŠ† {π‘₯ ∣ (Ο‰ βŠ† π‘₯ ↔ Lim π‘₯)}
114 eleq1 2822 . . . . . . . . . 10 (π‘₯ = (cardβ€˜π‘¦) β†’ (π‘₯ ∈ On ↔ (cardβ€˜π‘¦) ∈ On))
11588, 114mpbiri 258 . . . . . . . . 9 (π‘₯ = (cardβ€˜π‘¦) β†’ π‘₯ ∈ On)
116115rexlimivw 3152 . . . . . . . 8 (βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦) β†’ π‘₯ ∈ On)
117116abssi 4067 . . . . . . 7 {π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)} βŠ† On
118 fvex 6902 . . . . . . . . 9 (cfβ€˜π΄) ∈ V
119106, 118eqeltrrdi 2843 . . . . . . . 8 (Lim 𝐴 β†’ ∩ {π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)} ∈ V)
120 intex 5337 . . . . . . . 8 ({π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)} β‰  βˆ… ↔ ∩ {π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)} ∈ V)
121119, 120sylibr 233 . . . . . . 7 (Lim 𝐴 β†’ {π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)} β‰  βˆ…)
122 onint 7775 . . . . . . 7 (({π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)} βŠ† On ∧ {π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)} β‰  βˆ…) β†’ ∩ {π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)} ∈ {π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)})
123117, 121, 122sylancr 588 . . . . . 6 (Lim 𝐴 β†’ ∩ {π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)} ∈ {π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)})
124113, 123sselid 3980 . . . . 5 (Lim 𝐴 β†’ ∩ {π‘₯ ∣ βˆƒπ‘¦ ∈ {𝑦 ∈ 𝒫 𝐴 ∣ βˆͺ 𝑦 = 𝐴}π‘₯ = (cardβ€˜π‘¦)} ∈ {π‘₯ ∣ (Ο‰ βŠ† π‘₯ ↔ Lim π‘₯)})
125106, 124eqeltrd 2834 . . . 4 (Lim 𝐴 β†’ (cfβ€˜π΄) ∈ {π‘₯ ∣ (Ο‰ βŠ† π‘₯ ↔ Lim π‘₯)})
126 sseq2 4008 . . . . . 6 (π‘₯ = (cfβ€˜π΄) β†’ (Ο‰ βŠ† π‘₯ ↔ Ο‰ βŠ† (cfβ€˜π΄)))
127 limeq 6374 . . . . . 6 (π‘₯ = (cfβ€˜π΄) β†’ (Lim π‘₯ ↔ Lim (cfβ€˜π΄)))
128126, 127bibi12d 346 . . . . 5 (π‘₯ = (cfβ€˜π΄) β†’ ((Ο‰ βŠ† π‘₯ ↔ Lim π‘₯) ↔ (Ο‰ βŠ† (cfβ€˜π΄) ↔ Lim (cfβ€˜π΄))))
129118, 128elab 3668 . . . 4 ((cfβ€˜π΄) ∈ {π‘₯ ∣ (Ο‰ βŠ† π‘₯ ↔ Lim π‘₯)} ↔ (Ο‰ βŠ† (cfβ€˜π΄) ↔ Lim (cfβ€˜π΄)))
130125, 129sylib 217 . . 3 (Lim 𝐴 β†’ (Ο‰ βŠ† (cfβ€˜π΄) ↔ Lim (cfβ€˜π΄)))
131103, 130mpbid 231 . 2 (Lim 𝐴 β†’ Lim (cfβ€˜π΄))
132 eloni 6372 . . . . . . 7 (𝐴 ∈ On β†’ Ord 𝐴)
133 ordzsl 7831 . . . . . . 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 6889 . . . . . . . . 9 (𝐴 = βˆ… β†’ (cfβ€˜π΄) = (cfβ€˜βˆ…))
141 cf0 10243 . . . . . . . . 9 (cfβ€˜βˆ…) = βˆ…
142140, 141eqtrdi 2789 . . . . . . . 8 (𝐴 = βˆ… β†’ (cfβ€˜π΄) = βˆ…)
143 limeq 6374 . . . . . . . 8 ((cfβ€˜π΄) = βˆ… β†’ (Lim (cfβ€˜π΄) ↔ Lim βˆ…))
144142, 143syl 17 . . . . . . 7 (𝐴 = βˆ… β†’ (Lim (cfβ€˜π΄) ↔ Lim βˆ…))
14577, 144mtbiri 327 . . . . . 6 (𝐴 = βˆ… β†’ Β¬ Lim (cfβ€˜π΄))
146 1n0 8485 . . . . . . . . . 10 1o β‰  βˆ…
147 df1o2 8470 . . . . . . . . . . . 12 1o = {βˆ…}
148147unieqi 4921 . . . . . . . . . . 11 βˆͺ 1o = βˆͺ {βˆ…}
149 0ex 5307 . . . . . . . . . . . 12 βˆ… ∈ V
150149unisn 4930 . . . . . . . . . . 11 βˆͺ {βˆ…} = βˆ…
151148, 150eqtri 2761 . . . . . . . . . 10 βˆͺ 1o = βˆ…
152146, 151neeqtrri 3015 . . . . . . . . 9 1o β‰  βˆͺ 1o
153 limuni 6423 . . . . . . . . . 10 (Lim 1o β†’ 1o = βˆͺ 1o)
154153necon3ai 2966 . . . . . . . . 9 (1o β‰  βˆͺ 1o β†’ Β¬ Lim 1o)
155152, 154ax-mp 5 . . . . . . . 8 Β¬ Lim 1o
156 fveq2 6889 . . . . . . . . . 10 (𝐴 = suc π‘₯ β†’ (cfβ€˜π΄) = (cfβ€˜suc π‘₯))
157 cfsuc 10249 . . . . . . . . . 10 (π‘₯ ∈ On β†’ (cfβ€˜suc π‘₯) = 1o)
158156, 157sylan9eqr 2795 . . . . . . . . 9 ((π‘₯ ∈ On ∧ 𝐴 = suc π‘₯) β†’ (cfβ€˜π΄) = 1o)
159 limeq 6374 . . . . . . . . 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 10240 . . . . . . . . 9 cf:On⟢On
167166fdmi 6727 . . . . . . . 8 dom cf = On
168167eleq2i 2826 . . . . . . 7 (𝐴 ∈ dom cf ↔ 𝐴 ∈ On)
169 ndmfv 6924 . . . . . . 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 3948  βˆ…c0 4322  π’« cpw 4602  {csn 4628  βˆͺ cuni 4908  βˆ© cint 4950  βˆ© ciin 4998   class class class wbr 5148   E cep 5579   Or wor 5587   Fr wfr 5628   We wwe 5630  β—‘ccnv 5675  dom cdm 5676  Ord word 6361  Oncon0 6362  Lim wlim 6363  suc csuc 6364  β€˜cfv 6541  Ο‰com 7852  1oc1o 8456   β‰ˆ cen 8933   β‰Ί csdm 8935  Fincfn 8936  cardccrd 9927  cfccf 9929
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 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-inf2 9633
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 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550  df-riota 7362  df-ov 7409  df-om 7853  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-card 9931  df-cf 9933
This theorem is referenced by:  cfom  10256
  Copyright terms: Public domain W3C validator