Step | Hyp | Ref
| Expression |
1 | | iscn 13268 |
. . . 4
TopOn TopOn
|
2 | 1 | simprbda 383 |
. . 3
TopOn TopOn
|
3 | | eqid 2175 |
. . . . . . 7
|
4 | 3 | cncnpi 13299 |
. . . . . 6
|
5 | 4 | ralrimiva 2548 |
. . . . 5
|
6 | 5 | adantl 277 |
. . . 4
TopOn TopOn
|
7 | | toponuni 13084 |
. . . . . 6
TopOn
|
8 | 7 | ad2antrr 488 |
. . . . 5
TopOn TopOn
|
9 | 8 | raleqdv 2676 |
. . . 4
TopOn TopOn
|
10 | 6, 9 | mpbird 167 |
. . 3
TopOn TopOn
|
11 | 2, 10 | jca 306 |
. 2
TopOn TopOn
|
12 | | simprl 529 |
. . 3
TopOn TopOn
|
13 | | cnvimass 4984 |
. . . . . . . . . 10
|
14 | | fdm 5363 |
. . . . . . . . . . 11
|
15 | 14 | adantl 277 |
. . . . . . . . . 10
TopOn
TopOn
|
16 | 13, 15 | sseqtrid 3203 |
. . . . . . . . 9
TopOn
TopOn
|
17 | | ssralv 3217 |
. . . . . . . . 9
|
18 | 16, 17 | syl 14 |
. . . . . . . 8
TopOn
TopOn
|
19 | | simp-4l 541 |
. . . . . . . . . . . 12
TopOn
TopOn
TopOn |
20 | | simp-4r 542 |
. . . . . . . . . . . 12
TopOn
TopOn
TopOn |
21 | | topontop 13083 |
. . . . . . . . . . . . . 14
TopOn
|
22 | 20, 21 | syl 14 |
. . . . . . . . . . . . 13
TopOn
TopOn
|
23 | | simprr 531 |
. . . . . . . . . . . . 13
TopOn
TopOn
|
24 | | cnprcl2k 13277 |
. . . . . . . . . . . . 13
TopOn
|
25 | 19, 22, 23, 24 | syl3anc 1238 |
. . . . . . . . . . . 12
TopOn
TopOn
|
26 | | simpllr 534 |
. . . . . . . . . . . 12
TopOn
TopOn
|
27 | | ffn 5357 |
. . . . . . . . . . . . . 14
|
28 | 27 | ad2antlr 489 |
. . . . . . . . . . . . 13
TopOn
TopOn
|
29 | | simprl 529 |
. . . . . . . . . . . . 13
TopOn
TopOn
|
30 | | elpreima 5627 |
. . . . . . . . . . . . . 14
|
31 | 30 | simplbda 384 |
. . . . . . . . . . . . 13
|
32 | 28, 29, 31 | syl2anc 411 |
. . . . . . . . . . . 12
TopOn
TopOn
|
33 | | icnpimaex 13282 |
. . . . . . . . . . . 12
TopOn TopOn
|
34 | 19, 20, 25, 23, 26, 32, 33 | syl33anc 1253 |
. . . . . . . . . . 11
TopOn
TopOn
|
35 | | simpllr 534 |
. . . . . . . . . . . . . . 15
TopOn TopOn
|
36 | 35 | ffund 5361 |
. . . . . . . . . . . . . 14
TopOn TopOn
|
37 | | toponss 13095 |
. . . . . . . . . . . . . . . 16
TopOn |
38 | 19, 37 | sylan 283 |
. . . . . . . . . . . . . . 15
TopOn TopOn
|
39 | 35 | fdmd 5364 |
. . . . . . . . . . . . . . 15
TopOn TopOn
|
40 | 38, 39 | sseqtrrd 3192 |
. . . . . . . . . . . . . 14
TopOn TopOn
|
41 | | funimass3 5624 |
. . . . . . . . . . . . . 14
|
42 | 36, 40, 41 | syl2anc 411 |
. . . . . . . . . . . . 13
TopOn TopOn
|
43 | 42 | anbi2d 464 |
. . . . . . . . . . . 12
TopOn TopOn
|
44 | 43 | rexbidva 2472 |
. . . . . . . . . . 11
TopOn
TopOn
|
45 | 34, 44 | mpbid 147 |
. . . . . . . . . 10
TopOn
TopOn
|
46 | 45 | expr 375 |
. . . . . . . . 9
TopOn
TopOn
|
47 | 46 | ralimdva 2542 |
. . . . . . . 8
TopOn
TopOn
|
48 | 18, 47 | syld 45 |
. . . . . . 7
TopOn
TopOn
|
49 | 48 | impr 379 |
. . . . . 6
TopOn
TopOn
|
50 | 49 | an32s 568 |
. . . . 5
TopOn
TopOn
|
51 | | topontop 13083 |
. . . . . . 7
TopOn
|
52 | 51 | ad3antrrr 492 |
. . . . . 6
TopOn
TopOn |
53 | | eltop2 13141 |
. . . . . 6
|
54 | 52, 53 | syl 14 |
. . . . 5
TopOn
TopOn
|
55 | 50, 54 | mpbird 167 |
. . . 4
TopOn
TopOn |
56 | 55 | ralrimiva 2548 |
. . 3
TopOn TopOn
|
57 | 1 | adantr 276 |
. . 3
TopOn TopOn
|
58 | 12, 56, 57 | mpbir2and 944 |
. 2
TopOn TopOn
|
59 | 11, 58 | impbida 596 |
1
TopOn TopOn
|