Step | Hyp | Ref
| Expression |
1 | | simpll 527 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β π½ β (TopOnβπ)) |
2 | | toptopon2 13010 |
. . . . . 6
β’ (πΎ β Top β πΎ β (TopOnββͺ πΎ)) |
3 | 2 | biimpi 120 |
. . . . 5
β’ (πΎ β Top β πΎ β (TopOnββͺ πΎ)) |
4 | 3 | ad2antlr 489 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β πΎ β (TopOnββͺ πΎ)) |
5 | | simpr3 1005 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β πΉ β ((π½ CnP πΎ)βπ)) |
6 | | cnpf2 13200 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnββͺ πΎ)
β§ πΉ β ((π½ CnP πΎ)βπ)) β πΉ:πβΆβͺ πΎ) |
7 | 1, 4, 5, 6 | syl3anc 1238 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β πΉ:πβΆβͺ πΎ) |
8 | | simpr1 1003 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β π΄ β π) |
9 | 7, 8 | fssresd 5384 |
. 2
β’ (((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β (πΉ βΎ π΄):π΄βΆβͺ πΎ) |
10 | | simplr2 1040 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β§ π¦ β πΎ) β π β π΄) |
11 | | fvres 5531 |
. . . . . 6
β’ (π β π΄ β ((πΉ βΎ π΄)βπ) = (πΉβπ)) |
12 | 10, 11 | syl 14 |
. . . . 5
β’ ((((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β§ π¦ β πΎ) β ((πΉ βΎ π΄)βπ) = (πΉβπ)) |
13 | 12 | eleq1d 2244 |
. . . 4
β’ ((((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β§ π¦ β πΎ) β (((πΉ βΎ π΄)βπ) β π¦ β (πΉβπ) β π¦)) |
14 | 1 | ad2antrr 488 |
. . . . . . 7
β’
(((((π½ β
(TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β§ π¦ β πΎ) β§ (πΉβπ) β π¦) β π½ β (TopOnβπ)) |
15 | 4 | ad2antrr 488 |
. . . . . . 7
β’
(((((π½ β
(TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β§ π¦ β πΎ) β§ (πΉβπ) β π¦) β πΎ β (TopOnββͺ πΎ)) |
16 | 8 | ad2antrr 488 |
. . . . . . . 8
β’
(((((π½ β
(TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β§ π¦ β πΎ) β§ (πΉβπ) β π¦) β π΄ β π) |
17 | | simpr2 1004 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β π β π΄) |
18 | 17 | ad2antrr 488 |
. . . . . . . 8
β’
(((((π½ β
(TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β§ π¦ β πΎ) β§ (πΉβπ) β π¦) β π β π΄) |
19 | 16, 18 | sseldd 3154 |
. . . . . . 7
β’
(((((π½ β
(TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β§ π¦ β πΎ) β§ (πΉβπ) β π¦) β π β π) |
20 | 5 | ad2antrr 488 |
. . . . . . 7
β’
(((((π½ β
(TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β§ π¦ β πΎ) β§ (πΉβπ) β π¦) β πΉ β ((π½ CnP πΎ)βπ)) |
21 | | simplr 528 |
. . . . . . 7
β’
(((((π½ β
(TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β§ π¦ β πΎ) β§ (πΉβπ) β π¦) β π¦ β πΎ) |
22 | | simpr 110 |
. . . . . . 7
β’
(((((π½ β
(TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β§ π¦ β πΎ) β§ (πΉβπ) β π¦) β (πΉβπ) β π¦) |
23 | | icnpimaex 13204 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnββͺ πΎ)
β§ π β π) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π¦ β πΎ β§ (πΉβπ) β π¦)) β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦)) |
24 | 14, 15, 19, 20, 21, 22, 23 | syl33anc 1253 |
. . . . . 6
β’
(((((π½ β
(TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β§ π¦ β πΎ) β§ (πΉβπ) β π¦) β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦)) |
25 | 24 | ex 115 |
. . . . 5
β’ ((((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β§ π¦ β πΎ) β ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦))) |
26 | | idd 21 |
. . . . . . . . . . 11
β’ (((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β (π β π₯ β π β π₯)) |
27 | 26, 17 | jctird 317 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β (π β π₯ β (π β π₯ β§ π β π΄))) |
28 | | elin 3316 |
. . . . . . . . . 10
β’ (π β (π₯ β© π΄) β (π β π₯ β§ π β π΄)) |
29 | 27, 28 | syl6ibr 162 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β (π β π₯ β π β (π₯ β© π΄))) |
30 | | inss1 3353 |
. . . . . . . . . . . 12
β’ (π₯ β© π΄) β π₯ |
31 | | imass2 4997 |
. . . . . . . . . . . 12
β’ ((π₯ β© π΄) β π₯ β (πΉ β (π₯ β© π΄)) β (πΉ β π₯)) |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . . . 11
β’ (πΉ β (π₯ β© π΄)) β (πΉ β π₯) |
33 | | id 19 |
. . . . . . . . . . 11
β’ ((πΉ β π₯) β π¦ β (πΉ β π₯) β π¦) |
34 | 32, 33 | sstrid 3164 |
. . . . . . . . . 10
β’ ((πΉ β π₯) β π¦ β (πΉ β (π₯ β© π΄)) β π¦) |
35 | 34 | a1i 9 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β ((πΉ β π₯) β π¦ β (πΉ β (π₯ β© π΄)) β π¦)) |
36 | 29, 35 | anim12d 335 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β ((π β π₯ β§ (πΉ β π₯) β π¦) β (π β (π₯ β© π΄) β§ (πΉ β (π₯ β© π΄)) β π¦))) |
37 | 36 | reximdv 2576 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β (βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦) β βπ₯ β π½ (π β (π₯ β© π΄) β§ (πΉ β (π₯ β© π΄)) β π¦))) |
38 | | vex 2738 |
. . . . . . . . . 10
β’ π₯ β V |
39 | 38 | inex1 4132 |
. . . . . . . . 9
β’ (π₯ β© π΄) β V |
40 | 39 | a1i 9 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β§ π₯ β π½) β (π₯ β© π΄) β V) |
41 | | topontop 13005 |
. . . . . . . . . 10
β’ (π½ β (TopOnβπ) β π½ β Top) |
42 | 41 | ad2antrr 488 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β π½ β Top) |
43 | | uniexg 4433 |
. . . . . . . . . . 11
β’ (π½ β Top β βͺ π½
β V) |
44 | 42, 43 | syl 14 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β βͺ
π½ β
V) |
45 | | toponuni 13006 |
. . . . . . . . . . . . 13
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
46 | 45 | sseq2d 3183 |
. . . . . . . . . . . 12
β’ (π½ β (TopOnβπ) β (π΄ β π β π΄ β βͺ π½)) |
47 | 46 | ad2antrr 488 |
. . . . . . . . . . 11
β’ (((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β (π΄ β π β π΄ β βͺ π½)) |
48 | 8, 47 | mpbid 147 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β π΄ β βͺ π½) |
49 | 44, 48 | ssexd 4138 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β π΄ β V) |
50 | | elrest 12616 |
. . . . . . . . 9
β’ ((π½ β Top β§ π΄ β V) β (π§ β (π½ βΎt π΄) β βπ₯ β π½ π§ = (π₯ β© π΄))) |
51 | 42, 49, 50 | syl2anc 411 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β (π§ β (π½ βΎt π΄) β βπ₯ β π½ π§ = (π₯ β© π΄))) |
52 | | simpr 110 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β§ π§ = (π₯ β© π΄)) β π§ = (π₯ β© π΄)) |
53 | 52 | eleq2d 2245 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β§ π§ = (π₯ β© π΄)) β (π β π§ β π β (π₯ β© π΄))) |
54 | 52 | imaeq2d 4963 |
. . . . . . . . . . 11
β’ ((((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β§ π§ = (π₯ β© π΄)) β ((πΉ βΎ π΄) β π§) = ((πΉ βΎ π΄) β (π₯ β© π΄))) |
55 | | inss2 3354 |
. . . . . . . . . . . 12
β’ (π₯ β© π΄) β π΄ |
56 | | resima2 4934 |
. . . . . . . . . . . 12
β’ ((π₯ β© π΄) β π΄ β ((πΉ βΎ π΄) β (π₯ β© π΄)) = (πΉ β (π₯ β© π΄))) |
57 | 55, 56 | ax-mp 5 |
. . . . . . . . . . 11
β’ ((πΉ βΎ π΄) β (π₯ β© π΄)) = (πΉ β (π₯ β© π΄)) |
58 | 54, 57 | eqtrdi 2224 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β§ π§ = (π₯ β© π΄)) β ((πΉ βΎ π΄) β π§) = (πΉ β (π₯ β© π΄))) |
59 | 58 | sseq1d 3182 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β§ π§ = (π₯ β© π΄)) β (((πΉ βΎ π΄) β π§) β π¦ β (πΉ β (π₯ β© π΄)) β π¦)) |
60 | 53, 59 | anbi12d 473 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β§ π§ = (π₯ β© π΄)) β ((π β π§ β§ ((πΉ βΎ π΄) β π§) β π¦) β (π β (π₯ β© π΄) β§ (πΉ β (π₯ β© π΄)) β π¦))) |
61 | 40, 51, 60 | rexxfr2d 4459 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β (βπ§ β (π½ βΎt π΄)(π β π§ β§ ((πΉ βΎ π΄) β π§) β π¦) β βπ₯ β π½ (π β (π₯ β© π΄) β§ (πΉ β (π₯ β© π΄)) β π¦))) |
62 | 37, 61 | sylibrd 169 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β (βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦) β βπ§ β (π½ βΎt π΄)(π β π§ β§ ((πΉ βΎ π΄) β π§) β π¦))) |
63 | 62 | adantr 276 |
. . . . 5
β’ ((((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β§ π¦ β πΎ) β (βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦) β βπ§ β (π½ βΎt π΄)(π β π§ β§ ((πΉ βΎ π΄) β π§) β π¦))) |
64 | 25, 63 | syld 45 |
. . . 4
β’ ((((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β§ π¦ β πΎ) β ((πΉβπ) β π¦ β βπ§ β (π½ βΎt π΄)(π β π§ β§ ((πΉ βΎ π΄) β π§) β π¦))) |
65 | 13, 64 | sylbid 150 |
. . 3
β’ ((((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β§ π¦ β πΎ) β (((πΉ βΎ π΄)βπ) β π¦ β βπ§ β (π½ βΎt π΄)(π β π§ β§ ((πΉ βΎ π΄) β π§) β π¦))) |
66 | 65 | ralrimiva 2548 |
. 2
β’ (((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β βπ¦ β πΎ (((πΉ βΎ π΄)βπ) β π¦ β βπ§ β (π½ βΎt π΄)(π β π§ β§ ((πΉ βΎ π΄) β π§) β π¦))) |
67 | | resttopon 13164 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π½ βΎt π΄) β (TopOnβπ΄)) |
68 | 1, 8, 67 | syl2anc 411 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β (π½ βΎt π΄) β (TopOnβπ΄)) |
69 | | iscnp 13192 |
. . 3
β’ (((π½ βΎt π΄) β (TopOnβπ΄) β§ πΎ β (TopOnββͺ πΎ)
β§ π β π΄) β ((πΉ βΎ π΄) β (((π½ βΎt π΄) CnP πΎ)βπ) β ((πΉ βΎ π΄):π΄βΆβͺ πΎ β§ βπ¦ β πΎ (((πΉ βΎ π΄)βπ) β π¦ β βπ§ β (π½ βΎt π΄)(π β π§ β§ ((πΉ βΎ π΄) β π§) β π¦))))) |
70 | 68, 4, 17, 69 | syl3anc 1238 |
. 2
β’ (((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β ((πΉ βΎ π΄) β (((π½ βΎt π΄) CnP πΎ)βπ) β ((πΉ βΎ π΄):π΄βΆβͺ πΎ β§ βπ¦ β πΎ (((πΉ βΎ π΄)βπ) β π¦ β βπ§ β (π½ βΎt π΄)(π β π§ β§ ((πΉ βΎ π΄) β π§) β π¦))))) |
71 | 9, 66, 70 | mpbir2and 944 |
1
β’ (((π½ β (TopOnβπ) β§ πΎ β Top) β§ (π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ))) β (πΉ βΎ π΄) β (((π½ βΎt π΄) CnP πΎ)βπ)) |