Proof of Theorem br8d
Step | Hyp | Ref
| Expression |
1 | | br8d.10 |
. . . 4
|
2 | 1 | breqd 4664 |
. . 3
|
3 | | opex 4932 |
. . . 4
|
4 | | opex 4932 |
. . . 4
|
5 | | eqeq1 2626 |
. . . . . . . . . 10
|
6 | 5 | 3anbi1d 1403 |
. . . . . . . . 9
|
7 | 6 | rexbidv 3052 |
. . . . . . . 8
|
8 | 7 | 2rexbidv 3057 |
. . . . . . 7
|
9 | 8 | 2rexbidv 3057 |
. . . . . 6
|
10 | 9 | 2rexbidv 3057 |
. . . . 5
|
11 | 10 | rexbidv 3052 |
. . . 4
|
12 | | eqeq1 2626 |
. . . . . . . . . 10
|
13 | 12 | 3anbi2d 1404 |
. . . . . . . . 9
|
14 | 13 | rexbidv 3052 |
. . . . . . . 8
|
15 | 14 | 2rexbidv 3057 |
. . . . . . 7
|
16 | 15 | 2rexbidv 3057 |
. . . . . 6
|
17 | 16 | 2rexbidv 3057 |
. . . . 5
|
18 | 17 | rexbidv 3052 |
. . . 4
|
19 | | eqid 2622 |
. . . 4
|
20 | 3, 4, 11, 18, 19 | brab 4998 |
. . 3
|
21 | 2, 20 | syl6bb 276 |
. 2
|
22 | | br8d.11 |
. . 3
|
23 | | br8d.12 |
. . 3
|
24 | | br8d.13 |
. . 3
|
25 | | br8d.14 |
. . 3
|
26 | | br8d.15 |
. . 3
|
27 | | br8d.16 |
. . 3
|
28 | | br8d.17 |
. . 3
|
29 | | br8d.18 |
. . 3
|
30 | | opex 4932 |
. . . . . . . . . . . . . . 15
|
31 | | opex 4932 |
. . . . . . . . . . . . . . 15
|
32 | 30, 31 | opth 4945 |
. . . . . . . . . . . . . 14
|
33 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
|
34 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
|
35 | 33, 34 | opth 4945 |
. . . . . . . . . . . . . . . 16
|
36 | | br8d.1 |
. . . . . . . . . . . . . . . . 17
|
37 | | br8d.2 |
. . . . . . . . . . . . . . . . 17
|
38 | 36, 37 | sylan9bb 736 |
. . . . . . . . . . . . . . . 16
|
39 | 35, 38 | sylbi 207 |
. . . . . . . . . . . . . . 15
|
40 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
|
41 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
|
42 | 40, 41 | opth 4945 |
. . . . . . . . . . . . . . . 16
|
43 | | br8d.3 |
. . . . . . . . . . . . . . . . 17
|
44 | | br8d.4 |
. . . . . . . . . . . . . . . . 17
|
45 | 43, 44 | sylan9bb 736 |
. . . . . . . . . . . . . . . 16
|
46 | 42, 45 | sylbi 207 |
. . . . . . . . . . . . . . 15
|
47 | 39, 46 | sylan9bb 736 |
. . . . . . . . . . . . . 14
|
48 | 32, 47 | sylbi 207 |
. . . . . . . . . . . . 13
|
49 | 48 | eqcoms 2630 |
. . . . . . . . . . . 12
|
50 | | opex 4932 |
. . . . . . . . . . . . . . 15
|
51 | | opex 4932 |
. . . . . . . . . . . . . . 15
|
52 | 50, 51 | opth 4945 |
. . . . . . . . . . . . . 14
|
53 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
|
54 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
|
55 | 53, 54 | opth 4945 |
. . . . . . . . . . . . . . . 16
|
56 | | br8d.5 |
. . . . . . . . . . . . . . . . 17
|
57 | | br8d.6 |
. . . . . . . . . . . . . . . . 17
|
58 | 56, 57 | sylan9bb 736 |
. . . . . . . . . . . . . . . 16
|
59 | 55, 58 | sylbi 207 |
. . . . . . . . . . . . . . 15
|
60 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
|
61 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
|
62 | 60, 61 | opth 4945 |
. . . . . . . . . . . . . . . 16
|
63 | | br8d.7 |
. . . . . . . . . . . . . . . . 17
|
64 | | br8d.8 |
. . . . . . . . . . . . . . . . 17
|
65 | 63, 64 | sylan9bb 736 |
. . . . . . . . . . . . . . . 16
|
66 | 62, 65 | sylbi 207 |
. . . . . . . . . . . . . . 15
|
67 | 59, 66 | sylan9bb 736 |
. . . . . . . . . . . . . 14
|
68 | 52, 67 | sylbi 207 |
. . . . . . . . . . . . 13
|
69 | 68 | eqcoms 2630 |
. . . . . . . . . . . 12
|
70 | 49, 69 | sylan9bb 736 |
. . . . . . . . . . 11
|
71 | 70 | biimp3a 1432 |
. . . . . . . . . 10
|
72 | 71 | a1i 11 |
. . . . . . . . 9
|
73 | 72 | rexlimdva 3031 |
. . . . . . . 8
|
74 | 73 | rexlimdvva 3038 |
. . . . . . 7
|
75 | 74 | rexlimdvva 3038 |
. . . . . 6
|
76 | 75 | rexlimdvva 3038 |
. . . . 5
|
77 | 76 | rexlimdva 3031 |
. . . 4
|
78 | | simpl1l 1112 |
. . . . . 6
|
79 | | simpl1r 1113 |
. . . . . 6
|
80 | | simpl21 1139 |
. . . . . 6
|
81 | | simpl22 1140 |
. . . . . . 7
|
82 | | simpl23 1141 |
. . . . . . 7
|
83 | | simpl31 1142 |
. . . . . . 7
|
84 | | simpl32 1143 |
. . . . . . . 8
|
85 | | simpl33 1144 |
. . . . . . . 8
|
86 | | eqidd 2623 |
. . . . . . . 8
|
87 | | eqidd 2623 |
. . . . . . . 8
|
88 | | simpr 477 |
. . . . . . . 8
|
89 | | opeq1 4402 |
. . . . . . . . . . . 12
|
90 | 89 | opeq2d 4409 |
. . . . . . . . . . 11
|
91 | 90 | eqeq2d 2632 |
. . . . . . . . . 10
|
92 | 91, 63 | 3anbi23d 1402 |
. . . . . . . . 9
|
93 | | opeq2 4403 |
. . . . . . . . . . . 12
|
94 | 93 | opeq2d 4409 |
. . . . . . . . . . 11
|
95 | 94 | eqeq2d 2632 |
. . . . . . . . . 10
|
96 | 95, 64 | 3anbi23d 1402 |
. . . . . . . . 9
|
97 | 92, 96 | rspc2ev 3324 |
. . . . . . . 8
|
98 | 84, 85, 86, 87, 88, 97 | syl113anc 1338 |
. . . . . . 7
|
99 | | opeq2 4403 |
. . . . . . . . . . . 12
|
100 | 99 | opeq2d 4409 |
. . . . . . . . . . 11
|
101 | 100 | eqeq2d 2632 |
. . . . . . . . . 10
|
102 | 101, 44 | 3anbi13d 1401 |
. . . . . . . . 9
|
103 | 102 | 2rexbidv 3057 |
. . . . . . . 8
|
104 | | opeq1 4402 |
. . . . . . . . . . . 12
|
105 | 104 | opeq1d 4408 |
. . . . . . . . . . 11
|
106 | 105 | eqeq2d 2632 |
. . . . . . . . . 10
|
107 | 106, 56 | 3anbi23d 1402 |
. . . . . . . . 9
|
108 | 107 | 2rexbidv 3057 |
. . . . . . . 8
|
109 | | opeq2 4403 |
. . . . . . . . . . . 12
|
110 | 109 | opeq1d 4408 |
. . . . . . . . . . 11
|
111 | 110 | eqeq2d 2632 |
. . . . . . . . . 10
|
112 | 111, 57 | 3anbi23d 1402 |
. . . . . . . . 9
|
113 | 112 | 2rexbidv 3057 |
. . . . . . . 8
|
114 | 103, 108,
113 | rspc3ev 3326 |
. . . . . . 7
|
115 | 81, 82, 83, 98, 114 | syl31anc 1329 |
. . . . . 6
|
116 | | opeq1 4402 |
. . . . . . . . . . . . 13
|
117 | 116 | opeq1d 4408 |
. . . . . . . . . . . 12
|
118 | 117 | eqeq2d 2632 |
. . . . . . . . . . 11
|
119 | 118, 36 | 3anbi13d 1401 |
. . . . . . . . . 10
|
120 | 119 | rexbidv 3052 |
. . . . . . . . 9
|
121 | 120 | 2rexbidv 3057 |
. . . . . . . 8
|
122 | 121 | 2rexbidv 3057 |
. . . . . . 7
|
123 | | opeq2 4403 |
. . . . . . . . . . . . 13
|
124 | 123 | opeq1d 4408 |
. . . . . . . . . . . 12
|
125 | 124 | eqeq2d 2632 |
. . . . . . . . . . 11
|
126 | 125, 37 | 3anbi13d 1401 |
. . . . . . . . . 10
|
127 | 126 | rexbidv 3052 |
. . . . . . . . 9
|
128 | 127 | 2rexbidv 3057 |
. . . . . . . 8
|
129 | 128 | 2rexbidv 3057 |
. . . . . . 7
|
130 | | opeq1 4402 |
. . . . . . . . . . . . 13
|
131 | 130 | opeq2d 4409 |
. . . . . . . . . . . 12
|
132 | 131 | eqeq2d 2632 |
. . . . . . . . . . 11
|
133 | 132, 43 | 3anbi13d 1401 |
. . . . . . . . . 10
|
134 | 133 | rexbidv 3052 |
. . . . . . . . 9
|
135 | 134 | 2rexbidv 3057 |
. . . . . . . 8
|
136 | 135 | 2rexbidv 3057 |
. . . . . . 7
|
137 | 122, 129,
136 | rspc3ev 3326 |
. . . . . 6
|
138 | 78, 79, 80, 115, 137 | syl31anc 1329 |
. . . . 5
|
139 | 138 | ex 450 |
. . . 4
|
140 | 77, 139 | impbid 202 |
. . 3
|
141 | 22, 23, 24, 25, 26, 27, 28, 29, 140 | syl233anc 1355 |
. 2
|
142 | 21, 141 | bitrd 268 |
1
|