Step | Hyp | Ref
| Expression |
1 | | iscn 12366 |
. . . 4
TopOn TopOn
|
2 | 1 | simprbda 380 |
. . 3
TopOn TopOn
|
3 | | eqid 2139 |
. . . . . . 7
|
4 | 3 | cncnpi 12397 |
. . . . . 6
|
5 | 4 | ralrimiva 2505 |
. . . . 5
|
6 | 5 | adantl 275 |
. . . 4
TopOn TopOn
|
7 | | toponuni 12182 |
. . . . . 6
TopOn
|
8 | 7 | ad2antrr 479 |
. . . . 5
TopOn TopOn
|
9 | 8 | raleqdv 2632 |
. . . 4
TopOn TopOn
|
10 | 6, 9 | mpbird 166 |
. . 3
TopOn TopOn
|
11 | 2, 10 | jca 304 |
. 2
TopOn TopOn
|
12 | | simprl 520 |
. . 3
TopOn TopOn
|
13 | | cnvimass 4902 |
. . . . . . . . . 10
|
14 | | fdm 5278 |
. . . . . . . . . . 11
|
15 | 14 | adantl 275 |
. . . . . . . . . 10
TopOn
TopOn
|
16 | 13, 15 | sseqtrid 3147 |
. . . . . . . . 9
TopOn
TopOn
|
17 | | ssralv 3161 |
. . . . . . . . 9
|
18 | 16, 17 | syl 14 |
. . . . . . . 8
TopOn
TopOn
|
19 | | simp-4l 530 |
. . . . . . . . . . . 12
TopOn
TopOn
TopOn |
20 | | simp-4r 531 |
. . . . . . . . . . . 12
TopOn
TopOn
TopOn |
21 | | topontop 12181 |
. . . . . . . . . . . . . 14
TopOn
|
22 | 20, 21 | syl 14 |
. . . . . . . . . . . . 13
TopOn
TopOn
|
23 | | simprr 521 |
. . . . . . . . . . . . 13
TopOn
TopOn
|
24 | | cnprcl2k 12375 |
. . . . . . . . . . . . 13
TopOn
|
25 | 19, 22, 23, 24 | syl3anc 1216 |
. . . . . . . . . . . 12
TopOn
TopOn
|
26 | | simpllr 523 |
. . . . . . . . . . . 12
TopOn
TopOn
|
27 | | ffn 5272 |
. . . . . . . . . . . . . 14
|
28 | 27 | ad2antlr 480 |
. . . . . . . . . . . . 13
TopOn
TopOn
|
29 | | simprl 520 |
. . . . . . . . . . . . 13
TopOn
TopOn
|
30 | | elpreima 5539 |
. . . . . . . . . . . . . 14
|
31 | 30 | simplbda 381 |
. . . . . . . . . . . . 13
|
32 | 28, 29, 31 | syl2anc 408 |
. . . . . . . . . . . 12
TopOn
TopOn
|
33 | | icnpimaex 12380 |
. . . . . . . . . . . 12
TopOn TopOn
|
34 | 19, 20, 25, 23, 26, 32, 33 | syl33anc 1231 |
. . . . . . . . . . 11
TopOn
TopOn
|
35 | | simpllr 523 |
. . . . . . . . . . . . . . 15
TopOn TopOn
|
36 | 35 | ffund 5276 |
. . . . . . . . . . . . . 14
TopOn TopOn
|
37 | | toponss 12193 |
. . . . . . . . . . . . . . . 16
TopOn |
38 | 19, 37 | sylan 281 |
. . . . . . . . . . . . . . 15
TopOn TopOn
|
39 | 35 | fdmd 5279 |
. . . . . . . . . . . . . . 15
TopOn TopOn
|
40 | 38, 39 | sseqtrrd 3136 |
. . . . . . . . . . . . . 14
TopOn TopOn
|
41 | | funimass3 5536 |
. . . . . . . . . . . . . 14
|
42 | 36, 40, 41 | syl2anc 408 |
. . . . . . . . . . . . 13
TopOn TopOn
|
43 | 42 | anbi2d 459 |
. . . . . . . . . . . 12
TopOn TopOn
|
44 | 43 | rexbidva 2434 |
. . . . . . . . . . 11
TopOn
TopOn
|
45 | 34, 44 | mpbid 146 |
. . . . . . . . . 10
TopOn
TopOn
|
46 | 45 | expr 372 |
. . . . . . . . 9
TopOn
TopOn
|
47 | 46 | ralimdva 2499 |
. . . . . . . 8
TopOn
TopOn
|
48 | 18, 47 | syld 45 |
. . . . . . 7
TopOn
TopOn
|
49 | 48 | impr 376 |
. . . . . 6
TopOn
TopOn
|
50 | 49 | an32s 557 |
. . . . 5
TopOn
TopOn
|
51 | | topontop 12181 |
. . . . . . 7
TopOn
|
52 | 51 | ad3antrrr 483 |
. . . . . 6
TopOn
TopOn |
53 | | eltop2 12239 |
. . . . . 6
|
54 | 52, 53 | syl 14 |
. . . . 5
TopOn
TopOn
|
55 | 50, 54 | mpbird 166 |
. . . 4
TopOn
TopOn |
56 | 55 | ralrimiva 2505 |
. . 3
TopOn TopOn
|
57 | 1 | adantr 274 |
. . 3
TopOn TopOn
|
58 | 12, 56, 57 | mpbir2and 928 |
. 2
TopOn TopOn
|
59 | 11, 58 | impbida 585 |
1
TopOn TopOn
|