Step | Hyp | Ref
| Expression |
1 | | elxpi 4555 |
. . . 4
|
2 | | vex 2689 |
. . . . . . . 8
|
3 | | vex 2689 |
. . . . . . . 8
|
4 | 2, 3 | dfop 3704 |
. . . . . . 7
|
5 | | snssi 3664 |
. . . . . . . . . . . . 13
|
6 | | ssun3 3241 |
. . . . . . . . . . . . 13
|
7 | 5, 6 | syl 14 |
. . . . . . . . . . . 12
|
8 | 7 | adantr 274 |
. . . . . . . . . . 11
|
9 | | sseq1 3120 |
. . . . . . . . . . 11
|
10 | 8, 9 | syl5ibrcom 156 |
. . . . . . . . . 10
|
11 | | df-pr 3534 |
. . . . . . . . . . . 12
|
12 | | snssi 3664 |
. . . . . . . . . . . . . . 15
|
13 | | ssun4 3242 |
. . . . . . . . . . . . . . 15
|
14 | 12, 13 | syl 14 |
. . . . . . . . . . . . . 14
|
15 | 7, 14 | anim12i 336 |
. . . . . . . . . . . . 13
|
16 | | unss 3250 |
. . . . . . . . . . . . 13
|
17 | 15, 16 | sylib 121 |
. . . . . . . . . . . 12
|
18 | 11, 17 | eqsstrid 3143 |
. . . . . . . . . . 11
|
19 | | sseq1 3120 |
. . . . . . . . . . 11
|
20 | 18, 19 | syl5ibrcom 156 |
. . . . . . . . . 10
|
21 | 10, 20 | jaod 706 |
. . . . . . . . 9
|
22 | | vex 2689 |
. . . . . . . . . 10
|
23 | 22 | elpr 3548 |
. . . . . . . . 9
|
24 | 22 | elpw 3516 |
. . . . . . . . 9
|
25 | 21, 23, 24 | 3imtr4g 204 |
. . . . . . . 8
|
26 | 25 | ssrdv 3103 |
. . . . . . 7
|
27 | 4, 26 | eqsstrid 3143 |
. . . . . 6
|
28 | | sseq1 3120 |
. . . . . . 7
|
29 | 28 | biimpar 295 |
. . . . . 6
|
30 | 27, 29 | sylan2 284 |
. . . . 5
|
31 | 30 | exlimivv 1868 |
. . . 4
|
32 | 1, 31 | syl 14 |
. . 3
|
33 | 22 | elpw 3516 |
. . 3
|
34 | 32, 33 | sylibr 133 |
. 2
|
35 | 34 | ssriv 3101 |
1
|