Step | Hyp | Ref
| Expression |
1 | | ffn 6045 |
. . . . 5
|
2 | | fnresdm 6000 |
. . . . 5
|
3 | 1, 2 | syl 17 |
. . . 4
|
4 | 3 | adantl 482 |
. . 3
|
5 | 4 | fveq2d 6195 |
. 2
|
6 | | ssid 3624 |
. . . 4
|
7 | | sseq1 3626 |
. . . . . 6
|
8 | | reseq2 5391 |
. . . . . . . . . 10
|
9 | | res0 5400 |
. . . . . . . . . 10
|
10 | 8, 9 | syl6eq 2672 |
. . . . . . . . 9
|
11 | 10 | fveq2d 6195 |
. . . . . . . 8
|
12 | 11 | eleq1d 2686 |
. . . . . . 7
|
13 | 12 | imbi2d 330 |
. . . . . 6
|
14 | 7, 13 | imbi12d 334 |
. . . . 5
|
15 | | sseq1 3626 |
. . . . . 6
|
16 | | reseq2 5391 |
. . . . . . . . 9
|
17 | 16 | fveq2d 6195 |
. . . . . . . 8
|
18 | 17 | eleq1d 2686 |
. . . . . . 7
|
19 | 18 | imbi2d 330 |
. . . . . 6
|
20 | 15, 19 | imbi12d 334 |
. . . . 5
|
21 | | sseq1 3626 |
. . . . . 6
|
22 | | reseq2 5391 |
. . . . . . . . 9
|
23 | 22 | fveq2d 6195 |
. . . . . . . 8
|
24 | 23 | eleq1d 2686 |
. . . . . . 7
|
25 | 24 | imbi2d 330 |
. . . . . 6
|
26 | 21, 25 | imbi12d 334 |
. . . . 5
|
27 | | sseq1 3626 |
. . . . . 6
|
28 | | reseq2 5391 |
. . . . . . . . 9
|
29 | 28 | fveq2d 6195 |
. . . . . . . 8
|
30 | 29 | eleq1d 2686 |
. . . . . . 7
|
31 | 30 | imbi2d 330 |
. . . . . 6
|
32 | 27, 31 | imbi12d 334 |
. . . . 5
|
33 | | 0ex 4790 |
. . . . . . . . 9
|
34 | | f0 6086 |
. . . . . . . . 9
|
35 | | pttop 21385 |
. . . . . . . . 9
|
36 | 33, 34, 35 | mp2an 708 |
. . . . . . . 8
|
37 | | eqid 2622 |
. . . . . . . . . . . . 13
|
38 | 37 | ptuni 21397 |
. . . . . . . . . . . 12
|
39 | 33, 34, 38 | mp2an 708 |
. . . . . . . . . . 11
|
40 | | ixp0x 7936 |
. . . . . . . . . . . 12
|
41 | | snfi 8038 |
. . . . . . . . . . . 12
|
42 | 40, 41 | eqeltri 2697 |
. . . . . . . . . . 11
|
43 | 39, 42 | eqeltrri 2698 |
. . . . . . . . . 10
|
44 | | pwfi 8261 |
. . . . . . . . . 10
|
45 | 43, 44 | mpbi 220 |
. . . . . . . . 9
|
46 | | pwuni 4474 |
. . . . . . . . 9
|
47 | | ssfi 8180 |
. . . . . . . . 9
|
48 | 45, 46, 47 | mp2an 708 |
. . . . . . . 8
|
49 | | elin 3796 |
. . . . . . . 8
|
50 | 36, 48, 49 | mpbir2an 955 |
. . . . . . 7
|
51 | | fincmp 21196 |
. . . . . . 7
|
52 | 50, 51 | ax-mp 5 |
. . . . . 6
|
53 | 52 | 2a1i 12 |
. . . . 5
|
54 | | ssun1 3776 |
. . . . . . . . 9
|
55 | | id 22 |
. . . . . . . . 9
|
56 | 54, 55 | syl5ss 3614 |
. . . . . . . 8
|
57 | 56 | imim1i 63 |
. . . . . . 7
|
58 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
59 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
60 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
61 | | resabs1 5427 |
. . . . . . . . . . . . . . . . 17
|
62 | 54, 61 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
|
63 | 62 | eqcomi 2631 |
. . . . . . . . . . . . . . 15
|
64 | 63 | fveq2i 6194 |
. . . . . . . . . . . . . 14
|
65 | | ssun2 3777 |
. . . . . . . . . . . . . . . . 17
|
66 | | resabs1 5427 |
. . . . . . . . . . . . . . . . 17
|
67 | 65, 66 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
|
68 | 67 | eqcomi 2631 |
. . . . . . . . . . . . . . 15
|
69 | 68 | fveq2i 6194 |
. . . . . . . . . . . . . 14
|
70 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
71 | | vex 3203 |
. . . . . . . . . . . . . . . 16
|
72 | | snex 4908 |
. . . . . . . . . . . . . . . 16
|
73 | 71, 72 | unex 6956 |
. . . . . . . . . . . . . . 15
|
74 | 73 | a1i 11 |
. . . . . . . . . . . . . 14
|
75 | | simplr 792 |
. . . . . . . . . . . . . . . 16
|
76 | | cmptop 21198 |
. . . . . . . . . . . . . . . . 17
|
77 | 76 | ssriv 3607 |
. . . . . . . . . . . . . . . 16
|
78 | | fss 6056 |
. . . . . . . . . . . . . . . 16
|
79 | 75, 77, 78 | sylancl 694 |
. . . . . . . . . . . . . . 15
|
80 | | simprr 796 |
. . . . . . . . . . . . . . 15
|
81 | 79, 80 | fssresd 6071 |
. . . . . . . . . . . . . 14
|
82 | | eqidd 2623 |
. . . . . . . . . . . . . 14
|
83 | | simprl 794 |
. . . . . . . . . . . . . . 15
|
84 | | disjsn 4246 |
. . . . . . . . . . . . . . 15
|
85 | 83, 84 | sylibr 224 |
. . . . . . . . . . . . . 14
|
86 | 58, 59, 60, 64, 69, 70, 74, 81, 82, 85 | ptunhmeo 21611 |
. . . . . . . . . . . . 13
|
87 | | hmphi 21580 |
. . . . . . . . . . . . 13
|
88 | 86, 87 | syl 17 |
. . . . . . . . . . . 12
|
89 | 1 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
|
90 | 65, 80 | syl5ss 3614 |
. . . . . . . . . . . . . . . . 17
|
91 | | vex 3203 |
. . . . . . . . . . . . . . . . . 18
|
92 | 91 | snss 4316 |
. . . . . . . . . . . . . . . . 17
|
93 | 90, 92 | sylibr 224 |
. . . . . . . . . . . . . . . 16
|
94 | | fnressn 6425 |
. . . . . . . . . . . . . . . 16
|
95 | 89, 93, 94 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
96 | 95 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
97 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
|
98 | 91 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
99 | 75, 93 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . 19
|
100 | 77, 99 | sseldi 3601 |
. . . . . . . . . . . . . . . . . 18
|
101 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
|
102 | 101 | toptopon 20722 |
. . . . . . . . . . . . . . . . . 18
TopOn |
103 | 100, 102 | sylib 208 |
. . . . . . . . . . . . . . . . 17
TopOn |
104 | 97, 98, 103 | pt1hmeo 21609 |
. . . . . . . . . . . . . . . 16
|
105 | | hmphi 21580 |
. . . . . . . . . . . . . . . 16
|
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . . 15
|
107 | | cmphmph 21591 |
. . . . . . . . . . . . . . 15
|
108 | 106, 99, 107 | sylc 65 |
. . . . . . . . . . . . . 14
|
109 | 96, 108 | eqeltrd 2701 |
. . . . . . . . . . . . 13
|
110 | | txcmp 21446 |
. . . . . . . . . . . . . 14
|
111 | 110 | expcom 451 |
. . . . . . . . . . . . 13
|
112 | 109, 111 | syl 17 |
. . . . . . . . . . . 12
|
113 | | cmphmph 21591 |
. . . . . . . . . . . 12
|
114 | 88, 112, 113 | sylsyld 61 |
. . . . . . . . . . 11
|
115 | 114 | expcom 451 |
. . . . . . . . . 10
|
116 | 115 | a2d 29 |
. . . . . . . . 9
|
117 | 116 | ex 450 |
. . . . . . . 8
|
118 | 117 | a2d 29 |
. . . . . . 7
|
119 | 57, 118 | syl5 34 |
. . . . . 6
|
120 | 119 | adantl 482 |
. . . . 5
|
121 | 14, 20, 26, 32, 53, 120 | findcard2s 8201 |
. . . 4
|
122 | 6, 121 | mpi 20 |
. . 3
|
123 | 122 | anabsi5 858 |
. 2
|
124 | 5, 123 | eqeltrrd 2702 |
1
|