Step | Hyp | Ref
| Expression |
1 | | cnconst2 21087 |
. . . 4
TopOn TopOn
|
2 | 1 | 3expa 1265 |
. . 3
TopOn TopOn
|
3 | | eqid 2622 |
. . 3
|
4 | 2, 3 | fmptd 6385 |
. 2
TopOn TopOn
|
5 | | eqid 2622 |
. . . . . 6
|
6 | | eqid 2622 |
. . . . . 6
↾t
↾t |
7 | | eqid 2622 |
. . . . . 6
↾t ↾t |
8 | 5, 6, 7 | xkobval 21389 |
. . . . 5
↾t ↾t |
9 | 8 | abeq2i 2735 |
. . . 4
↾t
↾t
|
10 | 2 | adantlr 751 |
. . . . . . . . . . . . . 14
TopOn
TopOn
|
11 | 10 | adantlr 751 |
. . . . . . . . . . . . 13
TopOn
TopOn
↾t |
12 | 11 | adantlr 751 |
. . . . . . . . . . . 12
TopOn TopOn
↾t
|
13 | | simplr 792 |
. . . . . . . . . . . . . 14
TopOn TopOn
↾t
|
14 | 13 | imaeq2d 5466 |
. . . . . . . . . . . . 13
TopOn TopOn
↾t
|
15 | | ima0 5481 |
. . . . . . . . . . . . . 14
|
16 | | 0ss 3972 |
. . . . . . . . . . . . . 14
|
17 | 15, 16 | eqsstri 3635 |
. . . . . . . . . . . . 13
|
18 | 14, 17 | syl6eqss 3655 |
. . . . . . . . . . . 12
TopOn TopOn
↾t
|
19 | | imaeq1 5461 |
. . . . . . . . . . . . . 14
|
20 | 19 | sseq1d 3632 |
. . . . . . . . . . . . 13
|
21 | 20 | elrab 3363 |
. . . . . . . . . . . 12
|
22 | 12, 18, 21 | sylanbrc 698 |
. . . . . . . . . . 11
TopOn TopOn
↾t
|
23 | 22 | ralrimiva 2966 |
. . . . . . . . . 10
TopOn
TopOn
↾t
|
24 | | rabid2 3118 |
. . . . . . . . . 10
|
25 | 23, 24 | sylibr 224 |
. . . . . . . . 9
TopOn
TopOn
↾t |
26 | | simpllr 799 |
. . . . . . . . . . 11
TopOn
TopOn
↾t TopOn |
27 | | toponmax 20730 |
. . . . . . . . . . 11
TopOn
|
28 | 26, 27 | syl 17 |
. . . . . . . . . 10
TopOn
TopOn
↾t |
29 | 28 | adantr 481 |
. . . . . . . . 9
TopOn
TopOn
↾t |
30 | 25, 29 | eqeltrrd 2702 |
. . . . . . . 8
TopOn
TopOn
↾t
|
31 | | ifnefalse 4098 |
. . . . . . . . . . . . . . 15
|
32 | 31 | ad2antlr 763 |
. . . . . . . . . . . . . 14
TopOn TopOn
↾t
|
33 | 32 | eleq2d 2687 |
. . . . . . . . . . . . 13
TopOn TopOn
↾t
|
34 | | vex 3203 |
. . . . . . . . . . . . . . . 16
|
35 | 34 | snss 4316 |
. . . . . . . . . . . . . . 15
|
36 | 33, 35 | syl6bb 276 |
. . . . . . . . . . . . . 14
TopOn TopOn
↾t
|
37 | | df-ima 5127 |
. . . . . . . . . . . . . . . . 17
|
38 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . . . . 22
TopOn
TopOn
↾t |
39 | 38 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
TopOn TopOn
↾t
|
40 | 39 | elpwid 4170 |
. . . . . . . . . . . . . . . . . . . 20
TopOn TopOn
↾t
|
41 | | toponuni 20719 |
. . . . . . . . . . . . . . . . . . . . 21
TopOn
|
42 | 41 | ad5antr 770 |
. . . . . . . . . . . . . . . . . . . 20
TopOn TopOn
↾t
|
43 | 40, 42 | sseqtr4d 3642 |
. . . . . . . . . . . . . . . . . . 19
TopOn TopOn
↾t
|
44 | | xpssres 5434 |
. . . . . . . . . . . . . . . . . . 19
|
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . . 18
TopOn TopOn
↾t
|
46 | 45 | rneqd 5353 |
. . . . . . . . . . . . . . . . 17
TopOn TopOn
↾t
|
47 | 37, 46 | syl5eq 2668 |
. . . . . . . . . . . . . . . 16
TopOn TopOn
↾t
|
48 | | rnxp 5564 |
. . . . . . . . . . . . . . . . 17
|
49 | 48 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
TopOn TopOn
↾t
|
50 | 47, 49 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
TopOn TopOn
↾t
|
51 | 50 | sseq1d 3632 |
. . . . . . . . . . . . . 14
TopOn TopOn
↾t
|
52 | 11 | adantlr 751 |
. . . . . . . . . . . . . . 15
TopOn TopOn
↾t
|
53 | 52 | biantrurd 529 |
. . . . . . . . . . . . . 14
TopOn TopOn
↾t
|
54 | 36, 51, 53 | 3bitr2d 296 |
. . . . . . . . . . . . 13
TopOn TopOn
↾t
|
55 | 33, 54 | bitr3d 270 |
. . . . . . . . . . . 12
TopOn TopOn
↾t
|
56 | 55, 21 | syl6bbr 278 |
. . . . . . . . . . 11
TopOn TopOn
↾t
|
57 | 56 | rabbi2dva 3821 |
. . . . . . . . . 10
TopOn
TopOn
↾t |
58 | | simplrr 801 |
. . . . . . . . . . . . 13
TopOn
TopOn
↾t |
59 | | toponss 20731 |
. . . . . . . . . . . . 13
TopOn |
60 | 26, 58, 59 | syl2anc 693 |
. . . . . . . . . . . 12
TopOn
TopOn
↾t |
61 | 60 | adantr 481 |
. . . . . . . . . . 11
TopOn
TopOn
↾t |
62 | | sseqin2 3817 |
. . . . . . . . . . 11
|
63 | 61, 62 | sylib 208 |
. . . . . . . . . 10
TopOn
TopOn
↾t |
64 | 57, 63 | eqtr3d 2658 |
. . . . . . . . 9
TopOn
TopOn
↾t
|
65 | 58 | adantr 481 |
. . . . . . . . 9
TopOn
TopOn
↾t |
66 | 64, 65 | eqeltrd 2701 |
. . . . . . . 8
TopOn
TopOn
↾t
|
67 | 30, 66 | pm2.61dane 2881 |
. . . . . . 7
TopOn
TopOn
↾t
|
68 | | imaeq2 5462 |
. . . . . . . . 9
|
69 | 3 | mptpreima 5628 |
. . . . . . . . 9
|
70 | 68, 69 | syl6eq 2672 |
. . . . . . . 8
|
71 | 70 | eleq1d 2686 |
. . . . . . 7
|
72 | 67, 71 | syl5ibrcom 237 |
. . . . . 6
TopOn
TopOn
↾t |
73 | 72 | expimpd 629 |
. . . . 5
TopOn TopOn
↾t
|
74 | 73 | rexlimdvva 3038 |
. . . 4
TopOn TopOn
↾t
|
75 | 9, 74 | syl5bi 232 |
. . 3
TopOn TopOn
↾t
|
76 | 75 | ralrimiv 2965 |
. 2
TopOn TopOn
↾t
|
77 | | simpr 477 |
. . 3
TopOn TopOn
TopOn |
78 | | ovex 6678 |
. . . . . 6
|
79 | 78 | pwex 4848 |
. . . . 5
|
80 | 5, 6, 7 | xkotf 21388 |
. . . . . 6
↾t ↾t |
81 | | frn 6053 |
. . . . . 6
↾t ↾t
↾t
|
82 | 80, 81 | ax-mp 5 |
. . . . 5
↾t |
83 | 79, 82 | ssexi 4803 |
. . . 4
↾t |
84 | 83 | a1i 11 |
. . 3
TopOn TopOn
↾t |
85 | | topontop 20718 |
. . . 4
TopOn
|
86 | | topontop 20718 |
. . . 4
TopOn
|
87 | 5, 6, 7 | xkoval 21390 |
. . . 4
↾t
|
88 | 85, 86, 87 | syl2an 494 |
. . 3
TopOn TopOn
↾t
|
89 | | eqid 2622 |
. . . . 5
|
90 | 89 | xkotopon 21403 |
. . . 4
TopOn |
91 | 85, 86, 90 | syl2an 494 |
. . 3
TopOn TopOn
TopOn
|
92 | 77, 84, 88, 91 | subbascn 21058 |
. 2
TopOn TopOn
↾t |
93 | 4, 76, 92 | mpbir2and 957 |
1
TopOn TopOn
|