Step | Hyp | Ref
| Expression |
1 | | dfac3 8944 |
. . 3
CHOICE
|
2 | | nfra1 2941 |
. . . . . . 7
|
3 | | rsp 2929 |
. . . . . . . . . . . . 13
|
4 | | equid 1939 |
. . . . . . . . . . . . . . . . . . 19
|
5 | | neeq1 2856 |
. . . . . . . . . . . . . . . . . . . . 21
|
6 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . 21
|
7 | 5, 6 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . 20
|
8 | 7 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . 19
|
9 | 4, 8 | mpanr2 720 |
. . . . . . . . . . . . . . . . . 18
|
10 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
|
11 | 10 | preq1d 4274 |
. . . . . . . . . . . . . . . . . . . . 21
|
12 | | preq2 4269 |
. . . . . . . . . . . . . . . . . . . . 21
|
13 | 11, 12 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . . . 20
|
14 | 13 | anim2i 593 |
. . . . . . . . . . . . . . . . . . 19
|
15 | 14 | reximi 3011 |
. . . . . . . . . . . . . . . . . 18
|
16 | 9, 15 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
17 | | prex 4909 |
. . . . . . . . . . . . . . . . . 18
|
18 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . 20
|
19 | 18 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . 19
|
20 | 19 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . 18
|
21 | 17, 20 | elab 3350 |
. . . . . . . . . . . . . . . . 17
|
22 | 16, 21 | sylibr 224 |
. . . . . . . . . . . . . . . 16
|
23 | | vex 3203 |
. . . . . . . . . . . . . . . . . 18
|
24 | 23 | prid2 4298 |
. . . . . . . . . . . . . . . . 17
|
25 | | fvex 6201 |
. . . . . . . . . . . . . . . . . 18
|
26 | 25 | prid1 4297 |
. . . . . . . . . . . . . . . . 17
|
27 | 24, 26 | pm3.2i 471 |
. . . . . . . . . . . . . . . 16
|
28 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . 18
|
29 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . 18
|
30 | 28, 29 | anbi12d 747 |
. . . . . . . . . . . . . . . . 17
|
31 | 30 | rspcev 3309 |
. . . . . . . . . . . . . . . 16
|
32 | 22, 27, 31 | sylancl 694 |
. . . . . . . . . . . . . . 15
|
33 | | eleq1 2689 |
. . . . . . . . . . . . . . . . 17
|
34 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . 19
|
35 | 34 | anbi2d 740 |
. . . . . . . . . . . . . . . . . 18
|
36 | 35 | rexbidv 3052 |
. . . . . . . . . . . . . . . . 17
|
37 | 33, 36 | anbi12d 747 |
. . . . . . . . . . . . . . . 16
|
38 | 25, 37 | spcev 3300 |
. . . . . . . . . . . . . . 15
|
39 | 32, 38 | sylan2 491 |
. . . . . . . . . . . . . 14
|
40 | 39 | ex 450 |
. . . . . . . . . . . . 13
|
41 | 3, 40 | syl8 76 |
. . . . . . . . . . . 12
|
42 | 41 | impd 447 |
. . . . . . . . . . 11
|
43 | 42 | pm2.43d 53 |
. . . . . . . . . 10
|
44 | | df-rex 2918 |
. . . . . . . . . . . . . 14
|
45 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . 20
|
46 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . 22
|
47 | 46 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . . . 21
|
48 | 47 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . 20
|
49 | 45, 48 | elab 3350 |
. . . . . . . . . . . . . . . . . . 19
|
50 | | neeq1 2856 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
51 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
52 | 51 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
53 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
54 | 52, 53 | bitrd 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
55 | 50, 54 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
56 | 55 | rspccv 3306 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
57 | | elirrv 8504 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
58 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
59 | 57, 58 | mtbii 316 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
60 | 59 | con2i 134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
61 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
62 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
63 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
64 | 61, 23, 62, 63 | prel12 4383 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
65 | | ancom 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
66 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
67 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
68 | 66, 67 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
69 | 65, 68 | syl5rbbr 275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
70 | 64, 69 | sylan9bbr 737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
71 | 60, 70 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
72 | 71 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
73 | 72 | pm5.32da 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
74 | 61, 23, 62, 63 | preleq 8514 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
75 | 73, 74 | syl6bir 244 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
76 | 51 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
77 | 76 | biimparc 504 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
78 | 75, 77 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
79 | 78 | exp4c 636 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
80 | 79 | com13 88 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
81 | 56, 80 | syl8 76 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
82 | 81 | com4r 94 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
83 | 82 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . 22
|
84 | 83 | imp4a 614 |
. . . . . . . . . . . . . . . . . . . . 21
|
85 | 84 | com3l 89 |
. . . . . . . . . . . . . . . . . . . 20
|
86 | 85 | rexlimiv 3027 |
. . . . . . . . . . . . . . . . . . 19
|
87 | 49, 86 | sylbi 207 |
. . . . . . . . . . . . . . . . . 18
|
88 | 87 | expd 452 |
. . . . . . . . . . . . . . . . 17
|
89 | 88 | com13 88 |
. . . . . . . . . . . . . . . 16
|
90 | 89 | imp4b 613 |
. . . . . . . . . . . . . . 15
|
91 | 90 | exlimdv 1861 |
. . . . . . . . . . . . . 14
|
92 | 44, 91 | syl5bi 232 |
. . . . . . . . . . . . 13
|
93 | 92 | expimpd 629 |
. . . . . . . . . . . 12
|
94 | 93 | alrimiv 1855 |
. . . . . . . . . . 11
|
95 | | mo2icl 3385 |
. . . . . . . . . . 11
|
96 | 94, 95 | syl 17 |
. . . . . . . . . 10
|
97 | 43, 96 | jctird 567 |
. . . . . . . . 9
|
98 | | df-reu 2919 |
. . . . . . . . . 10
|
99 | | eu5 2496 |
. . . . . . . . . 10
|
100 | 98, 99 | bitri 264 |
. . . . . . . . 9
|
101 | 97, 100 | syl6ibr 242 |
. . . . . . . 8
|
102 | 101 | expd 452 |
. . . . . . 7
|
103 | 2, 102 | ralrimi 2957 |
. . . . . 6
|
104 | | vex 3203 |
. . . . . . . . . . . 12
|
105 | 104 | rnex 7100 |
. . . . . . . . . . 11
|
106 | | p0ex 4853 |
. . . . . . . . . . 11
|
107 | 105, 106 | unex 6956 |
. . . . . . . . . 10
|
108 | | vex 3203 |
. . . . . . . . . 10
|
109 | 107, 108 | unex 6956 |
. . . . . . . . 9
|
110 | 109 | pwex 4848 |
. . . . . . . 8
|
111 | | ssun1 3776 |
. . . . . . . . . . . . . . 15
|
112 | | fvrn0 6216 |
. . . . . . . . . . . . . . 15
|
113 | 111, 112 | sselii 3600 |
. . . . . . . . . . . . . 14
|
114 | | elun2 3781 |
. . . . . . . . . . . . . 14
|
115 | | prssi 4353 |
. . . . . . . . . . . . . 14
|
116 | 113, 114,
115 | sylancr 695 |
. . . . . . . . . . . . 13
|
117 | | prex 4909 |
. . . . . . . . . . . . . 14
|
118 | 117 | elpw 4164 |
. . . . . . . . . . . . 13
|
119 | 116, 118 | sylibr 224 |
. . . . . . . . . . . 12
|
120 | | eleq1 2689 |
. . . . . . . . . . . 12
|
121 | 119, 120 | syl5ibrcom 237 |
. . . . . . . . . . 11
|
122 | 121 | adantld 483 |
. . . . . . . . . 10
|
123 | 122 | rexlimiv 3027 |
. . . . . . . . 9
|
124 | 123 | abssi 3677 |
. . . . . . . 8
|
125 | 110, 124 | ssexi 4803 |
. . . . . . 7
|
126 | | rexeq 3139 |
. . . . . . . . . 10
|
127 | 126 | reubidv 3126 |
. . . . . . . . 9
|
128 | 127 | imbi2d 330 |
. . . . . . . 8
|
129 | 128 | ralbidv 2986 |
. . . . . . 7
|
130 | 125, 129 | spcev 3300 |
. . . . . 6
|
131 | 103, 130 | syl 17 |
. . . . 5
|
132 | 131 | exlimiv 1858 |
. . . 4
|
133 | 132 | alimi 1739 |
. . 3
|
134 | 1, 133 | sylbi 207 |
. 2
CHOICE |
135 | | dfac2a 8952 |
. 2
CHOICE |
136 | 134, 135 | impbii 199 |
1
CHOICE
|