Step | Hyp | Ref
| Expression |
1 | | eluni2 4440 |
. . . 4
|
2 | | ssel2 3598 |
. . . . . . 7
|
3 | | filelss 21656 |
. . . . . . . 8
|
4 | 3 | ex 450 |
. . . . . . 7
|
5 | 2, 4 | syl 17 |
. . . . . 6
|
6 | 5 | rexlimdva 3031 |
. . . . 5
|
7 | 6 | 3ad2ant1 1082 |
. . . 4
|
8 | 1, 7 | syl5bi 232 |
. . 3
|
9 | 8 | pm4.71rd 667 |
. 2
|
10 | | ssn0 3976 |
. . . 4
|
11 | | fvprc 6185 |
. . . . 5
|
12 | 11 | necon1ai 2821 |
. . . 4
|
13 | 10, 12 | syl 17 |
. . 3
|
14 | 13 | 3adant3 1081 |
. 2
|
15 | | filtop 21659 |
. . . . . . . . 9
|
16 | 2, 15 | syl 17 |
. . . . . . . 8
|
17 | 16 | a1d 25 |
. . . . . . 7
|
18 | 17 | ralimdva 2962 |
. . . . . 6
|
19 | | r19.2z 4060 |
. . . . . . 7
|
20 | 19 | ex 450 |
. . . . . 6
|
21 | 18, 20 | sylan9 689 |
. . . . 5
|
22 | 21 | 3impia 1261 |
. . . 4
|
23 | | eluni2 4440 |
. . . 4
|
24 | 22, 23 | sylibr 224 |
. . 3
|
25 | | sbcel1v 3495 |
. . 3
|
26 | 24, 25 | sylibr 224 |
. 2
|
27 | | 0nelfil 21653 |
. . . . . 6
|
28 | 2, 27 | syl 17 |
. . . . 5
|
29 | 28 | ralrimiva 2966 |
. . . 4
|
30 | 29 | 3ad2ant1 1082 |
. . 3
|
31 | | sbcel1v 3495 |
. . . . . 6
|
32 | | eluni2 4440 |
. . . . . 6
|
33 | 31, 32 | bitri 264 |
. . . . 5
|
34 | 33 | notbii 310 |
. . . 4
|
35 | | ralnex 2992 |
. . . 4
|
36 | 34, 35 | bitr4i 267 |
. . 3
|
37 | 30, 36 | sylibr 224 |
. 2
|
38 | | simp13 1093 |
. . . . 5
|
39 | | r19.29 3072 |
. . . . . 6
|
40 | 39 | ex 450 |
. . . . 5
|
41 | 38, 40 | syl 17 |
. . . 4
|
42 | | simp1 1061 |
. . . . 5
|
43 | | simp1 1061 |
. . . . . . . . 9
|
44 | | simpl 473 |
. . . . . . . . 9
|
45 | 43, 44, 2 | syl2an 494 |
. . . . . . . 8
|
46 | | simprrr 805 |
. . . . . . . 8
|
47 | | simpl2 1065 |
. . . . . . . 8
|
48 | | simpl3 1066 |
. . . . . . . 8
|
49 | | filss 21657 |
. . . . . . . 8
|
50 | 45, 46, 47, 48, 49 | syl13anc 1328 |
. . . . . . 7
|
51 | 50 | expr 643 |
. . . . . 6
|
52 | 51 | reximdva 3017 |
. . . . 5
|
53 | 42, 52 | syl3an1 1359 |
. . . 4
|
54 | 41, 53 | syld 47 |
. . 3
|
55 | | sbcel1v 3495 |
. . . 4
|
56 | 55, 1 | bitri 264 |
. . 3
|
57 | | sbcel1v 3495 |
. . . 4
|
58 | | eluni2 4440 |
. . . 4
|
59 | 57, 58 | bitri 264 |
. . 3
|
60 | 54, 56, 59 | 3imtr4g 285 |
. 2
|
61 | | simp13 1093 |
. . . . 5
|
62 | | r19.29 3072 |
. . . . . 6
|
63 | 62 | ex 450 |
. . . . 5
|
64 | 61, 63 | syl 17 |
. . . 4
|
65 | | simp11 1091 |
. . . . 5
|
66 | | r19.29 3072 |
. . . . . . . . . . 11
|
67 | 66 | ex 450 |
. . . . . . . . . 10
|
68 | | elun1 3780 |
. . . . . . . . . . . . . . . 16
|
69 | | elun2 3781 |
. . . . . . . . . . . . . . . 16
|
70 | 68, 69 | anim12i 590 |
. . . . . . . . . . . . . . 15
|
71 | | eleq2 2690 |
. . . . . . . . . . . . . . . . 17
|
72 | | eleq2 2690 |
. . . . . . . . . . . . . . . . 17
|
73 | 71, 72 | anbi12d 747 |
. . . . . . . . . . . . . . . 16
|
74 | 73 | rspcev 3309 |
. . . . . . . . . . . . . . 15
|
75 | 70, 74 | sylan2 491 |
. . . . . . . . . . . . . 14
|
76 | 75 | an12s 843 |
. . . . . . . . . . . . 13
|
77 | 76 | ex 450 |
. . . . . . . . . . . 12
|
78 | 77 | ad2antlr 763 |
. . . . . . . . . . 11
|
79 | 78 | rexlimdva 3031 |
. . . . . . . . . 10
|
80 | 67, 79 | syl9r 78 |
. . . . . . . . 9
|
81 | 80 | impr 649 |
. . . . . . . 8
|
82 | 81 | ancom2s 844 |
. . . . . . 7
|
83 | 82 | rexlimiva 3028 |
. . . . . 6
|
84 | 83 | imp 445 |
. . . . 5
|
85 | | ssel2 3598 |
. . . . . . 7
|
86 | | filin 21658 |
. . . . . . . 8
|
87 | 86 | 3expib 1268 |
. . . . . . 7
|
88 | 85, 87 | syl 17 |
. . . . . 6
|
89 | 88 | reximdva 3017 |
. . . . 5
|
90 | 65, 84, 89 | syl2im 40 |
. . . 4
|
91 | 64, 90 | syland 498 |
. . 3
|
92 | | eluni2 4440 |
. . . . 5
|
93 | 55, 92 | bitri 264 |
. . . 4
|
94 | 59, 93 | anbi12i 733 |
. . 3
|
95 | | sbcel1v 3495 |
. . . 4
|
96 | | eluni2 4440 |
. . . 4
|
97 | 95, 96 | bitri 264 |
. . 3
|
98 | 91, 94, 97 | 3imtr4g 285 |
. 2
|
99 | 9, 14, 26, 37, 60, 98 | isfild 21662 |
1
|