Step | Hyp | Ref
| Expression |
1 | | ineq1 3692 |
. . . . 5
|
2 | 1 | eleq1d 2526 |
. . . 4
|
3 | 2 | imbi2d 316 |
. . 3
|
4 | | elgrug 9191 |
. . . . . 6
|
5 | 4 | ibi 241 |
. . . . 5
|
6 | | trin 4555 |
. . . . . . 7
|
7 | 6 | ex 434 |
. . . . . 6
|
8 | | inss1 3717 |
. . . . . . . 8
|
9 | | ssralv 3563 |
. . . . . . . 8
|
10 | 8, 9 | ax-mp 5 |
. . . . . . 7
|
11 | | inss2 3718 |
. . . . . . . 8
|
12 | | ssralv 3563 |
. . . . . . . 8
|
13 | 11, 12 | ax-mp 5 |
. . . . . . 7
|
14 | | elin 3686 |
. . . . . . . . . . . . 13
|
15 | 14 | simplbi2 625 |
. . . . . . . . . . . 12
|
16 | | ssralv 3563 |
. . . . . . . . . . . . . 14
|
17 | 8, 16 | ax-mp 5 |
. . . . . . . . . . . . 13
|
18 | | ssralv 3563 |
. . . . . . . . . . . . . 14
|
19 | 11, 18 | ax-mp 5 |
. . . . . . . . . . . . 13
|
20 | | elin 3686 |
. . . . . . . . . . . . . . 15
|
21 | 20 | simplbi2 625 |
. . . . . . . . . . . . . 14
|
22 | 21 | ral2imi 2845 |
. . . . . . . . . . . . 13
|
23 | 17, 19, 22 | syl2im 38 |
. . . . . . . . . . . 12
|
24 | 15, 23 | im2anan9 835 |
. . . . . . . . . . 11
|
25 | | vex 3112 |
. . . . . . . . . . . . . 14
|
26 | | mapss 7481 |
. . . . . . . . . . . . . 14
|
27 | 25, 8, 26 | mp2an 672 |
. . . . . . . . . . . . 13
|
28 | | ssralv 3563 |
. . . . . . . . . . . . 13
|
29 | 27, 28 | ax-mp 5 |
. . . . . . . . . . . 12
|
30 | 25 | inex1 4593 |
. . . . . . . . . . . . . . . . 17
|
31 | | vex 3112 |
. . . . . . . . . . . . . . . . 17
|
32 | 30, 31 | elmap 7467 |
. . . . . . . . . . . . . . . 16
|
33 | | fss 5744 |
. . . . . . . . . . . . . . . . 17
|
34 | 11, 33 | mpan2 671 |
. . . . . . . . . . . . . . . 16
|
35 | 32, 34 | sylbi 195 |
. . . . . . . . . . . . . . 15
|
36 | 35 | imim1i 58 |
. . . . . . . . . . . . . 14
|
37 | 36 | alimi 1633 |
. . . . . . . . . . . . 13
|
38 | | df-ral 2812 |
. . . . . . . . . . . . 13
|
39 | 37, 38 | sylibr 212 |
. . . . . . . . . . . 12
|
40 | | elin 3686 |
. . . . . . . . . . . . . 14
|
41 | 40 | simplbi2 625 |
. . . . . . . . . . . . 13
|
42 | 41 | ral2imi 2845 |
. . . . . . . . . . . 12
|
43 | 29, 39, 42 | syl2im 38 |
. . . . . . . . . . 11
|
44 | 24, 43 | im2anan9 835 |
. . . . . . . . . 10
|
45 | 44 | 3impa 1191 |
. . . . . . . . 9
|
46 | | df-3an 975 |
. . . . . . . . 9
|
47 | | df-3an 975 |
. . . . . . . . 9
|
48 | 45, 46, 47 | 3imtr4g 270 |
. . . . . . . 8
|
49 | 48 | ral2imi 2845 |
. . . . . . 7
|
50 | 10, 13, 49 | syl2im 38 |
. . . . . 6
|
51 | 7, 50 | im2anan9 835 |
. . . . 5
|
52 | 5, 51 | syl 16 |
. . . 4
|
53 | | elgrug 9191 |
. . . . 5
|
54 | 30, 53 | ax-mp 5 |
. . . 4
|
55 | 52, 54 | syl6ibr 227 |
. . 3
|
56 | 3, 55 | vtoclga 3173 |
. 2
|
57 | 56 | com12 31 |
1
|