Step | Hyp | Ref
| Expression |
1 | | simp1 1136 |
. . . . . . . . 9
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β π½ β (TopOnβπ)) |
2 | | elpwi 4609 |
. . . . . . . . 9
β’ (π β π« π β π β π) |
3 | | resttopon 22885 |
. . . . . . . . 9
β’ ((π½ β (TopOnβπ) β§ π β π) β (π½ βΎt π) β (TopOnβπ)) |
4 | 1, 2, 3 | syl2an 596 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β§ π β π« π) β (π½ βΎt π) β (TopOnβπ)) |
5 | | simp2 1137 |
. . . . . . . . . . 11
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β πΎ β (TopOnβπ)) |
6 | | resttopon 22885 |
. . . . . . . . . . 11
β’ ((πΎ β (TopOnβπ) β§ π β π) β (πΎ βΎt π) β (TopOnβπ)) |
7 | 5, 2, 6 | syl2an 596 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β§ π β π« π) β (πΎ βΎt π) β (TopOnβπ)) |
8 | | toponuni 22636 |
. . . . . . . . . 10
β’ ((πΎ βΎt π) β (TopOnβπ) β π = βͺ (πΎ βΎt π)) |
9 | 7, 8 | syl 17 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β§ π β π« π) β π = βͺ (πΎ βΎt π)) |
10 | 9 | fveq2d 6895 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β§ π β π« π) β (TopOnβπ) = (TopOnββͺ
(πΎ βΎt
π))) |
11 | 4, 10 | eleqtrd 2835 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β§ π β π« π) β (π½ βΎt π) β (TopOnββͺ (πΎ
βΎt π))) |
12 | | simpl2 1192 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β§ π β π« π) β πΎ β (TopOnβπ)) |
13 | | topontop 22635 |
. . . . . . . . 9
β’ (πΎ β (TopOnβπ) β πΎ β Top) |
14 | 12, 13 | syl 17 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β§ π β π« π) β πΎ β Top) |
15 | | simpl3 1193 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β§ π β π« π) β π½ β πΎ) |
16 | | ssrest 22900 |
. . . . . . . 8
β’ ((πΎ β Top β§ π½ β πΎ) β (π½ βΎt π) β (πΎ βΎt π)) |
17 | 14, 15, 16 | syl2anc 584 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β§ π β π« π) β (π½ βΎt π) β (πΎ βΎt π)) |
18 | | eqid 2732 |
. . . . . . . . . 10
β’ βͺ (πΎ
βΎt π) =
βͺ (πΎ βΎt π) |
19 | 18 | sscmp 23129 |
. . . . . . . . 9
β’ (((π½ βΎt π) β (TopOnββͺ (πΎ
βΎt π))
β§ (πΎ
βΎt π)
β Comp β§ (π½
βΎt π)
β (πΎ
βΎt π))
β (π½
βΎt π)
β Comp) |
20 | 19 | 3com23 1126 |
. . . . . . . 8
β’ (((π½ βΎt π) β (TopOnββͺ (πΎ
βΎt π))
β§ (π½
βΎt π)
β (πΎ
βΎt π)
β§ (πΎ
βΎt π)
β Comp) β (π½
βΎt π)
β Comp) |
21 | 20 | 3expia 1121 |
. . . . . . 7
β’ (((π½ βΎt π) β (TopOnββͺ (πΎ
βΎt π))
β§ (π½
βΎt π)
β (πΎ
βΎt π))
β ((πΎ
βΎt π)
β Comp β (π½
βΎt π)
β Comp)) |
22 | 11, 17, 21 | syl2anc 584 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β§ π β π« π) β ((πΎ βΎt π) β Comp β (π½ βΎt π) β Comp)) |
23 | 17 | sseld 3981 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β§ π β π« π) β ((π₯ β© π) β (π½ βΎt π) β (π₯ β© π) β (πΎ βΎt π))) |
24 | 22, 23 | imim12d 81 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β§ π β π« π) β (((π½ βΎt π) β Comp β (π₯ β© π) β (π½ βΎt π)) β ((πΎ βΎt π) β Comp β (π₯ β© π) β (πΎ βΎt π)))) |
25 | 24 | ralimdva 3167 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β (βπ β π« π((π½ βΎt π) β Comp β (π₯ β© π) β (π½ βΎt π)) β βπ β π« π((πΎ βΎt π) β Comp β (π₯ β© π) β (πΎ βΎt π)))) |
26 | 25 | anim2d 612 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β ((π₯ β π β§ βπ β π« π((π½ βΎt π) β Comp β (π₯ β© π) β (π½ βΎt π))) β (π₯ β π β§ βπ β π« π((πΎ βΎt π) β Comp β (π₯ β© π) β (πΎ βΎt π))))) |
27 | | elkgen 23260 |
. . . 4
β’ (π½ β (TopOnβπ) β (π₯ β (πGenβπ½) β (π₯ β π β§ βπ β π« π((π½ βΎt π) β Comp β (π₯ β© π) β (π½ βΎt π))))) |
28 | 27 | 3ad2ant1 1133 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β (π₯ β (πGenβπ½) β (π₯ β π β§ βπ β π« π((π½ βΎt π) β Comp β (π₯ β© π) β (π½ βΎt π))))) |
29 | | elkgen 23260 |
. . . 4
β’ (πΎ β (TopOnβπ) β (π₯ β (πGenβπΎ) β (π₯ β π β§ βπ β π« π((πΎ βΎt π) β Comp β (π₯ β© π) β (πΎ βΎt π))))) |
30 | 29 | 3ad2ant2 1134 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β (π₯ β (πGenβπΎ) β (π₯ β π β§ βπ β π« π((πΎ βΎt π) β Comp β (π₯ β© π) β (πΎ βΎt π))))) |
31 | 26, 28, 30 | 3imtr4d 293 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β (π₯ β (πGenβπ½) β π₯ β (πGenβπΎ))) |
32 | 31 | ssrdv 3988 |
1
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β (πGenβπ½) β
(πGenβπΎ)) |