Step | Hyp | Ref
| Expression |
1 | | iscn 21039 |
. . . 4
TopOn TopOn
|
2 | 1 | simprbda 653 |
. . 3
TopOn TopOn
|
3 | | eqid 2622 |
. . . . . . 7
|
4 | 3 | cncnpi 21082 |
. . . . . 6
|
5 | 4 | ralrimiva 2966 |
. . . . 5
|
6 | 5 | adantl 482 |
. . . 4
TopOn TopOn
|
7 | | toponuni 20719 |
. . . . . 6
TopOn
|
8 | 7 | ad2antrr 762 |
. . . . 5
TopOn TopOn
|
9 | 8 | raleqdv 3144 |
. . . 4
TopOn TopOn
|
10 | 6, 9 | mpbird 247 |
. . 3
TopOn TopOn
|
11 | 2, 10 | jca 554 |
. 2
TopOn TopOn
|
12 | | simprl 794 |
. . 3
TopOn TopOn
|
13 | | cnvimass 5485 |
. . . . . . . . . 10
|
14 | | fdm 6051 |
. . . . . . . . . . 11
|
15 | 14 | adantl 482 |
. . . . . . . . . 10
TopOn
TopOn
|
16 | 13, 15 | syl5sseq 3653 |
. . . . . . . . 9
TopOn
TopOn
|
17 | | ssralv 3666 |
. . . . . . . . 9
|
18 | 16, 17 | syl 17 |
. . . . . . . 8
TopOn
TopOn
|
19 | | simprr 796 |
. . . . . . . . . . . 12
TopOn
TopOn
|
20 | | simpllr 799 |
. . . . . . . . . . . 12
TopOn
TopOn
|
21 | | ffn 6045 |
. . . . . . . . . . . . . 14
|
22 | 21 | ad2antlr 763 |
. . . . . . . . . . . . 13
TopOn
TopOn
|
23 | | simprl 794 |
. . . . . . . . . . . . 13
TopOn
TopOn
|
24 | | elpreima 6337 |
. . . . . . . . . . . . . 14
|
25 | 24 | simplbda 654 |
. . . . . . . . . . . . 13
|
26 | 22, 23, 25 | syl2anc 693 |
. . . . . . . . . . . 12
TopOn
TopOn
|
27 | | cnpimaex 21060 |
. . . . . . . . . . . 12
|
28 | 19, 20, 26, 27 | syl3anc 1326 |
. . . . . . . . . . 11
TopOn
TopOn
|
29 | | simpllr 799 |
. . . . . . . . . . . . . . 15
TopOn TopOn
|
30 | | ffun 6048 |
. . . . . . . . . . . . . . 15
|
31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . 14
TopOn TopOn
|
32 | | simp-4l 806 |
. . . . . . . . . . . . . . . 16
TopOn
TopOn
TopOn |
33 | | toponss 20731 |
. . . . . . . . . . . . . . . 16
TopOn |
34 | 32, 33 | sylan 488 |
. . . . . . . . . . . . . . 15
TopOn TopOn
|
35 | 29, 14 | syl 17 |
. . . . . . . . . . . . . . 15
TopOn TopOn
|
36 | 34, 35 | sseqtr4d 3642 |
. . . . . . . . . . . . . 14
TopOn TopOn
|
37 | | funimass3 6333 |
. . . . . . . . . . . . . 14
|
38 | 31, 36, 37 | syl2anc 693 |
. . . . . . . . . . . . 13
TopOn TopOn
|
39 | 38 | anbi2d 740 |
. . . . . . . . . . . 12
TopOn TopOn
|
40 | 39 | rexbidva 3049 |
. . . . . . . . . . 11
TopOn
TopOn
|
41 | 28, 40 | mpbid 222 |
. . . . . . . . . 10
TopOn
TopOn
|
42 | 41 | expr 643 |
. . . . . . . . 9
TopOn
TopOn
|
43 | 42 | ralimdva 2962 |
. . . . . . . 8
TopOn
TopOn
|
44 | 18, 43 | syld 47 |
. . . . . . 7
TopOn
TopOn
|
45 | 44 | impr 649 |
. . . . . 6
TopOn
TopOn
|
46 | 45 | an32s 846 |
. . . . 5
TopOn
TopOn
|
47 | | topontop 20718 |
. . . . . . 7
TopOn
|
48 | 47 | ad3antrrr 766 |
. . . . . 6
TopOn
TopOn |
49 | | eltop2 20779 |
. . . . . 6
|
50 | 48, 49 | syl 17 |
. . . . 5
TopOn
TopOn
|
51 | 46, 50 | mpbird 247 |
. . . 4
TopOn
TopOn |
52 | 51 | ralrimiva 2966 |
. . 3
TopOn TopOn
|
53 | 1 | adantr 481 |
. . 3
TopOn TopOn
|
54 | 12, 52, 53 | mpbir2and 957 |
. 2
TopOn TopOn
|
55 | 11, 54 | impbida 877 |
1
TopOn TopOn
|