Step | Hyp | Ref
| Expression |
1 | | ufilfil 21708 |
. . 3
|
2 | | ufilmax 21711 |
. . . . 5
|
3 | 2 | 3expia 1267 |
. . . 4
|
4 | 3 | ralrimiva 2966 |
. . 3
|
5 | 1, 4 | jca 554 |
. 2
|
6 | | simpl 473 |
. . 3
|
7 | | selpw 4165 |
. . . . 5
|
8 | | simpll 790 |
. . . . . . . . . . . . . . . 16
|
9 | | snex 4908 |
. . . . . . . . . . . . . . . 16
|
10 | | unexg 6959 |
. . . . . . . . . . . . . . . 16
|
11 | 8, 9, 10 | sylancl 694 |
. . . . . . . . . . . . . . 15
|
12 | | ssfii 8325 |
. . . . . . . . . . . . . . 15
|
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . 14
|
14 | | filsspw 21655 |
. . . . . . . . . . . . . . . . . 18
|
15 | 14 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
16 | 7 | biimpri 218 |
. . . . . . . . . . . . . . . . . . 19
|
17 | 16 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . 18
|
18 | 17 | snssd 4340 |
. . . . . . . . . . . . . . . . 17
|
19 | 15, 18 | unssd 3789 |
. . . . . . . . . . . . . . . 16
|
20 | | ssun2 3777 |
. . . . . . . . . . . . . . . . . 18
|
21 | | vex 3203 |
. . . . . . . . . . . . . . . . . . 19
|
22 | 21 | snnz 4309 |
. . . . . . . . . . . . . . . . . 18
|
23 | | ssn0 3976 |
. . . . . . . . . . . . . . . . . 18
|
24 | 20, 22, 23 | mp2an 708 |
. . . . . . . . . . . . . . . . 17
|
25 | 24 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
26 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
|
27 | | ineq2 3808 |
. . . . . . . . . . . . . . . . . . . . 21
|
28 | 27 | neeq1d 2853 |
. . . . . . . . . . . . . . . . . . . 20
|
29 | 21, 28 | ralsn 4222 |
. . . . . . . . . . . . . . . . . . 19
|
30 | 29 | ralbii 2980 |
. . . . . . . . . . . . . . . . . 18
|
31 | 26, 30 | sylibr 224 |
. . . . . . . . . . . . . . . . 17
|
32 | | filfbas 21652 |
. . . . . . . . . . . . . . . . . . 19
|
33 | 32 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
|
34 | | simplr 792 |
. . . . . . . . . . . . . . . . . . 19
|
35 | | inss2 3834 |
. . . . . . . . . . . . . . . . . . . 20
|
36 | | filtop 21659 |
. . . . . . . . . . . . . . . . . . . . . 22
|
37 | 36 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
38 | | ineq1 3807 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
39 | 38 | neeq1d 2853 |
. . . . . . . . . . . . . . . . . . . . . 22
|
40 | 39 | rspcva 3307 |
. . . . . . . . . . . . . . . . . . . . 21
|
41 | 37, 40 | sylan 488 |
. . . . . . . . . . . . . . . . . . . 20
|
42 | | ssn0 3976 |
. . . . . . . . . . . . . . . . . . . 20
|
43 | 35, 41, 42 | sylancr 695 |
. . . . . . . . . . . . . . . . . . 19
|
44 | 36 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
|
45 | | snfbas 21670 |
. . . . . . . . . . . . . . . . . . 19
|
46 | 34, 43, 44, 45 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
|
47 | | fbunfip 21673 |
. . . . . . . . . . . . . . . . . 18
|
48 | 33, 46, 47 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
49 | 31, 48 | mpbird 247 |
. . . . . . . . . . . . . . . 16
|
50 | | fsubbas 21671 |
. . . . . . . . . . . . . . . . 17
|
51 | 44, 50 | syl 17 |
. . . . . . . . . . . . . . . 16
|
52 | 19, 25, 49, 51 | mpbir3and 1245 |
. . . . . . . . . . . . . . 15
|
53 | | ssfg 21676 |
. . . . . . . . . . . . . . 15
|
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . 14
|
55 | 13, 54 | sstrd 3613 |
. . . . . . . . . . . . 13
|
56 | 55 | unssad 3790 |
. . . . . . . . . . . 12
|
57 | | fgcl 21682 |
. . . . . . . . . . . . 13
|
58 | | sseq2 3627 |
. . . . . . . . . . . . . . 15
|
59 | | eqeq2 2633 |
. . . . . . . . . . . . . . 15
|
60 | 58, 59 | imbi12d 334 |
. . . . . . . . . . . . . 14
|
61 | 60 | rspcv 3305 |
. . . . . . . . . . . . 13
|
62 | 52, 57, 61 | 3syl 18 |
. . . . . . . . . . . 12
|
63 | 56, 62 | mpid 44 |
. . . . . . . . . . 11
|
64 | | vsnid 4209 |
. . . . . . . . . . . . . . 15
|
65 | 20, 64 | sselii 3600 |
. . . . . . . . . . . . . 14
|
66 | 65 | a1i 11 |
. . . . . . . . . . . . 13
|
67 | 55, 66 | sseldd 3604 |
. . . . . . . . . . . 12
|
68 | | eleq2 2690 |
. . . . . . . . . . . 12
|
69 | 67, 68 | syl5ibrcom 237 |
. . . . . . . . . . 11
|
70 | 63, 69 | syld 47 |
. . . . . . . . . 10
|
71 | 70 | impancom 456 |
. . . . . . . . 9
|
72 | 71 | an32s 846 |
. . . . . . . 8
|
73 | 72 | con3d 148 |
. . . . . . 7
|
74 | | rexnal 2995 |
. . . . . . . . 9
|
75 | | nne 2798 |
. . . . . . . . . . 11
|
76 | | filelss 21656 |
. . . . . . . . . . . . 13
|
77 | | reldisj 4020 |
. . . . . . . . . . . . 13
|
78 | 76, 77 | syl 17 |
. . . . . . . . . . . 12
|
79 | | difss 3737 |
. . . . . . . . . . . . . 14
|
80 | | filss 21657 |
. . . . . . . . . . . . . . 15
|
81 | 80 | 3exp2 1285 |
. . . . . . . . . . . . . 14
|
82 | 79, 81 | mpii 46 |
. . . . . . . . . . . . 13
|
83 | 82 | imp 445 |
. . . . . . . . . . . 12
|
84 | 78, 83 | sylbid 230 |
. . . . . . . . . . 11
|
85 | 75, 84 | syl5bi 232 |
. . . . . . . . . 10
|
86 | 85 | rexlimdva 3031 |
. . . . . . . . 9
|
87 | 74, 86 | syl5bir 233 |
. . . . . . . 8
|
88 | 87 | ad2antrr 762 |
. . . . . . 7
|
89 | 73, 88 | syld 47 |
. . . . . 6
|
90 | 89 | orrd 393 |
. . . . 5
|
91 | 7, 90 | sylan2b 492 |
. . . 4
|
92 | 91 | ralrimiva 2966 |
. . 3
|
93 | | isufil 21707 |
. . 3
|
94 | 6, 92, 93 | sylanbrc 698 |
. 2
|
95 | 5, 94 | impbii 199 |
1
|