Step | Hyp | Ref
| Expression |
1 | | xpassen.1 |
. . . 4
|
2 | | xpassen.2 |
. . . 4
|
3 | 1, 2 | xpex 6962 |
. . 3
|
4 | | xpassen.3 |
. . 3
|
5 | 3, 4 | xpex 6962 |
. 2
|
6 | 2, 4 | xpex 6962 |
. . 3
|
7 | 1, 6 | xpex 6962 |
. 2
|
8 | | opex 4932 |
. . 3
|
9 | 8 | a1i 11 |
. 2
|
10 | | opex 4932 |
. . 3
|
11 | 10 | a1i 11 |
. 2
|
12 | | sneq 4187 |
. . . . . . . . . . . . . . . . 17
|
13 | 12 | dmeqd 5326 |
. . . . . . . . . . . . . . . 16
|
14 | 13 | unieqd 4446 |
. . . . . . . . . . . . . . 15
|
15 | 14 | sneqd 4189 |
. . . . . . . . . . . . . 14
|
16 | 15 | dmeqd 5326 |
. . . . . . . . . . . . 13
|
17 | 16 | unieqd 4446 |
. . . . . . . . . . . 12
|
18 | | opex 4932 |
. . . . . . . . . . . . . . . . 17
|
19 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
|
20 | 18, 19 | op1sta 5617 |
. . . . . . . . . . . . . . . 16
|
21 | 20 | sneqi 4188 |
. . . . . . . . . . . . . . 15
|
22 | 21 | dmeqi 5325 |
. . . . . . . . . . . . . 14
|
23 | 22 | unieqi 4445 |
. . . . . . . . . . . . 13
|
24 | | vex 3203 |
. . . . . . . . . . . . . 14
|
25 | | vex 3203 |
. . . . . . . . . . . . . 14
|
26 | 24, 25 | op1sta 5617 |
. . . . . . . . . . . . 13
|
27 | 23, 26 | eqtri 2644 |
. . . . . . . . . . . 12
|
28 | 17, 27 | syl6req 2673 |
. . . . . . . . . . 11
|
29 | 15 | rneqd 5353 |
. . . . . . . . . . . . . 14
|
30 | 29 | unieqd 4446 |
. . . . . . . . . . . . 13
|
31 | 21 | rneqi 5352 |
. . . . . . . . . . . . . . 15
|
32 | 31 | unieqi 4445 |
. . . . . . . . . . . . . 14
|
33 | 24, 25 | op2nda 5620 |
. . . . . . . . . . . . . 14
|
34 | 32, 33 | eqtri 2644 |
. . . . . . . . . . . . 13
|
35 | 30, 34 | syl6req 2673 |
. . . . . . . . . . . 12
|
36 | 12 | rneqd 5353 |
. . . . . . . . . . . . . 14
|
37 | 36 | unieqd 4446 |
. . . . . . . . . . . . 13
|
38 | 18, 19 | op2nda 5620 |
. . . . . . . . . . . . 13
|
39 | 37, 38 | syl6req 2673 |
. . . . . . . . . . . 12
|
40 | 35, 39 | opeq12d 4410 |
. . . . . . . . . . 11
|
41 | 28, 40 | opeq12d 4410 |
. . . . . . . . . 10
|
42 | | sneq 4187 |
. . . . . . . . . . . . . . 15
|
43 | 42 | dmeqd 5326 |
. . . . . . . . . . . . . 14
|
44 | 43 | unieqd 4446 |
. . . . . . . . . . . . 13
|
45 | | opex 4932 |
. . . . . . . . . . . . . 14
|
46 | 24, 45 | op1sta 5617 |
. . . . . . . . . . . . 13
|
47 | 44, 46 | syl6req 2673 |
. . . . . . . . . . . 12
|
48 | 42 | rneqd 5353 |
. . . . . . . . . . . . . . . . 17
|
49 | 48 | unieqd 4446 |
. . . . . . . . . . . . . . . 16
|
50 | 49 | sneqd 4189 |
. . . . . . . . . . . . . . 15
|
51 | 50 | dmeqd 5326 |
. . . . . . . . . . . . . 14
|
52 | 51 | unieqd 4446 |
. . . . . . . . . . . . 13
|
53 | 24, 45 | op2nda 5620 |
. . . . . . . . . . . . . . . . 17
|
54 | 53 | sneqi 4188 |
. . . . . . . . . . . . . . . 16
|
55 | 54 | dmeqi 5325 |
. . . . . . . . . . . . . . 15
|
56 | 55 | unieqi 4445 |
. . . . . . . . . . . . . 14
|
57 | 25, 19 | op1sta 5617 |
. . . . . . . . . . . . . 14
|
58 | 56, 57 | eqtri 2644 |
. . . . . . . . . . . . 13
|
59 | 52, 58 | syl6req 2673 |
. . . . . . . . . . . 12
|
60 | 47, 59 | opeq12d 4410 |
. . . . . . . . . . 11
|
61 | 50 | rneqd 5353 |
. . . . . . . . . . . . 13
|
62 | 61 | unieqd 4446 |
. . . . . . . . . . . 12
|
63 | 54 | rneqi 5352 |
. . . . . . . . . . . . . 14
|
64 | 63 | unieqi 4445 |
. . . . . . . . . . . . 13
|
65 | 25, 19 | op2nda 5620 |
. . . . . . . . . . . . 13
|
66 | 64, 65 | eqtri 2644 |
. . . . . . . . . . . 12
|
67 | 62, 66 | syl6req 2673 |
. . . . . . . . . . 11
|
68 | 60, 67 | opeq12d 4410 |
. . . . . . . . . 10
|
69 | 41, 68 | eq2tri 2683 |
. . . . . . . . 9
|
70 | | anass 681 |
. . . . . . . . 9
|
71 | 69, 70 | anbi12i 733 |
. . . . . . . 8
|
72 | | an32 839 |
. . . . . . . 8
|
73 | | an32 839 |
. . . . . . . 8
|
74 | 71, 72, 73 | 3bitr4i 292 |
. . . . . . 7
|
75 | 74 | exbii 1774 |
. . . . . 6
|
76 | | 19.41v 1914 |
. . . . . 6
|
77 | | 19.41v 1914 |
. . . . . 6
|
78 | 75, 76, 77 | 3bitr3i 290 |
. . . . 5
|
79 | 78 | 2exbii 1775 |
. . . 4
|
80 | | 19.41vv 1915 |
. . . 4
|
81 | | 19.41vv 1915 |
. . . 4
|
82 | 79, 80, 81 | 3bitr3i 290 |
. . 3
|
83 | | elxp 5131 |
. . . . 5
|
84 | | excom 2042 |
. . . . 5
|
85 | | elxp 5131 |
. . . . . . . . 9
|
86 | 85 | anbi1i 731 |
. . . . . . . 8
|
87 | | an12 838 |
. . . . . . . 8
|
88 | | 19.41vv 1915 |
. . . . . . . 8
|
89 | 86, 87, 88 | 3bitr4i 292 |
. . . . . . 7
|
90 | 89 | 2exbii 1775 |
. . . . . 6
|
91 | | exrot4 2046 |
. . . . . 6
|
92 | | anass 681 |
. . . . . . . . 9
|
93 | 92 | exbii 1774 |
. . . . . . . 8
|
94 | | opeq1 4402 |
. . . . . . . . . . . 12
|
95 | 94 | eqeq2d 2632 |
. . . . . . . . . . 11
|
96 | 95 | anbi1d 741 |
. . . . . . . . . 10
|
97 | 96 | anbi2d 740 |
. . . . . . . . 9
|
98 | 18, 97 | ceqsexv 3242 |
. . . . . . . 8
|
99 | | an12 838 |
. . . . . . . 8
|
100 | 93, 98, 99 | 3bitri 286 |
. . . . . . 7
|
101 | 100 | 3exbii 1776 |
. . . . . 6
|
102 | 90, 91, 101 | 3bitri 286 |
. . . . 5
|
103 | 83, 84, 102 | 3bitri 286 |
. . . 4
|
104 | 103 | anbi1i 731 |
. . 3
|
105 | | elxp 5131 |
. . . . 5
|
106 | | elxp 5131 |
. . . . . . . . . 10
|
107 | 106 | anbi2i 730 |
. . . . . . . . 9
|
108 | | anass 681 |
. . . . . . . . 9
|
109 | | 19.42vv 1920 |
. . . . . . . . . 10
|
110 | | an12 838 |
. . . . . . . . . . . 12
|
111 | | anass 681 |
. . . . . . . . . . . . 13
|
112 | 111 | anbi2i 730 |
. . . . . . . . . . . 12
|
113 | 110, 112 | bitri 264 |
. . . . . . . . . . 11
|
114 | 113 | 2exbii 1775 |
. . . . . . . . . 10
|
115 | 109, 114 | bitr3i 266 |
. . . . . . . . 9
|
116 | 107, 108,
115 | 3bitr3i 290 |
. . . . . . . 8
|
117 | 116 | exbii 1774 |
. . . . . . 7
|
118 | | exrot3 2045 |
. . . . . . 7
|
119 | | opeq2 4403 |
. . . . . . . . . . 11
|
120 | 119 | eqeq2d 2632 |
. . . . . . . . . 10
|
121 | 120 | anbi1d 741 |
. . . . . . . . 9
|
122 | 45, 121 | ceqsexv 3242 |
. . . . . . . 8
|
123 | 122 | 2exbii 1775 |
. . . . . . 7
|
124 | 117, 118,
123 | 3bitri 286 |
. . . . . 6
|
125 | 124 | exbii 1774 |
. . . . 5
|
126 | 105, 125 | bitri 264 |
. . . 4
|
127 | 126 | anbi1i 731 |
. . 3
|
128 | 82, 104, 127 | 3bitr4i 292 |
. 2
|
129 | 5, 7, 9, 11, 128 | en2i 7993 |
1
|