Step | Hyp | Ref
| Expression |
1 | | ssralv 3666 |
. . . . 5
|
2 | | dfon2lem8 31695 |
. . . . . . . 8
|
3 | 2 | simprd 479 |
. . . . . . 7
|
4 | | intss1 4492 |
. . . . . . . . 9
|
5 | 2 | simpld 475 |
. . . . . . . . . 10
|
6 | | intex 4820 |
. . . . . . . . . . 11
|
7 | | dfon2lem3 31690 |
. . . . . . . . . . . . . . . . 17
|
8 | 7 | imp 445 |
. . . . . . . . . . . . . . . 16
|
9 | 8 | simprd 479 |
. . . . . . . . . . . . . . 15
|
10 | | untelirr 31585 |
. . . . . . . . . . . . . . 15
|
11 | 9, 10 | syl 17 |
. . . . . . . . . . . . . 14
|
12 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
|
13 | 12 | notbid 308 |
. . . . . . . . . . . . . 14
|
14 | 11, 13 | syl5ibcom 235 |
. . . . . . . . . . . . 13
|
15 | 14 | a1dd 50 |
. . . . . . . . . . . 12
|
16 | 8 | simpld 475 |
. . . . . . . . . . . . . . . . 17
|
17 | | trss 4761 |
. . . . . . . . . . . . . . . . 17
|
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . . . 16
|
19 | | eqss 3618 |
. . . . . . . . . . . . . . . . 17
|
20 | 19 | simplbi2com 657 |
. . . . . . . . . . . . . . . 16
|
21 | 18, 20 | syl6 35 |
. . . . . . . . . . . . . . 15
|
22 | 21 | com23 86 |
. . . . . . . . . . . . . 14
|
23 | | con3 149 |
. . . . . . . . . . . . . 14
|
24 | 22, 23 | syl6 35 |
. . . . . . . . . . . . 13
|
25 | 24 | com23 86 |
. . . . . . . . . . . 12
|
26 | 15, 25 | pm2.61d 170 |
. . . . . . . . . . 11
|
27 | 6, 26 | sylanb 489 |
. . . . . . . . . 10
|
28 | 5, 27 | syldan 487 |
. . . . . . . . 9
|
29 | 4, 28 | syl5 34 |
. . . . . . . 8
|
30 | 29 | ralrimiv 2965 |
. . . . . . 7
|
31 | | eleq2 2690 |
. . . . . . . . . 10
|
32 | 31 | notbid 308 |
. . . . . . . . 9
|
33 | 32 | ralbidv 2986 |
. . . . . . . 8
|
34 | 33 | rspcev 3309 |
. . . . . . 7
|
35 | 3, 30, 34 | syl2anc 693 |
. . . . . 6
|
36 | 35 | expcom 451 |
. . . . 5
|
37 | 1, 36 | syl6com 37 |
. . . 4
|
38 | 37 | impd 447 |
. . 3
|
39 | 38 | alrimiv 1855 |
. 2
|
40 | | df-fr 5073 |
. . 3
|
41 | | epel 5032 |
. . . . . . . 8
|
42 | 41 | notbii 310 |
. . . . . . 7
|
43 | 42 | ralbii 2980 |
. . . . . 6
|
44 | 43 | rexbii 3041 |
. . . . 5
|
45 | 44 | imbi2i 326 |
. . . 4
|
46 | 45 | albii 1747 |
. . 3
|
47 | 40, 46 | bitri 264 |
. 2
|
48 | 39, 47 | sylibr 224 |
1
|