Step | Hyp | Ref
| Expression |
1 | | dmresi 5164 |
. . . . . 6
|
2 | | filnet.h |
. . . . . . . . 9
|
3 | | filnet.d |
. . . . . . . . 9
|
4 | 2, 3 | filnetlem2 27271 |
. . . . . . . 8
|
5 | 4 | simpli 446 |
. . . . . . 7
|
6 | | dmss 5043 |
. . . . . . 7
|
7 | 5, 6 | ax-mp 5 |
. . . . . 6
|
8 | 1, 7 | eqsstr3i 3412 |
. . . . 5
|
9 | | ssun1 3543 |
. . . . 5
|
10 | 8, 9 | sstri 3390 |
. . . 4
|
11 | | dmrnssfld 5102 |
. . . 4
|
12 | 10, 11 | sstri 3390 |
. . 3
|
13 | 4 | simpri 450 |
. . . . 5
|
14 | | uniss 4122 |
. . . . 5
|
15 | | uniss 4122 |
. . . . 5
|
16 | 13, 14, 15 | mp2b 10 |
. . . 4
|
17 | | unixpss 4959 |
. . . . 5
|
18 | | unidm 3523 |
. . . . 5
|
19 | 17, 18 | sseqtri 3413 |
. . . 4
|
20 | 16, 19 | sstri 3390 |
. . 3
|
21 | 12, 20 | eqssi 3397 |
. 2
|
22 | | filelss 18388 |
. . . . . . . 8
|
23 | | xpss2 4953 |
. . . . . . . 8
|
24 | 22, 23 | syl 16 |
. . . . . . 7
|
25 | 24 | ralrimiva 2835 |
. . . . . 6
|
26 | | ss2iun 4196 |
. . . . . 6
|
27 | 25, 26 | syl 16 |
. . . . 5
|
28 | | iunxpconst 4899 |
. . . . 5
|
29 | 27, 28 | syl6sseq 3427 |
. . . 4
|
30 | 2, 29 | syl5eqss 3425 |
. . 3
|
31 | 5 | a1i 11 |
. . . . 5
|
32 | 3 | relopabi 4969 |
. . . . 5
|
33 | 31, 32 | jctil 525 |
. . . 4
|
34 | | simpl 445 |
. . . . . . . . . 10
|
35 | 30 | adantr 453 |
. . . . . . . . . . . 12
|
36 | | simprl 734 |
. . . . . . . . . . . 12
|
37 | 35, 36 | sseldd 3382 |
. . . . . . . . . . 11
|
38 | | xp1st 6567 |
. . . . . . . . . . 11
|
39 | 37, 38 | syl 16 |
. . . . . . . . . 10
|
40 | | simprr 735 |
. . . . . . . . . . . 12
|
41 | 35, 40 | sseldd 3382 |
. . . . . . . . . . 11
|
42 | | xp1st 6567 |
. . . . . . . . . . 11
|
43 | 41, 42 | syl 16 |
. . . . . . . . . 10
|
44 | | filinn0 18396 |
. . . . . . . . . 10
|
45 | 34, 39, 43, 44 | syl3anc 1192 |
. . . . . . . . 9
|
46 | | n0 3669 |
. . . . . . . . 9
|
47 | 45, 46 | sylib 190 |
. . . . . . . 8
|
48 | 36 | adantr 453 |
. . . . . . . . . 10
|
49 | | filin 18390 |
. . . . . . . . . . . . . 14
|
50 | 34, 39, 43, 49 | syl3anc 1192 |
. . . . . . . . . . . . 13
|
51 | 50 | adantr 453 |
. . . . . . . . . . . 12
|
52 | | simpr 449 |
. . . . . . . . . . . 12
|
53 | | id 21 |
. . . . . . . . . . . . 13
|
54 | 53 | opeliunxp2 4982 |
. . . . . . . . . . . 12
|
55 | 51, 52, 54 | sylanbrc 647 |
. . . . . . . . . . 11
|
56 | 55, 2 | syl6eleqr 2572 |
. . . . . . . . . 10
|
57 | | fvex 5695 |
. . . . . . . . . . . . . 14
|
58 | 57 | inex1 4443 |
. . . . . . . . . . . . 13
|
59 | | vex 3009 |
. . . . . . . . . . . . 13
|
60 | 58, 59 | op1st 6546 |
. . . . . . . . . . . 12
|
61 | | inss1 3593 |
. . . . . . . . . . . 12
|
62 | 60, 61 | eqsstri 3411 |
. . . . . . . . . . 11
|
63 | | vex 3009 |
. . . . . . . . . . . 12
|
64 | | opex 4563 |
. . . . . . . . . . . 12
|
65 | 2, 3, 63, 64 | filnetlem1 27270 |
. . . . . . . . . . 11
|
66 | 62, 65 | mpbiran2 887 |
. . . . . . . . . 10
|
67 | 48, 56, 66 | sylanbrc 647 |
. . . . . . . . 9
|
68 | 40 | adantr 453 |
. . . . . . . . . 10
|
69 | | inss2 3594 |
. . . . . . . . . . . 12
|
70 | 60, 69 | eqsstri 3411 |
. . . . . . . . . . 11
|
71 | | vex 3009 |
. . . . . . . . . . . 12
|
72 | 2, 3, 71, 64 | filnetlem1 27270 |
. . . . . . . . . . 11
|
73 | 70, 72 | mpbiran2 887 |
. . . . . . . . . 10
|
74 | 68, 56, 73 | sylanbrc 647 |
. . . . . . . . 9
|
75 | | breq2 4306 |
. . . . . . . . . . 11
|
76 | | breq2 4306 |
. . . . . . . . . . 11
|
77 | 75, 76 | anbi12d 693 |
. . . . . . . . . 10
|
78 | 64, 77 | spcev 3093 |
. . . . . . . . 9
|
79 | 67, 74, 78 | syl2anc 644 |
. . . . . . . 8
|
80 | 47, 79 | exlimddv 1658 |
. . . . . . 7
|
81 | 80 | ralrimivva 2844 |
. . . . . 6
|
82 | | codir 5220 |
. . . . . 6
|
83 | 81, 82 | sylibr 205 |
. . . . 5
|
84 | | vex 3009 |
. . . . . . . . . . . . 13
|
85 | 2, 3, 63, 84 | filnetlem1 27270 |
. . . . . . . . . . . 12
|
86 | 85 | simplbi 448 |
. . . . . . . . . . 11
|
87 | 86 | simpld 447 |
. . . . . . . . . 10
|
88 | 2, 3, 84, 71 | filnetlem1 27270 |
. . . . . . . . . . . 12
|
89 | 88 | simplbi 448 |
. . . . . . . . . . 11
|
90 | 89 | simprd 451 |
. . . . . . . . . 10
|
91 | 87, 90 | anim12i 551 |
. . . . . . . . 9
|
92 | 88 | simprbi 452 |
. . . . . . . . . 10
|
93 | 85 | simprbi 452 |
. . . . . . . . . 10
|
94 | 92, 93 | sylan9ssr 3395 |
. . . . . . . . 9
|
95 | 2, 3, 63, 71 | filnetlem1 27270 |
. . . . . . . . 9
|
96 | 91, 94, 95 | sylanbrc 647 |
. . . . . . . 8
|
97 | 96 | ax-gen 1562 |
. . . . . . 7
|
98 | 97 | gen2 1563 |
. . . . . 6
|
99 | | cotr 5212 |
. . . . . 6
|
100 | 98, 99 | mpbir 202 |
. . . . 5
|
101 | 83, 100 | jctil 525 |
. . . 4
|
102 | | filtop 18391 |
. . . . . . . . 9
|
103 | | xpexg 6472 |
. . . . . . . . 9
|
104 | 102, 103 | mpdan 651 |
. . . . . . . 8
|
105 | 104, 30 | ssexd 4449 |
. . . . . . 7
|
106 | | xpexg 6472 |
. . . . . . 7
|
107 | 105, 105,
106 | syl2anc 644 |
. . . . . 6
|
108 | | ssexg 4448 |
. . . . . 6
|
109 | 13, 107, 108 | sylancr 646 |
. . . . 5
|
110 | 21 | isdir 15180 |
. . . . 5
|
111 | 109, 110 | syl 16 |
. . . 4
|
112 | 33, 101, 111 | mpbir2and 890 |
. . 3
|
113 | 30, 112 | jca 520 |
. 2
|
114 | 21, 113 | pm3.2i 443 |
1
|