Step | Hyp | Ref
| Expression |
1 | | cfss.1 |
. . . . . 6
|
2 | 1 | cflim3 9084 |
. . . . 5
|
3 | | fvex 6201 |
. . . . . . 7
|
4 | 3 | dfiin2 4555 |
. . . . . 6
|
5 | | cardon 8770 |
. . . . . . . . . 10
|
6 | | eleq1 2689 |
. . . . . . . . . 10
|
7 | 5, 6 | mpbiri 248 |
. . . . . . . . 9
|
8 | 7 | rexlimivw 3029 |
. . . . . . . 8
|
9 | 8 | abssi 3677 |
. . . . . . 7
|
10 | | limuni 5785 |
. . . . . . . . . . . 12
|
11 | 10 | eqcomd 2628 |
. . . . . . . . . . 11
|
12 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
13 | 12 | eqcomd 2628 |
. . . . . . . . . . . . . 14
|
14 | 13 | biantrud 528 |
. . . . . . . . . . . . 13
|
15 | | unieq 4444 |
. . . . . . . . . . . . . . . 16
|
16 | 15 | eqeq1d 2624 |
. . . . . . . . . . . . . . 15
|
17 | 1 | pwid 4174 |
. . . . . . . . . . . . . . . . 17
|
18 | | eleq1 2689 |
. . . . . . . . . . . . . . . . 17
|
19 | 17, 18 | mpbiri 248 |
. . . . . . . . . . . . . . . 16
|
20 | 19 | biantrurd 529 |
. . . . . . . . . . . . . . 15
|
21 | 16, 20 | bitr3d 270 |
. . . . . . . . . . . . . 14
|
22 | 21 | anbi1d 741 |
. . . . . . . . . . . . 13
|
23 | 14, 22 | bitr2d 269 |
. . . . . . . . . . . 12
|
24 | 1, 23 | spcev 3300 |
. . . . . . . . . . 11
|
25 | 11, 24 | syl 17 |
. . . . . . . . . 10
|
26 | | df-rex 2918 |
. . . . . . . . . . 11
|
27 | | rabid 3116 |
. . . . . . . . . . . . 13
|
28 | 27 | anbi1i 731 |
. . . . . . . . . . . 12
|
29 | 28 | exbii 1774 |
. . . . . . . . . . 11
|
30 | 26, 29 | bitri 264 |
. . . . . . . . . 10
|
31 | 25, 30 | sylibr 224 |
. . . . . . . . 9
|
32 | | fvex 6201 |
. . . . . . . . . 10
|
33 | | eqeq1 2626 |
. . . . . . . . . . 11
|
34 | 33 | rexbidv 3052 |
. . . . . . . . . 10
|
35 | 32, 34 | spcev 3300 |
. . . . . . . . 9
|
36 | 31, 35 | syl 17 |
. . . . . . . 8
|
37 | | abn0 3954 |
. . . . . . . 8
|
38 | 36, 37 | sylibr 224 |
. . . . . . 7
|
39 | | onint 6995 |
. . . . . . 7
|
40 | 9, 38, 39 | sylancr 695 |
. . . . . 6
|
41 | 4, 40 | syl5eqel 2705 |
. . . . 5
|
42 | 2, 41 | eqeltrd 2701 |
. . . 4
|
43 | | fvex 6201 |
. . . . 5
|
44 | | eqeq1 2626 |
. . . . . 6
|
45 | 44 | rexbidv 3052 |
. . . . 5
|
46 | 43, 45 | elab 3350 |
. . . 4
|
47 | 42, 46 | sylib 208 |
. . 3
|
48 | | df-rex 2918 |
. . 3
|
49 | 47, 48 | sylib 208 |
. 2
|
50 | | simprl 794 |
. . . . . . . 8
|
51 | 50, 27 | sylib 208 |
. . . . . . 7
|
52 | 51 | simpld 475 |
. . . . . 6
|
53 | 52 | elpwid 4170 |
. . . . 5
|
54 | | simpl 473 |
. . . . . . 7
|
55 | | vex 3203 |
. . . . . . . . . 10
|
56 | | limord 5784 |
. . . . . . . . . . . 12
|
57 | | ordsson 6989 |
. . . . . . . . . . . 12
|
58 | 56, 57 | syl 17 |
. . . . . . . . . . 11
|
59 | | sstr 3611 |
. . . . . . . . . . 11
|
60 | 58, 59 | sylan2 491 |
. . . . . . . . . 10
|
61 | | onssnum 8863 |
. . . . . . . . . 10
|
62 | 55, 60, 61 | sylancr 695 |
. . . . . . . . 9
|
63 | | cardid2 8779 |
. . . . . . . . 9
|
64 | 62, 63 | syl 17 |
. . . . . . . 8
|
65 | 64 | ensymd 8007 |
. . . . . . 7
|
66 | 53, 54, 65 | syl2anc 693 |
. . . . . 6
|
67 | | simprr 796 |
. . . . . 6
|
68 | 66, 67 | breqtrrd 4681 |
. . . . 5
|
69 | 51 | simprd 479 |
. . . . 5
|
70 | 53, 68, 69 | 3jca 1242 |
. . . 4
|
71 | 70 | ex 450 |
. . 3
|
72 | 71 | eximdv 1846 |
. 2
|
73 | 49, 72 | mpd 15 |
1
|