Step | Hyp | Ref
| Expression |
1 | | elxpi 4379 |
. . . 4
|
2 | | vex 2604 |
. . . . . . . 8
|
3 | | vex 2604 |
. . . . . . . 8
|
4 | 2, 3 | dfop 3569 |
. . . . . . 7
|
5 | | snssi 3529 |
. . . . . . . . . . . . 13
|
6 | | ssun3 3137 |
. . . . . . . . . . . . 13
|
7 | 5, 6 | syl 14 |
. . . . . . . . . . . 12
|
8 | 7 | adantr 270 |
. . . . . . . . . . 11
|
9 | | sseq1 3020 |
. . . . . . . . . . 11
|
10 | 8, 9 | syl5ibrcom 155 |
. . . . . . . . . 10
|
11 | | df-pr 3405 |
. . . . . . . . . . . 12
|
12 | | snssi 3529 |
. . . . . . . . . . . . . . 15
|
13 | | ssun4 3138 |
. . . . . . . . . . . . . . 15
|
14 | 12, 13 | syl 14 |
. . . . . . . . . . . . . 14
|
15 | 7, 14 | anim12i 331 |
. . . . . . . . . . . . 13
|
16 | | unss 3146 |
. . . . . . . . . . . . 13
|
17 | 15, 16 | sylib 120 |
. . . . . . . . . . . 12
|
18 | 11, 17 | syl5eqss 3043 |
. . . . . . . . . . 11
|
19 | | sseq1 3020 |
. . . . . . . . . . 11
|
20 | 18, 19 | syl5ibrcom 155 |
. . . . . . . . . 10
|
21 | 10, 20 | jaod 669 |
. . . . . . . . 9
|
22 | | vex 2604 |
. . . . . . . . . 10
|
23 | 22 | elpr 3419 |
. . . . . . . . 9
|
24 | 22 | elpw 3388 |
. . . . . . . . 9
|
25 | 21, 23, 24 | 3imtr4g 203 |
. . . . . . . 8
|
26 | 25 | ssrdv 3005 |
. . . . . . 7
|
27 | 4, 26 | syl5eqss 3043 |
. . . . . 6
|
28 | | sseq1 3020 |
. . . . . . 7
|
29 | 28 | biimpar 291 |
. . . . . 6
|
30 | 27, 29 | sylan2 280 |
. . . . 5
|
31 | 30 | exlimivv 1817 |
. . . 4
|
32 | 1, 31 | syl 14 |
. . 3
|
33 | 22 | elpw 3388 |
. . 3
|
34 | 32, 33 | sylibr 132 |
. 2
|
35 | 34 | ssriv 3003 |
1
|