Step | Hyp | Ref
| Expression |
1 | | nrmtop 22847 |
. . 3
β’ (π½ β Nrm β π½ β Top) |
2 | 1 | adantr 481 |
. 2
β’ ((π½ β Nrm β§
(KQβπ½) β Fre)
β π½ β
Top) |
3 | | simpll 765 |
. . . . 5
β’ (((π½ β Nrm β§
(KQβπ½) β Fre)
β§ (π₯ β π½ β§ π¦ β π₯)) β π½ β Nrm) |
4 | | simprl 769 |
. . . . 5
β’ (((π½ β Nrm β§
(KQβπ½) β Fre)
β§ (π₯ β π½ β§ π¦ β π₯)) β π₯ β π½) |
5 | 2 | adantr 481 |
. . . . . . 7
β’ (((π½ β Nrm β§
(KQβπ½) β Fre)
β§ (π₯ β π½ β§ π¦ β π₯)) β π½ β Top) |
6 | | toptopon2 22427 |
. . . . . . 7
β’ (π½ β Top β π½ β (TopOnββͺ π½)) |
7 | 5, 6 | sylib 217 |
. . . . . 6
β’ (((π½ β Nrm β§
(KQβπ½) β Fre)
β§ (π₯ β π½ β§ π¦ β π₯)) β π½ β (TopOnββͺ π½)) |
8 | | simplr 767 |
. . . . . 6
β’ (((π½ β Nrm β§
(KQβπ½) β Fre)
β§ (π₯ β π½ β§ π¦ β π₯)) β (KQβπ½) β Fre) |
9 | | simprr 771 |
. . . . . . 7
β’ (((π½ β Nrm β§
(KQβπ½) β Fre)
β§ (π₯ β π½ β§ π¦ β π₯)) β π¦ β π₯) |
10 | | elunii 4913 |
. . . . . . 7
β’ ((π¦ β π₯ β§ π₯ β π½) β π¦ β βͺ π½) |
11 | 9, 4, 10 | syl2anc 584 |
. . . . . 6
β’ (((π½ β Nrm β§
(KQβπ½) β Fre)
β§ (π₯ β π½ β§ π¦ β π₯)) β π¦ β βͺ π½) |
12 | | eqid 2732 |
. . . . . . 7
β’ (π§ β βͺ π½
β¦ {π€ β π½ β£ π§ β π€}) = (π§ β βͺ π½ β¦ {π€ β π½ β£ π§ β π€}) |
13 | 12 | r0cld 23249 |
. . . . . 6
β’ ((π½ β (TopOnββͺ π½)
β§ (KQβπ½) β
Fre β§ π¦ β βͺ π½)
β {π β βͺ π½
β£ βπ β
π½ (π β π β π¦ β π)} β (Clsdβπ½)) |
14 | 7, 8, 11, 13 | syl3anc 1371 |
. . . . 5
β’ (((π½ β Nrm β§
(KQβπ½) β Fre)
β§ (π₯ β π½ β§ π¦ β π₯)) β {π β βͺ π½ β£ βπ β π½ (π β π β π¦ β π)} β (Clsdβπ½)) |
15 | | simp1rr 1239 |
. . . . . . 7
β’ ((((π½ β Nrm β§
(KQβπ½) β Fre)
β§ (π₯ β π½ β§ π¦ β π₯)) β§ π β βͺ π½ β§ βπ β π½ (π β π β π¦ β π)) β π¦ β π₯) |
16 | 4 | adantr 481 |
. . . . . . . . 9
β’ ((((π½ β Nrm β§
(KQβπ½) β Fre)
β§ (π₯ β π½ β§ π¦ β π₯)) β§ π β βͺ π½) β π₯ β π½) |
17 | | elequ2 2121 |
. . . . . . . . . . 11
β’ (π = π₯ β (π β π β π β π₯)) |
18 | | elequ2 2121 |
. . . . . . . . . . 11
β’ (π = π₯ β (π¦ β π β π¦ β π₯)) |
19 | 17, 18 | bibi12d 345 |
. . . . . . . . . 10
β’ (π = π₯ β ((π β π β π¦ β π) β (π β π₯ β π¦ β π₯))) |
20 | 19 | rspcv 3608 |
. . . . . . . . 9
β’ (π₯ β π½ β (βπ β π½ (π β π β π¦ β π) β (π β π₯ β π¦ β π₯))) |
21 | 16, 20 | syl 17 |
. . . . . . . 8
β’ ((((π½ β Nrm β§
(KQβπ½) β Fre)
β§ (π₯ β π½ β§ π¦ β π₯)) β§ π β βͺ π½) β (βπ β π½ (π β π β π¦ β π) β (π β π₯ β π¦ β π₯))) |
22 | 21 | 3impia 1117 |
. . . . . . 7
β’ ((((π½ β Nrm β§
(KQβπ½) β Fre)
β§ (π₯ β π½ β§ π¦ β π₯)) β§ π β βͺ π½ β§ βπ β π½ (π β π β π¦ β π)) β (π β π₯ β π¦ β π₯)) |
23 | 15, 22 | mpbird 256 |
. . . . . 6
β’ ((((π½ β Nrm β§
(KQβπ½) β Fre)
β§ (π₯ β π½ β§ π¦ β π₯)) β§ π β βͺ π½ β§ βπ β π½ (π β π β π¦ β π)) β π β π₯) |
24 | 23 | rabssdv 4072 |
. . . . 5
β’ (((π½ β Nrm β§
(KQβπ½) β Fre)
β§ (π₯ β π½ β§ π¦ β π₯)) β {π β βͺ π½ β£ βπ β π½ (π β π β π¦ β π)} β π₯) |
25 | | nrmsep3 22866 |
. . . . 5
β’ ((π½ β Nrm β§ (π₯ β π½ β§ {π β βͺ π½ β£ βπ β π½ (π β π β π¦ β π)} β (Clsdβπ½) β§ {π β βͺ π½ β£ βπ β π½ (π β π β π¦ β π)} β π₯)) β βπ§ β π½ ({π β βͺ π½ β£ βπ β π½ (π β π β π¦ β π)} β π§ β§ ((clsβπ½)βπ§) β π₯)) |
26 | 3, 4, 14, 24, 25 | syl13anc 1372 |
. . . 4
β’ (((π½ β Nrm β§
(KQβπ½) β Fre)
β§ (π₯ β π½ β§ π¦ β π₯)) β βπ§ β π½ ({π β βͺ π½ β£ βπ β π½ (π β π β π¦ β π)} β π§ β§ ((clsβπ½)βπ§) β π₯)) |
27 | | elequ1 2113 |
. . . . . . . . . 10
β’ (π = π¦ β (π β π β π¦ β π)) |
28 | 27 | bibi1d 343 |
. . . . . . . . 9
β’ (π = π¦ β ((π β π β π¦ β π) β (π¦ β π β π¦ β π))) |
29 | 28 | ralbidv 3177 |
. . . . . . . 8
β’ (π = π¦ β (βπ β π½ (π β π β π¦ β π) β βπ β π½ (π¦ β π β π¦ β π))) |
30 | | biidd 261 |
. . . . . . . . 9
β’ (((π½ β Nrm β§
(KQβπ½) β Fre)
β§ (π₯ β π½ β§ π¦ β π₯)) β (π¦ β π β π¦ β π)) |
31 | 30 | ralrimivw 3150 |
. . . . . . . 8
β’ (((π½ β Nrm β§
(KQβπ½) β Fre)
β§ (π₯ β π½ β§ π¦ β π₯)) β βπ β π½ (π¦ β π β π¦ β π)) |
32 | 29, 11, 31 | elrabd 3685 |
. . . . . . 7
β’ (((π½ β Nrm β§
(KQβπ½) β Fre)
β§ (π₯ β π½ β§ π¦ β π₯)) β π¦ β {π β βͺ π½ β£ βπ β π½ (π β π β π¦ β π)}) |
33 | | ssel 3975 |
. . . . . . 7
β’ ({π β βͺ π½
β£ βπ β
π½ (π β π β π¦ β π)} β π§ β (π¦ β {π β βͺ π½ β£ βπ β π½ (π β π β π¦ β π)} β π¦ β π§)) |
34 | 32, 33 | syl5com 31 |
. . . . . 6
β’ (((π½ β Nrm β§
(KQβπ½) β Fre)
β§ (π₯ β π½ β§ π¦ β π₯)) β ({π β βͺ π½ β£ βπ β π½ (π β π β π¦ β π)} β π§ β π¦ β π§)) |
35 | 34 | anim1d 611 |
. . . . 5
β’ (((π½ β Nrm β§
(KQβπ½) β Fre)
β§ (π₯ β π½ β§ π¦ β π₯)) β (({π β βͺ π½ β£ βπ β π½ (π β π β π¦ β π)} β π§ β§ ((clsβπ½)βπ§) β π₯) β (π¦ β π§ β§ ((clsβπ½)βπ§) β π₯))) |
36 | 35 | reximdv 3170 |
. . . 4
β’ (((π½ β Nrm β§
(KQβπ½) β Fre)
β§ (π₯ β π½ β§ π¦ β π₯)) β (βπ§ β π½ ({π β βͺ π½ β£ βπ β π½ (π β π β π¦ β π)} β π§ β§ ((clsβπ½)βπ§) β π₯) β βπ§ β π½ (π¦ β π§ β§ ((clsβπ½)βπ§) β π₯))) |
37 | 26, 36 | mpd 15 |
. . 3
β’ (((π½ β Nrm β§
(KQβπ½) β Fre)
β§ (π₯ β π½ β§ π¦ β π₯)) β βπ§ β π½ (π¦ β π§ β§ ((clsβπ½)βπ§) β π₯)) |
38 | 37 | ralrimivva 3200 |
. 2
β’ ((π½ β Nrm β§
(KQβπ½) β Fre)
β βπ₯ β
π½ βπ¦ β π₯ βπ§ β π½ (π¦ β π§ β§ ((clsβπ½)βπ§) β π₯)) |
39 | | isreg 22843 |
. 2
β’ (π½ β Reg β (π½ β Top β§ βπ₯ β π½ βπ¦ β π₯ βπ§ β π½ (π¦ β π§ β§ ((clsβπ½)βπ§) β π₯))) |
40 | 2, 38, 39 | sylanbrc 583 |
1
β’ ((π½ β Nrm β§
(KQβπ½) β Fre)
β π½ β
Reg) |