Step | Hyp | Ref
| Expression |
1 | | vex 3203 |
. . . . 5
|
2 | 1 | elintrab 4488 |
. . . 4
|
3 | | filsspw 21655 |
. . . . . . . . . . . . . 14
|
4 | 3 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
|
5 | | difss 3737 |
. . . . . . . . . . . . . . 15
|
6 | | filtop 21659 |
. . . . . . . . . . . . . . . . . 18
|
7 | | difexg 4808 |
. . . . . . . . . . . . . . . . . 18
|
8 | 6, 7 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
9 | 8 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . 16
|
10 | | elpwg 4166 |
. . . . . . . . . . . . . . . 16
|
11 | 9, 10 | syl 17 |
. . . . . . . . . . . . . . 15
|
12 | 5, 11 | mpbiri 248 |
. . . . . . . . . . . . . 14
|
13 | 12 | snssd 4340 |
. . . . . . . . . . . . 13
|
14 | 4, 13 | unssd 3789 |
. . . . . . . . . . . 12
|
15 | | ssun1 3776 |
. . . . . . . . . . . . . 14
|
16 | | filn0 21666 |
. . . . . . . . . . . . . 14
|
17 | | ssn0 3976 |
. . . . . . . . . . . . . 14
|
18 | 15, 16, 17 | sylancr 695 |
. . . . . . . . . . . . 13
|
19 | 18 | 3ad2ant1 1082 |
. . . . . . . . . . . 12
|
20 | | elsni 4194 |
. . . . . . . . . . . . . . 15
|
21 | | filelss 21656 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
22 | 21 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
23 | | reldisj 4020 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
25 | | dfss4 3858 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
26 | 25 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
27 | 26 | sseq2d 3633 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
28 | 27 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
29 | 24, 28 | bitrd 268 |
. . . . . . . . . . . . . . . . . . . . . 22
|
30 | | filss 21657 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
31 | 30 | 3exp2 1285 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
32 | 31 | 3imp 1256 |
. . . . . . . . . . . . . . . . . . . . . 22
|
33 | 29, 32 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . 21
|
34 | 33 | necon3bd 2808 |
. . . . . . . . . . . . . . . . . . . 20
|
35 | 34 | 3exp 1264 |
. . . . . . . . . . . . . . . . . . 19
|
36 | 35 | com24 95 |
. . . . . . . . . . . . . . . . . 18
|
37 | 36 | 3imp1 1280 |
. . . . . . . . . . . . . . . . 17
|
38 | | ineq2 3808 |
. . . . . . . . . . . . . . . . . 18
|
39 | 38 | neeq1d 2853 |
. . . . . . . . . . . . . . . . 17
|
40 | 37, 39 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . 16
|
41 | 40 | expimpd 629 |
. . . . . . . . . . . . . . 15
|
42 | 20, 41 | sylan2i 687 |
. . . . . . . . . . . . . 14
|
43 | 42 | ralrimivv 2970 |
. . . . . . . . . . . . 13
|
44 | | filfbas 21652 |
. . . . . . . . . . . . . . 15
|
45 | 44 | 3ad2ant1 1082 |
. . . . . . . . . . . . . 14
|
46 | 5 | a1i 11 |
. . . . . . . . . . . . . . 15
|
47 | 26 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . . . . 22
|
48 | | difeq2 3722 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
49 | | dif0 3950 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
50 | 48, 49 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
51 | 50 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . . . . . 22
|
52 | 47, 51 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . . 21
|
53 | 6 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . 21
|
54 | 52, 53 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . 20
|
55 | 54 | 3expia 1267 |
. . . . . . . . . . . . . . . . . . 19
|
56 | 55 | necon3bd 2808 |
. . . . . . . . . . . . . . . . . 18
|
57 | 56 | ex 450 |
. . . . . . . . . . . . . . . . 17
|
58 | 57 | com23 86 |
. . . . . . . . . . . . . . . 16
|
59 | 58 | 3imp 1256 |
. . . . . . . . . . . . . . 15
|
60 | 6 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . 15
|
61 | | snfbas 21670 |
. . . . . . . . . . . . . . 15
|
62 | 46, 59, 60, 61 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
63 | | fbunfip 21673 |
. . . . . . . . . . . . . 14
|
64 | 45, 62, 63 | syl2anc 693 |
. . . . . . . . . . . . 13
|
65 | 43, 64 | mpbird 247 |
. . . . . . . . . . . 12
|
66 | | fsubbas 21671 |
. . . . . . . . . . . . . 14
|
67 | 6, 66 | syl 17 |
. . . . . . . . . . . . 13
|
68 | 67 | 3ad2ant1 1082 |
. . . . . . . . . . . 12
|
69 | 14, 19, 65, 68 | mpbir3and 1245 |
. . . . . . . . . . 11
|
70 | | fgcl 21682 |
. . . . . . . . . . 11
|
71 | 69, 70 | syl 17 |
. . . . . . . . . 10
|
72 | | filssufil 21716 |
. . . . . . . . . . 11
|
73 | | snex 4908 |
. . . . . . . . . . . . . . . . . . . . 21
|
74 | | unexg 6959 |
. . . . . . . . . . . . . . . . . . . . 21
|
75 | 73, 74 | mpan2 707 |
. . . . . . . . . . . . . . . . . . . 20
|
76 | | ssfii 8325 |
. . . . . . . . . . . . . . . . . . . 20
|
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
78 | 77 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . 18
|
79 | 78 | unssad 3790 |
. . . . . . . . . . . . . . . . 17
|
80 | | ssfg 21676 |
. . . . . . . . . . . . . . . . . 18
|
81 | 69, 80 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
82 | 79, 81 | sstrd 3613 |
. . . . . . . . . . . . . . . 16
|
83 | 82 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
|
84 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
85 | 83, 84 | sstrd 3613 |
. . . . . . . . . . . . . 14
|
86 | | ufilfil 21708 |
. . . . . . . . . . . . . . . . 17
|
87 | | 0nelfil 21653 |
. . . . . . . . . . . . . . . . 17
|
88 | 86, 87 | syl 17 |
. . . . . . . . . . . . . . . 16
|
89 | 88 | ad2antlr 763 |
. . . . . . . . . . . . . . 15
|
90 | | disjdif 4040 |
. . . . . . . . . . . . . . . . 17
|
91 | 86 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . 18
|
92 | | simprr 796 |
. . . . . . . . . . . . . . . . . 18
|
93 | 77 | unssbd 3791 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
94 | 93 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
95 | 94 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
96 | 69 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
97 | 96, 80 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
98 | 95, 97 | sstrd 3613 |
. . . . . . . . . . . . . . . . . . . . 21
|
99 | 98 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
100 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . 20
|
101 | 99, 100 | sstrd 3613 |
. . . . . . . . . . . . . . . . . . 19
|
102 | | snidg 4206 |
. . . . . . . . . . . . . . . . . . . . . 22
|
103 | 8, 102 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
104 | 103 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . 20
|
105 | 104 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
|
106 | 101, 105 | sseldd 3604 |
. . . . . . . . . . . . . . . . . 18
|
107 | | filin 21658 |
. . . . . . . . . . . . . . . . . 18
|
108 | 91, 92, 106, 107 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
|
109 | 90, 108 | syl5eqelr 2706 |
. . . . . . . . . . . . . . . 16
|
110 | 109 | expr 643 |
. . . . . . . . . . . . . . 15
|
111 | 89, 110 | mtod 189 |
. . . . . . . . . . . . . 14
|
112 | 85, 111 | jca 554 |
. . . . . . . . . . . . 13
|
113 | 112 | exp31 630 |
. . . . . . . . . . . 12
|
114 | 113 | reximdvai 3015 |
. . . . . . . . . . 11
|
115 | 72, 114 | syl5 34 |
. . . . . . . . . 10
|
116 | 71, 115 | mpd 15 |
. . . . . . . . 9
|
117 | 116 | 3expia 1267 |
. . . . . . . 8
|
118 | | filssufil 21716 |
. . . . . . . . . 10
|
119 | | filelss 21656 |
. . . . . . . . . . . . . . . . 17
|
120 | 119 | ex 450 |
. . . . . . . . . . . . . . . 16
|
121 | 86, 120 | syl 17 |
. . . . . . . . . . . . . . 15
|
122 | 121 | con3d 148 |
. . . . . . . . . . . . . 14
|
123 | 122 | impcom 446 |
. . . . . . . . . . . . 13
|
124 | 123 | a1d 25 |
. . . . . . . . . . . 12
|
125 | 124 | ancld 576 |
. . . . . . . . . . 11
|
126 | 125 | reximdva 3017 |
. . . . . . . . . 10
|
127 | 118, 126 | syl5com 31 |
. . . . . . . . 9
|
128 | 127 | adantr 481 |
. . . . . . . 8
|
129 | 117, 128 | pm2.61d 170 |
. . . . . . 7
|
130 | 129 | ex 450 |
. . . . . 6
|
131 | | rexanali 2998 |
. . . . . 6
|
132 | 130, 131 | syl6ib 241 |
. . . . 5
|
133 | 132 | con4d 114 |
. . . 4
|
134 | 2, 133 | syl5bi 232 |
. . 3
|
135 | 134 | ssrdv 3609 |
. 2
|
136 | | ssintub 4495 |
. . 3
|
137 | 136 | a1i 11 |
. 2
|
138 | 135, 137 | eqssd 3620 |
1
|