Step | Hyp | Ref
| Expression |
1 | | elequ1 1997 |
. . . . . . . . . . . . . . . 16
|
2 | | elequ2 2004 |
. . . . . . . . . . . . . . . 16
|
3 | 1, 2 | bitrd 268 |
. . . . . . . . . . . . . . 15
|
4 | 3 | notbid 308 |
. . . . . . . . . . . . . 14
|
5 | 4 | cbvralv 3171 |
. . . . . . . . . . . . 13
|
6 | 5 | biimpi 206 |
. . . . . . . . . . . 12
|
7 | 6 | ralimi 2952 |
. . . . . . . . . . 11
|
8 | | untuni 31586 |
. . . . . . . . . . 11
|
9 | 7, 8 | sylibr 224 |
. . . . . . . . . 10
|
10 | | vex 3203 |
. . . . . . . . . . . 12
|
11 | | sseq1 3626 |
. . . . . . . . . . . . 13
|
12 | | treq 4758 |
. . . . . . . . . . . . 13
|
13 | | raleq 3138 |
. . . . . . . . . . . . 13
|
14 | 11, 12, 13 | 3anbi123d 1399 |
. . . . . . . . . . . 12
|
15 | 10, 14 | elab 3350 |
. . . . . . . . . . 11
|
16 | | vex 3203 |
. . . . . . . . . . . . . . . 16
|
17 | | dfon2lem3 31690 |
. . . . . . . . . . . . . . . 16
|
18 | 16, 17 | ax-mp 5 |
. . . . . . . . . . . . . . 15
|
19 | 18 | simprd 479 |
. . . . . . . . . . . . . 14
|
20 | | untelirr 31585 |
. . . . . . . . . . . . . 14
|
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . 13
|
22 | 21 | ralimi 2952 |
. . . . . . . . . . . 12
|
23 | 22 | 3ad2ant3 1084 |
. . . . . . . . . . 11
|
24 | 15, 23 | sylbi 207 |
. . . . . . . . . 10
|
25 | 9, 24 | mprg 2926 |
. . . . . . . . 9
|
26 | | untelirr 31585 |
. . . . . . . . . 10
|
27 | | psseq2 3695 |
. . . . . . . . . . . . . . . . . 18
|
28 | 27 | anbi1d 741 |
. . . . . . . . . . . . . . . . 17
|
29 | | elequ2 2004 |
. . . . . . . . . . . . . . . . 17
|
30 | 28, 29 | imbi12d 334 |
. . . . . . . . . . . . . . . 16
|
31 | 30 | albidv 1849 |
. . . . . . . . . . . . . . 15
|
32 | 31 | cbvralv 3171 |
. . . . . . . . . . . . . 14
|
33 | 32 | 3anbi3i 1255 |
. . . . . . . . . . . . 13
|
34 | 33 | abbii 2739 |
. . . . . . . . . . . 12
|
35 | 34 | unieqi 4445 |
. . . . . . . . . . 11
|
36 | 35 | eleq2i 2693 |
. . . . . . . . . 10
|
37 | 26, 36 | sylnib 318 |
. . . . . . . . 9
|
38 | 25, 37 | ax-mp 5 |
. . . . . . . 8
|
39 | | dfon2lem7.1 |
. . . . . . . . . 10
|
40 | | dfon2lem2 31689 |
. . . . . . . . . 10
|
41 | 39, 40 | ssexi 4803 |
. . . . . . . . 9
|
42 | 41 | snss 4316 |
. . . . . . . 8
|
43 | 38, 42 | mtbi 312 |
. . . . . . 7
|
44 | 43 | intnan 960 |
. . . . . 6
|
45 | | df-suc 5729 |
. . . . . . . 8
|
46 | 45 | sseq1i 3629 |
. . . . . . 7
|
47 | | unss 3787 |
. . . . . . 7
|
48 | 46, 47 | bitr4i 267 |
. . . . . 6
|
49 | 44, 48 | mtbir 313 |
. . . . 5
|
50 | 41 | snss 4316 |
. . . . . 6
|
51 | 45 | sseq1i 3629 |
. . . . . . . . 9
|
52 | | unss 3787 |
. . . . . . . . 9
|
53 | 51, 52 | bitr4i 267 |
. . . . . . . 8
|
54 | | dfon2lem1 31688 |
. . . . . . . . . . . 12
|
55 | | suctr 5808 |
. . . . . . . . . . . 12
|
56 | 54, 55 | ax-mp 5 |
. . . . . . . . . . 11
|
57 | | vex 3203 |
. . . . . . . . . . . . . 14
|
58 | 57 | elsuc 5794 |
. . . . . . . . . . . . 13
|
59 | | eluni2 4440 |
. . . . . . . . . . . . . . 15
|
60 | | nfa1 2028 |
. . . . . . . . . . . . . . . 16
|
61 | 31 | rspccv 3306 |
. . . . . . . . . . . . . . . . . . 19
|
62 | | psseq1 3694 |
. . . . . . . . . . . . . . . . . . . . . 22
|
63 | | treq 4758 |
. . . . . . . . . . . . . . . . . . . . . 22
|
64 | 62, 63 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . 21
|
65 | | elequ1 1997 |
. . . . . . . . . . . . . . . . . . . . 21
|
66 | 64, 65 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . 20
|
67 | 66 | cbvalv 2273 |
. . . . . . . . . . . . . . . . . . 19
|
68 | 61, 67 | syl6ib 241 |
. . . . . . . . . . . . . . . . . 18
|
69 | 68 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . 17
|
70 | 15, 69 | sylbi 207 |
. . . . . . . . . . . . . . . 16
|
71 | 60, 70 | rexlimi 3024 |
. . . . . . . . . . . . . . 15
|
72 | 59, 71 | sylbi 207 |
. . . . . . . . . . . . . 14
|
73 | | psseq1 3694 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
74 | | treq 4758 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
75 | 73, 74 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
76 | | elequ1 1997 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
77 | 75, 76 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
78 | 77 | cbvalv 2273 |
. . . . . . . . . . . . . . . . . . . . . 22
|
79 | 61, 78 | syl6ib 241 |
. . . . . . . . . . . . . . . . . . . . 21
|
80 | 79 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . . . 20
|
81 | 15, 80 | sylbi 207 |
. . . . . . . . . . . . . . . . . . 19
|
82 | 81 | rexlimiv 3027 |
. . . . . . . . . . . . . . . . . 18
|
83 | 59, 82 | sylbi 207 |
. . . . . . . . . . . . . . . . 17
|
84 | 83 | rgen 2922 |
. . . . . . . . . . . . . . . 16
|
85 | | dfon2lem6 31693 |
. . . . . . . . . . . . . . . 16
|
86 | 54, 84, 85 | mp2an 708 |
. . . . . . . . . . . . . . 15
|
87 | | psseq2 3695 |
. . . . . . . . . . . . . . . . . 18
|
88 | 87 | anbi1d 741 |
. . . . . . . . . . . . . . . . 17
|
89 | | eleq2 2690 |
. . . . . . . . . . . . . . . . 17
|
90 | 88, 89 | imbi12d 334 |
. . . . . . . . . . . . . . . 16
|
91 | 90 | albidv 1849 |
. . . . . . . . . . . . . . 15
|
92 | 86, 91 | mpbiri 248 |
. . . . . . . . . . . . . 14
|
93 | 72, 92 | jaoi 394 |
. . . . . . . . . . . . 13
|
94 | 58, 93 | sylbi 207 |
. . . . . . . . . . . 12
|
95 | 94 | rgen 2922 |
. . . . . . . . . . 11
|
96 | 41 | sucex 7011 |
. . . . . . . . . . . . 13
|
97 | | sseq1 3626 |
. . . . . . . . . . . . . 14
|
98 | | treq 4758 |
. . . . . . . . . . . . . 14
|
99 | | raleq 3138 |
. . . . . . . . . . . . . 14
|
100 | 97, 98, 99 | 3anbi123d 1399 |
. . . . . . . . . . . . 13
|
101 | 96, 100 | elab 3350 |
. . . . . . . . . . . 12
|
102 | | elssuni 4467 |
. . . . . . . . . . . 12
|
103 | 101, 102 | sylbir 225 |
. . . . . . . . . . 11
|
104 | 56, 95, 103 | mp3an23 1416 |
. . . . . . . . . 10
|
105 | | sseq1 3626 |
. . . . . . . . . . . . 13
|
106 | | treq 4758 |
. . . . . . . . . . . . 13
|
107 | | raleq 3138 |
. . . . . . . . . . . . . 14
|
108 | | psseq1 3694 |
. . . . . . . . . . . . . . . . . 18
|
109 | | treq 4758 |
. . . . . . . . . . . . . . . . . 18
|
110 | 108, 109 | anbi12d 747 |
. . . . . . . . . . . . . . . . 17
|
111 | | elequ1 1997 |
. . . . . . . . . . . . . . . . 17
|
112 | 110, 111 | imbi12d 334 |
. . . . . . . . . . . . . . . 16
|
113 | 112 | cbvalv 2273 |
. . . . . . . . . . . . . . 15
|
114 | 113 | ralbii 2980 |
. . . . . . . . . . . . . 14
|
115 | 107, 114 | syl6bb 276 |
. . . . . . . . . . . . 13
|
116 | 105, 106,
115 | 3anbi123d 1399 |
. . . . . . . . . . . 12
|
117 | 116 | cbvabv 2747 |
. . . . . . . . . . 11
|
118 | 117 | unieqi 4445 |
. . . . . . . . . 10
|
119 | 104, 118 | syl6sseq 3651 |
. . . . . . . . 9
|
120 | 119 | a1i 11 |
. . . . . . . 8
|
121 | 53, 120 | syl5bir 233 |
. . . . . . 7
|
122 | 40, 121 | mpani 712 |
. . . . . 6
|
123 | 50, 122 | syl5bi 232 |
. . . . 5
|
124 | 49, 123 | mtoi 190 |
. . . 4
|
125 | | psseq1 3694 |
. . . . . . . 8
|
126 | | treq 4758 |
. . . . . . . 8
|
127 | 125, 126 | anbi12d 747 |
. . . . . . 7
|
128 | | eleq1 2689 |
. . . . . . 7
|
129 | 127, 128 | imbi12d 334 |
. . . . . 6
|
130 | 41, 129 | spcv 3299 |
. . . . 5
|
131 | 54, 130 | mpan2i 713 |
. . . 4
|
132 | 124, 131 | mtod 189 |
. . 3
|
133 | | dfpss2 3692 |
. . . . 5
|
134 | 133 | biimpri 218 |
. . . 4
|
135 | 40, 134 | mpan 706 |
. . 3
|
136 | 132, 135 | nsyl2 142 |
. 2
|
137 | | eluni2 4440 |
. . . . 5
|
138 | | psseq2 3695 |
. . . . . . . . . . . . . 14
|
139 | 138 | anbi1d 741 |
. . . . . . . . . . . . 13
|
140 | | elequ2 2004 |
. . . . . . . . . . . . 13
|
141 | 139, 140 | imbi12d 334 |
. . . . . . . . . . . 12
|
142 | 141 | albidv 1849 |
. . . . . . . . . . 11
|
143 | 142 | cbvralv 3171 |
. . . . . . . . . 10
|
144 | 13, 143 | syl6bb 276 |
. . . . . . . . 9
|
145 | 11, 12, 144 | 3anbi123d 1399 |
. . . . . . . 8
|
146 | 10, 145 | elab 3350 |
. . . . . . 7
|
147 | | rsp 2929 |
. . . . . . . 8
|
148 | 147 | 3ad2ant3 1084 |
. . . . . . 7
|
149 | 146, 148 | sylbi 207 |
. . . . . 6
|
150 | 149 | rexlimiv 3027 |
. . . . 5
|
151 | 137, 150 | sylbi 207 |
. . . 4
|
152 | 151 | rgen 2922 |
. . 3
|
153 | | raleq 3138 |
. . 3
|
154 | 152, 153 | mpbii 223 |
. 2
|
155 | | psseq2 3695 |
. . . . . 6
|
156 | 155 | anbi1d 741 |
. . . . 5
|
157 | | eleq2 2690 |
. . . . 5
|
158 | 156, 157 | imbi12d 334 |
. . . 4
|
159 | 158 | albidv 1849 |
. . 3
|
160 | 159 | rspccv 3306 |
. 2
|
161 | 136, 154,
160 | 3syl 18 |
1
|