Step | Hyp | Ref
| Expression |
1 | | sspwuni 4416 |
. . . . 5
|
2 | | compss.a |
. . . . . 6
|
3 | 2 | isf34lem1 8773 |
. . . . 5
|
4 | 1, 3 | sylan2b 475 |
. . . 4
|
5 | 4 | adantrr 716 |
. . 3
|
6 | | simplrr 762 |
. . . . . . . . . 10
|
7 | | simprl 756 |
. . . . . . . . . . . . . 14
|
8 | 7 | ad2antrr 725 |
. . . . . . . . . . . . 13
|
9 | | simpr 461 |
. . . . . . . . . . . . 13
|
10 | 8, 9 | eldifd 3486 |
. . . . . . . . . . . 12
|
11 | | simplrr 762 |
. . . . . . . . . . . 12
|
12 | | elunii 4254 |
. . . . . . . . . . . 12
|
13 | 10, 11, 12 | syl2anc 661 |
. . . . . . . . . . 11
|
14 | 13 | ex 434 |
. . . . . . . . . 10
|
15 | 6, 14 | mt3d 125 |
. . . . . . . . 9
|
16 | 15 | expr 615 |
. . . . . . . 8
|
17 | 16 | ralrimiva 2871 |
. . . . . . 7
|
18 | 17 | ex 434 |
. . . . . 6
|
19 | | n0 3794 |
. . . . . . . . 9
|
20 | | simpr 461 |
. . . . . . . . . . . . . . . . 17
|
21 | 20 | sselda 3503 |
. . . . . . . . . . . . . . . 16
|
22 | 21 | elpwid 4022 |
. . . . . . . . . . . . . . 15
|
23 | | dfss4 3731 |
. . . . . . . . . . . . . . 15
|
24 | 22, 23 | sylib 196 |
. . . . . . . . . . . . . 14
|
25 | | simpr 461 |
. . . . . . . . . . . . . 14
|
26 | 24, 25 | eqeltrd 2545 |
. . . . . . . . . . . . 13
|
27 | | difss 3630 |
. . . . . . . . . . . . . . . 16
|
28 | | elpw2g 4615 |
. . . . . . . . . . . . . . . 16
|
29 | 27, 28 | mpbiri 233 |
. . . . . . . . . . . . . . 15
|
30 | 29 | ad2antrr 725 |
. . . . . . . . . . . . . 14
|
31 | | difeq2 3615 |
. . . . . . . . . . . . . . . . 17
|
32 | 31 | eleq1d 2526 |
. . . . . . . . . . . . . . . 16
|
33 | | eleq2 2530 |
. . . . . . . . . . . . . . . 16
|
34 | 32, 33 | imbi12d 320 |
. . . . . . . . . . . . . . 15
|
35 | 34 | rspcv 3206 |
. . . . . . . . . . . . . 14
|
36 | 30, 35 | syl 16 |
. . . . . . . . . . . . 13
|
37 | 26, 36 | mpid 41 |
. . . . . . . . . . . 12
|
38 | | eldifi 3625 |
. . . . . . . . . . . 12
|
39 | 37, 38 | syl6 33 |
. . . . . . . . . . 11
|
40 | 39 | ex 434 |
. . . . . . . . . 10
|
41 | 40 | exlimdv 1724 |
. . . . . . . . 9
|
42 | 19, 41 | syl5bi 217 |
. . . . . . . 8
|
43 | 42 | impr 619 |
. . . . . . 7
|
44 | | eluni 4252 |
. . . . . . . . 9
|
45 | 29 | ad2antrr 725 |
. . . . . . . . . . . . 13
|
46 | 26 | adantlrr 720 |
. . . . . . . . . . . . . . . 16
|
47 | 46 | adantrl 715 |
. . . . . . . . . . . . . . 15
|
48 | | elndif 3627 |
. . . . . . . . . . . . . . . 16
|
49 | 48 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
|
50 | 47, 49 | jca 532 |
. . . . . . . . . . . . . 14
|
51 | | annim 425 |
. . . . . . . . . . . . . 14
|
52 | 50, 51 | sylib 196 |
. . . . . . . . . . . . 13
|
53 | 34 | notbid 294 |
. . . . . . . . . . . . . 14
|
54 | 53 | rspcev 3210 |
. . . . . . . . . . . . 13
|
55 | 45, 52, 54 | syl2anc 661 |
. . . . . . . . . . . 12
|
56 | | rexnal 2905 |
. . . . . . . . . . . 12
|
57 | 55, 56 | sylib 196 |
. . . . . . . . . . 11
|
58 | 57 | ex 434 |
. . . . . . . . . 10
|
59 | 58 | exlimdv 1724 |
. . . . . . . . 9
|
60 | 44, 59 | syl5bi 217 |
. . . . . . . 8
|
61 | 60 | con2d 115 |
. . . . . . 7
|
62 | 43, 61 | jcad 533 |
. . . . . 6
|
63 | 18, 62 | impbid 191 |
. . . . 5
|
64 | | eldif 3485 |
. . . . 5
|
65 | | vex 3112 |
. . . . . 6
|
66 | 65 | elintrab 4298 |
. . . . 5
|
67 | 63, 64, 66 | 3bitr4g 288 |
. . . 4
|
68 | 67 | eqrdv 2454 |
. . 3
|
69 | 5, 68 | eqtrd 2498 |
. 2
|
70 | 2 | compss 8777 |
. . 3
|
71 | 70 | inteqi 4290 |
. 2
|
72 | 69, 71 | syl6eqr 2516 |
1
|