Step | Hyp | Ref
| Expression |
1 | | opelxpi 4631 |
. . . 4
|
2 | | enq0ex 7372 |
. . . . 5
~Q0 |
3 | 2 | ecelqsi 6547 |
. . . 4
~Q0
~Q0 |
4 | 1, 3 | syl 14 |
. . 3
~Q0
~Q0 |
5 | | opelxpi 4631 |
. . . 4
|
6 | 2 | ecelqsi 6547 |
. . . 4
~Q0
~Q0 |
7 | 5, 6 | syl 14 |
. . 3
~Q0
~Q0 |
8 | 4, 7 | anim12i 336 |
. 2
~Q0
~Q0
~Q0
~Q0 |
9 | | eqid 2164 |
. . . 4
~Q0
~Q0 |
10 | | eqid 2164 |
. . . 4
~Q0
~Q0 |
11 | 9, 10 | pm3.2i 270 |
. . 3
~Q0 ~Q0 ~Q0 ~Q0 |
12 | | eqid 2164 |
. . 3
~Q0
~Q0 |
13 | | opeq12 3755 |
. . . . . 6
|
14 | | eceq1 6528 |
. . . . . . . . 9
~Q0
~Q0 |
15 | 14 | eqeq2d 2176 |
. . . . . . . 8
~Q0
~Q0 ~Q0 ~Q0 |
16 | 15 | anbi1d 461 |
. . . . . . 7
~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0
~Q0
~Q0 |
17 | | vex 2725 |
. . . . . . . . . . 11
|
18 | | vex 2725 |
. . . . . . . . . . 11
|
19 | 17, 18 | opth 4210 |
. . . . . . . . . 10
|
20 | | oveq1 5844 |
. . . . . . . . . . . 12
|
21 | 20 | adantr 274 |
. . . . . . . . . . 11
|
22 | | oveq1 5844 |
. . . . . . . . . . . 12
|
23 | 22 | adantl 275 |
. . . . . . . . . . 11
|
24 | 21, 23 | opeq12d 3761 |
. . . . . . . . . 10
|
25 | 19, 24 | sylbi 120 |
. . . . . . . . 9
|
26 | 25 | eceq1d 6529 |
. . . . . . . 8
~Q0
~Q0 |
27 | 26 | eqeq2d 2176 |
. . . . . . 7
~Q0
~Q0 ~Q0 ~Q0 |
28 | 16, 27 | anbi12d 465 |
. . . . . 6
~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0 ~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0 |
29 | 13, 28 | syl 14 |
. . . . 5
~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0 ~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0 |
30 | 29 | spc2egv 2812 |
. . . 4
~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0
~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0 |
31 | | opeq12 3755 |
. . . . . . 7
|
32 | | eceq1 6528 |
. . . . . . . . . 10
~Q0
~Q0 |
33 | 32 | eqeq2d 2176 |
. . . . . . . . 9
~Q0
~Q0 ~Q0 ~Q0 |
34 | 33 | anbi2d 460 |
. . . . . . . 8
~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0
~Q0
~Q0 |
35 | | vex 2725 |
. . . . . . . . . . . 12
|
36 | | vex 2725 |
. . . . . . . . . . . 12
|
37 | 35, 36 | opth 4210 |
. . . . . . . . . . 11
|
38 | | oveq2 5845 |
. . . . . . . . . . . . 13
|
39 | 38 | adantr 274 |
. . . . . . . . . . . 12
|
40 | | oveq2 5845 |
. . . . . . . . . . . . 13
|
41 | 40 | adantl 275 |
. . . . . . . . . . . 12
|
42 | 39, 41 | opeq12d 3761 |
. . . . . . . . . . 11
|
43 | 37, 42 | sylbi 120 |
. . . . . . . . . 10
|
44 | 43 | eceq1d 6529 |
. . . . . . . . 9
~Q0
~Q0 |
45 | 44 | eqeq2d 2176 |
. . . . . . . 8
~Q0
~Q0 ~Q0 ~Q0 |
46 | 34, 45 | anbi12d 465 |
. . . . . . 7
~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0 ~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0 |
47 | 31, 46 | syl 14 |
. . . . . 6
~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0 ~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0 |
48 | 47 | spc2egv 2812 |
. . . . 5
~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0
~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0 |
49 | 48 | 2eximdv 1869 |
. . . 4
~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0
~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0 |
50 | 30, 49 | sylan9 407 |
. . 3
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0 |
51 | 11, 12, 50 | mp2ani 429 |
. 2
~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0 |
52 | | ecexg 6497 |
. . . 4
~Q0
~Q0 |
53 | 2, 52 | ax-mp 5 |
. . 3
~Q0 |
54 | | eqeq1 2171 |
. . . . . . . 8
~Q0 ~Q0 ~Q0 ~Q0 |
55 | | eqeq1 2171 |
. . . . . . . 8
~Q0 ~Q0 ~Q0 ~Q0 |
56 | 54, 55 | bi2anan9 596 |
. . . . . . 7
~Q0 ~Q0 ~Q0
~Q0
~Q0
~Q0
~Q0
~Q0 |
57 | | eqeq1 2171 |
. . . . . . 7
~Q0 ~Q0 ~Q0 ~Q0 |
58 | 56, 57 | bi2anan9 596 |
. . . . . 6
~Q0
~Q0 ~Q0
~Q0 ~Q0 ~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0 |
59 | 58 | 3impa 1183 |
. . . . 5
~Q0 ~Q0
~Q0
~Q0
~Q0 ~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0 |
60 | 59 | 4exbidv 1857 |
. . . 4
~Q0 ~Q0
~Q0
~Q0 ~Q0 ~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0 |
61 | | mulnq0mo 7381 |
. . . 4
~Q0 ~Q0 ~Q0
~Q0 ~Q0 |
62 | | dfmq0qs 7362 |
. . . 4
·Q0
~Q0 ~Q0
~Q0 ~Q0 ~Q0 |
63 | 60, 61, 62 | ovig 5955 |
. . 3
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
·Q0 ~Q0
~Q0 |
64 | 53, 63 | mp3an3 1315 |
. 2
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
·Q0 ~Q0
~Q0 |
65 | 8, 51, 64 | sylc 62 |
1
~Q0
·Q0 ~Q0
~Q0 |