Step | Hyp | Ref
| Expression |
1 | | cnf2 21053 |
. . . 4
TopOn TopOn
|
2 | 1 | 3expia 1267 |
. . 3
TopOn TopOn
|
3 | | elpwi 4168 |
. . . . . . 7
|
4 | 3 | adantl 482 |
. . . . . 6
TopOn TopOn
|
5 | | toponuni 20719 |
. . . . . . 7
TopOn
|
6 | 5 | ad2antrr 762 |
. . . . . 6
TopOn TopOn
|
7 | 4, 6 | sseqtrd 3641 |
. . . . 5
TopOn TopOn
|
8 | | eqid 2622 |
. . . . . . 7
|
9 | 8 | cnclsi 21076 |
. . . . . 6
|
10 | 9 | expcom 451 |
. . . . 5
|
11 | 7, 10 | syl 17 |
. . . 4
TopOn TopOn
|
12 | 11 | ralrimdva 2969 |
. . 3
TopOn TopOn
|
13 | 2, 12 | jcad 555 |
. 2
TopOn TopOn
|
14 | | cnvimass 5485 |
. . . . . . . . 9
|
15 | | fdm 6051 |
. . . . . . . . . 10
|
16 | 15 | ad2antlr 763 |
. . . . . . . . 9
TopOn
TopOn |
17 | 14, 16 | syl5sseq 3653 |
. . . . . . . 8
TopOn
TopOn |
18 | | toponmax 20730 |
. . . . . . . . . 10
TopOn
|
19 | 18 | ad3antrrr 766 |
. . . . . . . . 9
TopOn
TopOn |
20 | | elpw2g 4827 |
. . . . . . . . 9
|
21 | 19, 20 | syl 17 |
. . . . . . . 8
TopOn
TopOn |
22 | 17, 21 | mpbird 247 |
. . . . . . 7
TopOn
TopOn |
23 | | fveq2 6191 |
. . . . . . . . . 10
|
24 | 23 | imaeq2d 5466 |
. . . . . . . . 9
|
25 | | imaeq2 5462 |
. . . . . . . . . 10
|
26 | 25 | fveq2d 6195 |
. . . . . . . . 9
|
27 | 24, 26 | sseq12d 3634 |
. . . . . . . 8
|
28 | 27 | rspcv 3305 |
. . . . . . 7
|
29 | 22, 28 | syl 17 |
. . . . . 6
TopOn
TopOn
|
30 | | topontop 20718 |
. . . . . . . . . 10
TopOn
|
31 | 30 | ad3antlr 767 |
. . . . . . . . 9
TopOn
TopOn |
32 | | elpwi 4168 |
. . . . . . . . . . 11
|
33 | 32 | adantl 482 |
. . . . . . . . . 10
TopOn
TopOn |
34 | | toponuni 20719 |
. . . . . . . . . . 11
TopOn
|
35 | 34 | ad3antlr 767 |
. . . . . . . . . 10
TopOn
TopOn |
36 | 33, 35 | sseqtrd 3641 |
. . . . . . . . 9
TopOn
TopOn |
37 | | ffun 6048 |
. . . . . . . . . . . 12
|
38 | 37 | ad2antlr 763 |
. . . . . . . . . . 11
TopOn
TopOn |
39 | | funimacnv 5970 |
. . . . . . . . . . 11
|
40 | 38, 39 | syl 17 |
. . . . . . . . . 10
TopOn
TopOn |
41 | | inss1 3833 |
. . . . . . . . . 10
|
42 | 40, 41 | syl6eqss 3655 |
. . . . . . . . 9
TopOn
TopOn |
43 | | eqid 2622 |
. . . . . . . . . 10
|
44 | 43 | clsss 20858 |
. . . . . . . . 9
|
45 | 31, 36, 42, 44 | syl3anc 1326 |
. . . . . . . 8
TopOn
TopOn |
46 | | sstr2 3610 |
. . . . . . . 8
|
47 | 45, 46 | syl5com 31 |
. . . . . . 7
TopOn
TopOn
|
48 | | topontop 20718 |
. . . . . . . . . . 11
TopOn
|
49 | 48 | ad3antrrr 766 |
. . . . . . . . . 10
TopOn
TopOn |
50 | 5 | ad3antrrr 766 |
. . . . . . . . . . . 12
TopOn
TopOn |
51 | 16, 50 | eqtrd 2656 |
. . . . . . . . . . 11
TopOn
TopOn |
52 | 14, 51 | syl5sseq 3653 |
. . . . . . . . . 10
TopOn
TopOn |
53 | 8 | clsss3 20863 |
. . . . . . . . . 10
|
54 | 49, 52, 53 | syl2anc 693 |
. . . . . . . . 9
TopOn
TopOn |
55 | 54, 51 | sseqtr4d 3642 |
. . . . . . . 8
TopOn
TopOn
|
56 | | funimass3 6333 |
. . . . . . . 8
|
57 | 38, 55, 56 | syl2anc 693 |
. . . . . . 7
TopOn
TopOn
|
58 | 47, 57 | sylibd 229 |
. . . . . 6
TopOn
TopOn
|
59 | 29, 58 | syld 47 |
. . . . 5
TopOn
TopOn
|
60 | 59 | ralrimdva 2969 |
. . . 4
TopOn TopOn
|
61 | 60 | imdistanda 729 |
. . 3
TopOn TopOn
|
62 | | cncls2 21077 |
. . 3
TopOn TopOn
|
63 | 61, 62 | sylibrd 249 |
. 2
TopOn TopOn
|
64 | 13, 63 | impbid 202 |
1
TopOn TopOn
|