Step | Hyp | Ref
| Expression |
1 | | topgele 20734 |
. . . 4
TopOn
|
2 | 1 | adantl 482 |
. . 3
TopOn |
3 | 2 | simprd 479 |
. 2
TopOn |
4 | | selpw 4165 |
. . . . . . 7
|
5 | | simp3 1063 |
. . . . . . . . . 10
TopOn
TopOn |
6 | | df-ima 5127 |
. . . . . . . . . . . . . . . . . 18
|
7 | | resmpt 5449 |
. . . . . . . . . . . . . . . . . . 19
|
8 | 7 | rneqd 5353 |
. . . . . . . . . . . . . . . . . 18
|
9 | 6, 8 | syl5eq 2668 |
. . . . . . . . . . . . . . . . 17
|
10 | | rnmptsn 33182 |
. . . . . . . . . . . . . . . . 17
|
11 | 9, 10 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
|
12 | | imassrn 5477 |
. . . . . . . . . . . . . . . 16
|
13 | 11, 12 | syl6eqssr 3656 |
. . . . . . . . . . . . . . 15
|
14 | | rnmptsn 33182 |
. . . . . . . . . . . . . . 15
|
15 | 13, 14 | syl6sseq 3651 |
. . . . . . . . . . . . . 14
|
16 | | dissneq.c |
. . . . . . . . . . . . . . 15
|
17 | | sneq 4187 |
. . . . . . . . . . . . . . . . . 18
|
18 | 17 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . 17
|
19 | 18 | cbvrexv 3172 |
. . . . . . . . . . . . . . . 16
|
20 | 19 | abbii 2739 |
. . . . . . . . . . . . . . 15
|
21 | 16, 20 | eqtri 2644 |
. . . . . . . . . . . . . 14
|
22 | 15, 21 | syl6sseqr 3652 |
. . . . . . . . . . . . 13
|
23 | 22 | adantl 482 |
. . . . . . . . . . . 12
|
24 | | sstr 3611 |
. . . . . . . . . . . . . 14
|
25 | 24 | expcom 451 |
. . . . . . . . . . . . 13
|
26 | 25 | adantr 481 |
. . . . . . . . . . . 12
|
27 | 23, 26 | mpd 15 |
. . . . . . . . . . 11
|
28 | 27 | 3adant3 1081 |
. . . . . . . . . 10
TopOn
|
29 | 5, 28 | ssexd 4805 |
. . . . . . . . 9
TopOn
|
30 | | isset 3207 |
. . . . . . . . 9
|
31 | 29, 30 | sylib 208 |
. . . . . . . 8
TopOn
|
32 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
33 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
34 | 32, 33 | mptsnun 33186 |
. . . . . . . . . . . . . 14
|
35 | 11 | unieqd 4446 |
. . . . . . . . . . . . . 14
|
36 | 34, 35 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
37 | 36 | adantl 482 |
. . . . . . . . . . . 12
|
38 | 27, 37 | jca 554 |
. . . . . . . . . . 11
|
39 | | sseq1 3626 |
. . . . . . . . . . . 12
|
40 | | unieq 4444 |
. . . . . . . . . . . . 13
|
41 | 40 | eqeq2d 2632 |
. . . . . . . . . . . 12
|
42 | 39, 41 | anbi12d 747 |
. . . . . . . . . . 11
|
43 | 38, 42 | syl5ibrcom 237 |
. . . . . . . . . 10
|
44 | 43 | eximdv 1846 |
. . . . . . . . 9
|
45 | 44 | 3adant3 1081 |
. . . . . . . 8
TopOn
|
46 | 31, 45 | mpd 15 |
. . . . . . 7
TopOn
|
47 | 4, 46 | syl3an2b 1363 |
. . . . . 6
TopOn |
48 | 47 | 3com23 1271 |
. . . . 5
TopOn
|
49 | 48 | 3expia 1267 |
. . . 4
TopOn |
50 | | topontop 20718 |
. . . . . . . 8
TopOn
|
51 | | tgtop 20777 |
. . . . . . . 8
|
52 | 50, 51 | syl 17 |
. . . . . . 7
TopOn
|
53 | 52 | eleq2d 2687 |
. . . . . 6
TopOn
|
54 | | eltg3 20766 |
. . . . . 6
TopOn
|
55 | 53, 54 | bitr3d 270 |
. . . . 5
TopOn
|
56 | 55 | adantl 482 |
. . . 4
TopOn
|
57 | 49, 56 | sylibrd 249 |
. . 3
TopOn |
58 | 57 | ssrdv 3609 |
. 2
TopOn |
59 | 3, 58 | eqssd 3620 |
1
TopOn |