Step | Hyp | Ref
| Expression |
1 | | toptopon2 20723 |
. . . . . 6
TopOn |
2 | 1 | biimpi 206 |
. . . . 5
TopOn |
3 | | fvex 6201 |
. . . . . 6
TopOn |
4 | | eleq2 2690 |
. . . . . . . 8
TopOn
TopOn |
5 | | eleq1 2689 |
. . . . . . . 8
TopOn TopOn
TopOn TopOn |
6 | 4, 5 | anbi12d 747 |
. . . . . . 7
TopOn TopOn TopOn TopOn
TopOn |
7 | | simpl 473 |
. . . . . . . . 9
TopOn TopOn TopOn
TopOn |
8 | | fntopon 20728 |
. . . . . . . . . . . 12
TopOn |
9 | | vuniex 6954 |
. . . . . . . . . . . 12
|
10 | 8, 9 | pm3.2i 471 |
. . . . . . . . . . 11
TopOn |
11 | | fnfvelrn 6356 |
. . . . . . . . . . 11
TopOn
TopOn TopOn |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . . 10
TopOn TopOn |
13 | 12 | jctr 565 |
. . . . . . . . 9
TopOn TopOn TopOn TopOn |
14 | 7, 13 | impbii 199 |
. . . . . . . 8
TopOn TopOn TopOn
TopOn |
15 | 14 | a1i 11 |
. . . . . . 7
TopOn TopOn TopOn
TopOn
TopOn |
16 | 6, 15 | bitrd 268 |
. . . . . 6
TopOn TopOn TopOn |
17 | 3, 16 | spcev 3300 |
. . . . 5
TopOn TopOn |
18 | 2, 17 | syl 17 |
. . . 4
TopOn |
19 | | funtopon 20725 |
. . . . . . . . . 10
TopOn |
20 | | elrnrexdm 6363 |
. . . . . . . . . 10
TopOn TopOn
TopOn TopOn |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . 9
TopOn TopOn TopOn |
22 | | rexex 3002 |
. . . . . . . . 9
TopOn TopOn TopOn |
23 | 21, 22 | syl 17 |
. . . . . . . 8
TopOn TopOn |
24 | 23 | anim2i 593 |
. . . . . . 7
TopOn TopOn |
25 | | 19.42v 1918 |
. . . . . . . . 9
TopOn TopOn |
26 | 25 | biimpri 218 |
. . . . . . . 8
TopOn TopOn |
27 | | eqimss 3657 |
. . . . . . . . . . . 12
TopOn
TopOn |
28 | 27 | sseld 3602 |
. . . . . . . . . . 11
TopOn
TopOn |
29 | 28 | com12 32 |
. . . . . . . . . 10
TopOn TopOn |
30 | 29 | imp 445 |
. . . . . . . . 9
TopOn TopOn |
31 | 30 | eximi 1762 |
. . . . . . . 8
TopOn
TopOn |
32 | 26, 31 | syl 17 |
. . . . . . 7
TopOn
TopOn |
33 | 24, 32 | syl 17 |
. . . . . 6
TopOn
TopOn |
34 | | topontop 20718 |
. . . . . . . 8
TopOn
|
35 | 34 | eximi 1762 |
. . . . . . 7
TopOn
|
36 | | ax5e 1841 |
. . . . . . 7
|
37 | 35, 36 | syl 17 |
. . . . . 6
TopOn |
38 | 33, 37 | syl 17 |
. . . . 5
TopOn
|
39 | 38 | exlimiv 1858 |
. . . 4
TopOn
|
40 | 18, 39 | impbii 199 |
. . 3
TopOn |
41 | | eluni 4439 |
. . . 4
TopOn
TopOn |
42 | 41 | bicomi 214 |
. . 3
TopOn
TopOn |
43 | 40, 42 | bitri 264 |
. 2
TopOn |
44 | 43 | eqriv 2619 |
1
TopOn |