Step | Hyp | Ref
| Expression |
1 | | opelxp 4374 |
. . 3
|
2 | | vex 2560 |
. . . . . . 7
|
3 | 2 | elima2 4674 |
. . . . . 6
~Q0
~Q0 |
4 | | elxp 4362 |
. . . . . . . . . 10
|
5 | 4 | anbi1i 431 |
. . . . . . . . 9
~Q0
~Q0 |
6 | | 19.41vv 1783 |
. . . . . . . . 9
~Q0
~Q0 |
7 | 5, 6 | bitr4i 176 |
. . . . . . . 8
~Q0
~Q0 |
8 | | simplr 482 |
. . . . . . . . . . 11
~Q0
|
9 | | breq1 3767 |
. . . . . . . . . . . . 13
~Q0 ~Q0 |
10 | 9 | adantr 261 |
. . . . . . . . . . . 12
~Q0
~Q0 |
11 | 10 | biimpa 280 |
. . . . . . . . . . 11
~Q0
~Q0 |
12 | | id 19 |
. . . . . . . . . . . 12
~Q0
~Q0 |
13 | | enq0er 6533 |
. . . . . . . . . . . . . . 15
~Q0 |
14 | 13 | a1i 9 |
. . . . . . . . . . . . . 14
~Q0
~Q0 |
15 | | simpr 103 |
. . . . . . . . . . . . . 14
~Q0
~Q0 |
16 | 14, 15 | ercl2 6119 |
. . . . . . . . . . . . 13
~Q0
|
17 | | elxp 4362 |
. . . . . . . . . . . . 13
|
18 | 16, 17 | sylib 127 |
. . . . . . . . . . . 12
~Q0
|
19 | | 19.42vv 1788 |
. . . . . . . . . . . 12
~Q0
~Q0
|
20 | 12, 18, 19 | sylanbrc 394 |
. . . . . . . . . . 11
~Q0
~Q0
|
21 | 8, 11, 20 | syl2anc 391 |
. . . . . . . . . 10
~Q0
~Q0
|
22 | | simprrl 491 |
. . . . . . . . . . . . 13
~Q0
|
23 | | elni 6406 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
24 | 23 | simprbi 260 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
25 | 24 | neneqd 2226 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
26 | 25 | ad2antrr 457 |
. . . . . . . . . . . . . . . . . . . . . 22
|
27 | | elni 6406 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
28 | 27 | simprbi 260 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
29 | 28 | neneqd 2226 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
30 | 29 | ad2antll 460 |
. . . . . . . . . . . . . . . . . . . . . 22
|
31 | 26, 30 | jca 290 |
. . . . . . . . . . . . . . . . . . . . 21
|
32 | | pm4.56 806 |
. . . . . . . . . . . . . . . . . . . . 21
|
33 | 31, 32 | sylib 127 |
. . . . . . . . . . . . . . . . . . . 20
|
34 | | pinn 6407 |
. . . . . . . . . . . . . . . . . . . . . 22
|
35 | 34 | ad2antrr 457 |
. . . . . . . . . . . . . . . . . . . . 21
|
36 | | pinn 6407 |
. . . . . . . . . . . . . . . . . . . . . 22
|
37 | 36 | ad2antll 460 |
. . . . . . . . . . . . . . . . . . . . 21
|
38 | | nnm00 6102 |
. . . . . . . . . . . . . . . . . . . . 21
|
39 | 35, 37, 38 | syl2anc 391 |
. . . . . . . . . . . . . . . . . . . 20
|
40 | 33, 39 | mtbird 598 |
. . . . . . . . . . . . . . . . . . 19
|
41 | 40 | ad2ant2rl 480 |
. . . . . . . . . . . . . . . . . 18
~Q0
|
42 | | breq2 3768 |
. . . . . . . . . . . . . . . . . . . . . 22
~Q0 ~Q0 |
43 | 42 | biimpac 282 |
. . . . . . . . . . . . . . . . . . . . 21
~Q0
~Q0 |
44 | 43 | ad2ant2lr 479 |
. . . . . . . . . . . . . . . . . . . 20
~Q0
~Q0 |
45 | | enq0breq 6534 |
. . . . . . . . . . . . . . . . . . . . . 22
~Q0 |
46 | 34, 45 | sylanl1 382 |
. . . . . . . . . . . . . . . . . . . . 21
~Q0 |
47 | 46 | ad2ant2rl 480 |
. . . . . . . . . . . . . . . . . . . 20
~Q0
~Q0
|
48 | 44, 47 | mpbid 135 |
. . . . . . . . . . . . . . . . . . 19
~Q0
|
49 | 48 | eqeq1d 2048 |
. . . . . . . . . . . . . . . . . 18
~Q0
|
50 | 41, 49 | mtbid 597 |
. . . . . . . . . . . . . . . . 17
~Q0
|
51 | | pinn 6407 |
. . . . . . . . . . . . . . . . . . . 20
|
52 | | nnm00 6102 |
. . . . . . . . . . . . . . . . . . . 20
|
53 | 51, 52 | sylan 267 |
. . . . . . . . . . . . . . . . . . 19
|
54 | 53 | ad2ant2lr 479 |
. . . . . . . . . . . . . . . . . 18
|
55 | 54 | ad2ant2rl 480 |
. . . . . . . . . . . . . . . . 17
~Q0
|
56 | 50, 55 | mtbid 597 |
. . . . . . . . . . . . . . . 16
~Q0
|
57 | | pm4.56 806 |
. . . . . . . . . . . . . . . 16
|
58 | 56, 57 | sylibr 137 |
. . . . . . . . . . . . . . 15
~Q0
|
59 | 58 | simprd 107 |
. . . . . . . . . . . . . 14
~Q0
|
60 | 59 | neneqad 2284 |
. . . . . . . . . . . . 13
~Q0
|
61 | | elni 6406 |
. . . . . . . . . . . . 13
|
62 | 22, 60, 61 | sylanbrc 394 |
. . . . . . . . . . . 12
~Q0
|
63 | | simprrr 492 |
. . . . . . . . . . . 12
~Q0
|
64 | | eleq1 2100 |
. . . . . . . . . . . . . 14
|
65 | | opelxp 4374 |
. . . . . . . . . . . . . 14
|
66 | 64, 65 | syl6bb 185 |
. . . . . . . . . . . . 13
|
67 | 66 | ad2antrl 459 |
. . . . . . . . . . . 12
~Q0
|
68 | 62, 63, 67 | mpbir2and 851 |
. . . . . . . . . . 11
~Q0
|
69 | 68 | exlimivv 1776 |
. . . . . . . . . 10
~Q0
|
70 | 21, 69 | syl 14 |
. . . . . . . . 9
~Q0 |
71 | 70 | exlimivv 1776 |
. . . . . . . 8
~Q0 |
72 | 7, 71 | sylbi 114 |
. . . . . . 7
~Q0 |
73 | 72 | exlimiv 1489 |
. . . . . 6
~Q0 |
74 | 3, 73 | sylbi 114 |
. . . . 5
~Q0 |
75 | 74 | ssriv 2949 |
. . . 4
~Q0
|
76 | | ecinxp 6181 |
. . . 4
~Q0
~Q0 ~Q0
|
77 | 75, 76 | mpan 400 |
. . 3
~Q0 ~Q0
|
78 | 1, 77 | sylbir 125 |
. 2
~Q0
~Q0 |
79 | | enq0enq 6529 |
. . 3
~Q0
|
80 | | eceq2 6143 |
. . 3
~Q0
~Q0 |
81 | 79, 80 | ax-mp 7 |
. 2
~Q0 |
82 | 78, 81 | syl6eqr 2090 |
1
~Q0 |