Step | Hyp | Ref
| Expression |
1 | | df-img 31973 |
. . 3
Img Image
Cart |
2 | 1 | breqi 4659 |
. 2
Img Image
Cart |
3 | | opex 4932 |
. . . 4
|
4 | | brimg.3 |
. . . 4
|
5 | 3, 4 | brco 5292 |
. . 3
Image
Cart
Cart Image
|
6 | | brimg.1 |
. . . . . 6
|
7 | | brimg.2 |
. . . . . 6
|
8 | | vex 3203 |
. . . . . 6
|
9 | 6, 7, 8 | brcart 32039 |
. . . . 5
Cart |
10 | 9 | anbi1i 731 |
. . . 4
Cart Image
Image
|
11 | 10 | exbii 1774 |
. . 3
Cart Image
Image
|
12 | 6, 7 | xpex 6962 |
. . . 4
|
13 | | breq1 4656 |
. . . 4
Image Image |
14 | 12, 13 | ceqsexv 3242 |
. . 3
Image
Image |
15 | 5, 11, 14 | 3bitri 286 |
. 2
Image
Cart
Image |
16 | 12, 4 | brimage 32033 |
. . 3
Image
|
17 | | 19.42v 1918 |
. . . . . . . 8
|
18 | | anass 681 |
. . . . . . . . . . 11
|
19 | | anass 681 |
. . . . . . . . . . . . 13
|
20 | | an12 838 |
. . . . . . . . . . . . 13
|
21 | 19, 20 | bitri 264 |
. . . . . . . . . . . 12
|
22 | 21 | anbi2i 730 |
. . . . . . . . . . 11
|
23 | 18, 22 | bitri 264 |
. . . . . . . . . 10
|
24 | 23 | 2exbii 1775 |
. . . . . . . . 9
|
25 | | excom 2042 |
. . . . . . . . 9
|
26 | | opex 4932 |
. . . . . . . . . . 11
|
27 | | breq1 4656 |
. . . . . . . . . . . . 13
|
28 | 27 | anbi2d 740 |
. . . . . . . . . . . 12
|
29 | 28 | anbi2d 740 |
. . . . . . . . . . 11
|
30 | 26, 29 | ceqsexv 3242 |
. . . . . . . . . 10
|
31 | 30 | exbii 1774 |
. . . . . . . . 9
|
32 | 24, 25, 31 | 3bitri 286 |
. . . . . . . 8
|
33 | | df-br 4654 |
. . . . . . . . . 10
|
34 | | risset 3062 |
. . . . . . . . . . 11
|
35 | | vex 3203 |
. . . . . . . . . . . . . . . 16
|
36 | 35 | brres 5402 |
. . . . . . . . . . . . . . 15
|
37 | | df-br 4654 |
. . . . . . . . . . . . . . 15
|
38 | | ancom 466 |
. . . . . . . . . . . . . . 15
|
39 | 36, 37, 38 | 3bitr3ri 291 |
. . . . . . . . . . . . . 14
|
40 | 39 | anbi2i 730 |
. . . . . . . . . . . . 13
|
41 | | elvv 5177 |
. . . . . . . . . . . . . . . 16
|
42 | 41 | anbi1i 731 |
. . . . . . . . . . . . . . 15
|
43 | | anass 681 |
. . . . . . . . . . . . . . 15
|
44 | | ancom 466 |
. . . . . . . . . . . . . . . . . 18
|
45 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . 21
|
46 | | opeq1 4402 |
. . . . . . . . . . . . . . . . . . . . . 22
|
47 | 46 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . 21
|
48 | 45, 47 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . 20
|
49 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
50 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
51 | 49, 50 | br1steq 31670 |
. . . . . . . . . . . . . . . . . . . . . 22
|
52 | | equcom 1945 |
. . . . . . . . . . . . . . . . . . . . . 22
|
53 | 51, 52 | bitri 264 |
. . . . . . . . . . . . . . . . . . . . 21
|
54 | | opex 4932 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
55 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
56 | 54, 55 | brco 5292 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
57 | | opex 4932 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
58 | 57, 35 | br1steq 31670 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
59 | 58 | anbi1i 731 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
60 | 59 | exbii 1774 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
61 | 56, 60 | bitri 264 |
. . . . . . . . . . . . . . . . . . . . . 22
|
62 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
63 | 57, 62 | ceqsexv 3242 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
64 | 49, 50 | br2ndeq 31671 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
65 | 63, 64 | bitri 264 |
. . . . . . . . . . . . . . . . . . . . . 22
|
66 | | equcom 1945 |
. . . . . . . . . . . . . . . . . . . . . 22
|
67 | 61, 65, 66 | 3bitri 286 |
. . . . . . . . . . . . . . . . . . . . 21
|
68 | 53, 67 | anbi12i 733 |
. . . . . . . . . . . . . . . . . . . 20
|
69 | 48, 68 | syl6bb 276 |
. . . . . . . . . . . . . . . . . . 19
|
70 | 69 | pm5.32i 669 |
. . . . . . . . . . . . . . . . . 18
|
71 | | df-3an 1039 |
. . . . . . . . . . . . . . . . . 18
|
72 | 44, 70, 71 | 3bitr4i 292 |
. . . . . . . . . . . . . . . . 17
|
73 | 72 | 2exbii 1775 |
. . . . . . . . . . . . . . . 16
|
74 | | 19.41vv 1915 |
. . . . . . . . . . . . . . . 16
|
75 | | opeq1 4402 |
. . . . . . . . . . . . . . . . . 18
|
76 | 75 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . 17
|
77 | | opeq2 4403 |
. . . . . . . . . . . . . . . . . 18
|
78 | 77 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . 17
|
79 | 35, 55, 76, 78 | ceqsex2v 3245 |
. . . . . . . . . . . . . . . 16
|
80 | 73, 74, 79 | 3bitr3ri 291 |
. . . . . . . . . . . . . . 15
|
81 | 42, 43, 80 | 3bitr4ri 293 |
. . . . . . . . . . . . . 14
|
82 | | ancom 466 |
. . . . . . . . . . . . . 14
|
83 | 81, 82 | bitri 264 |
. . . . . . . . . . . . 13
|
84 | 55 | brres 5402 |
. . . . . . . . . . . . 13
|
85 | 40, 83, 84 | 3bitr4i 292 |
. . . . . . . . . . . 12
|
86 | 85 | rexbii 3041 |
. . . . . . . . . . 11
|
87 | 34, 86 | bitri 264 |
. . . . . . . . . 10
|
88 | | df-rex 2918 |
. . . . . . . . . 10
|
89 | 33, 87, 88 | 3bitri 286 |
. . . . . . . . 9
|
90 | 89 | anbi2i 730 |
. . . . . . . 8
|
91 | 17, 32, 90 | 3bitr4ri 293 |
. . . . . . 7
|
92 | 91 | exbii 1774 |
. . . . . 6
|
93 | 55 | elima2 5472 |
. . . . . 6
|
94 | 55 | elima2 5472 |
. . . . . . 7
|
95 | | elxp 5131 |
. . . . . . . . . 10
|
96 | 95 | anbi1i 731 |
. . . . . . . . 9
|
97 | | 19.41vv 1915 |
. . . . . . . . 9
|
98 | 96, 97 | bitr4i 267 |
. . . . . . . 8
|
99 | 98 | exbii 1774 |
. . . . . . 7
|
100 | | exrot3 2045 |
. . . . . . . 8
|
101 | | exrot3 2045 |
. . . . . . . 8
|
102 | 100, 101 | bitri 264 |
. . . . . . 7
|
103 | 94, 99, 102 | 3bitri 286 |
. . . . . 6
|
104 | 92, 93, 103 | 3bitr4ri 293 |
. . . . 5
|
105 | 104 | eqriv 2619 |
. . . 4
|
106 | 105 | eqeq2i 2634 |
. . 3
|
107 | 16, 106 | bitri 264 |
. 2
Image
|
108 | 2, 15, 107 | 3bitri 286 |
1
Img |