| Step | Hyp | Ref
| Expression |
|---|
| 1 | | opnregcld.1 |
. . . . 5
β’ π = βͺ
π½ |
| 2 | 1 | clscld 22550 |
. . . 4
β’ ((π½ β Top β§ π΄ β π) β ((clsβπ½)βπ΄) β (Clsdβπ½)) |
| 3 | | eqcom 2739 |
. . . . 5
β’
(((intβπ½)β((clsβπ½)βπ΄)) = π΄ β π΄ = ((intβπ½)β((clsβπ½)βπ΄))) |
| 4 | 3 | biimpi 215 |
. . . 4
β’
(((intβπ½)β((clsβπ½)βπ΄)) = π΄ β π΄ = ((intβπ½)β((clsβπ½)βπ΄))) |
| 5 | | fveq2 6891 |
. . . . 5
β’ (π = ((clsβπ½)βπ΄) β ((intβπ½)βπ) = ((intβπ½)β((clsβπ½)βπ΄))) |
| 6 | 5 | rspceeqv 3633 |
. . . 4
β’
((((clsβπ½)βπ΄) β (Clsdβπ½) β§ π΄ = ((intβπ½)β((clsβπ½)βπ΄))) β βπ β (Clsdβπ½)π΄ = ((intβπ½)βπ)) |
| 7 | 2, 4, 6 | syl2an 596 |
. . 3
β’ (((π½ β Top β§ π΄ β π) β§ ((intβπ½)β((clsβπ½)βπ΄)) = π΄) β βπ β (Clsdβπ½)π΄ = ((intβπ½)βπ)) |
| 8 | 7 | ex 413 |
. 2
β’ ((π½ β Top β§ π΄ β π) β (((intβπ½)β((clsβπ½)βπ΄)) = π΄ β βπ β (Clsdβπ½)π΄ = ((intβπ½)βπ))) |
| 9 | | cldrcl 22529 |
. . . . . . 7
β’ (π β (Clsdβπ½) β π½ β Top) |
| 10 | 1 | cldss 22532 |
. . . . . . 7
β’ (π β (Clsdβπ½) β π β π) |
| 11 | 1 | ntrss2 22560 |
. . . . . . . . 9
β’ ((π½ β Top β§ π β π) β ((intβπ½)βπ) β π) |
| 12 | 9, 10, 11 | syl2anc 584 |
. . . . . . . 8
β’ (π β (Clsdβπ½) β ((intβπ½)βπ) β π) |
| 13 | 1 | clsss2 22575 |
. . . . . . . 8
β’ ((π β (Clsdβπ½) β§ ((intβπ½)βπ) β π) β ((clsβπ½)β((intβπ½)βπ)) β π) |
| 14 | 12, 13 | mpdan 685 |
. . . . . . 7
β’ (π β (Clsdβπ½) β ((clsβπ½)β((intβπ½)βπ)) β π) |
| 15 | 1 | ntrss 22558 |
. . . . . . 7
β’ ((π½ β Top β§ π β π β§ ((clsβπ½)β((intβπ½)βπ)) β π) β ((intβπ½)β((clsβπ½)β((intβπ½)βπ))) β ((intβπ½)βπ)) |
| 16 | 9, 10, 14, 15 | syl3anc 1371 |
. . . . . 6
β’ (π β (Clsdβπ½) β ((intβπ½)β((clsβπ½)β((intβπ½)βπ))) β ((intβπ½)βπ)) |
| 17 | 1 | ntridm 22571 |
. . . . . . . 8
β’ ((π½ β Top β§ π β π) β ((intβπ½)β((intβπ½)βπ)) = ((intβπ½)βπ)) |
| 18 | 9, 10, 17 | syl2anc 584 |
. . . . . . 7
β’ (π β (Clsdβπ½) β ((intβπ½)β((intβπ½)βπ)) = ((intβπ½)βπ)) |
| 19 | 1 | ntrss3 22563 |
. . . . . . . . . 10
β’ ((π½ β Top β§ π β π) β ((intβπ½)βπ) β π) |
| 20 | 9, 10, 19 | syl2anc 584 |
. . . . . . . . 9
β’ (π β (Clsdβπ½) β ((intβπ½)βπ) β π) |
| 21 | 1 | clsss3 22562 |
. . . . . . . . 9
β’ ((π½ β Top β§
((intβπ½)βπ) β π) β ((clsβπ½)β((intβπ½)βπ)) β π) |
| 22 | 9, 20, 21 | syl2anc 584 |
. . . . . . . 8
β’ (π β (Clsdβπ½) β ((clsβπ½)β((intβπ½)βπ)) β π) |
| 23 | 1 | sscls 22559 |
. . . . . . . . 9
β’ ((π½ β Top β§
((intβπ½)βπ) β π) β ((intβπ½)βπ) β ((clsβπ½)β((intβπ½)βπ))) |
| 24 | 9, 20, 23 | syl2anc 584 |
. . . . . . . 8
β’ (π β (Clsdβπ½) β ((intβπ½)βπ) β ((clsβπ½)β((intβπ½)βπ))) |
| 25 | 1 | ntrss 22558 |
. . . . . . . 8
β’ ((π½ β Top β§
((clsβπ½)β((intβπ½)βπ)) β π β§ ((intβπ½)βπ) β ((clsβπ½)β((intβπ½)βπ))) β ((intβπ½)β((intβπ½)βπ)) β ((intβπ½)β((clsβπ½)β((intβπ½)βπ)))) |
| 26 | 9, 22, 24, 25 | syl3anc 1371 |
. . . . . . 7
β’ (π β (Clsdβπ½) β ((intβπ½)β((intβπ½)βπ)) β ((intβπ½)β((clsβπ½)β((intβπ½)βπ)))) |
| 27 | 18, 26 | eqsstrrd 4021 |
. . . . . 6
β’ (π β (Clsdβπ½) β ((intβπ½)βπ) β ((intβπ½)β((clsβπ½)β((intβπ½)βπ)))) |
| 28 | 16, 27 | eqssd 3999 |
. . . . 5
β’ (π β (Clsdβπ½) β ((intβπ½)β((clsβπ½)β((intβπ½)βπ))) = ((intβπ½)βπ)) |
| 29 | 28 | adantl 482 |
. . . 4
β’ (((π½ β Top β§ π΄ β π) β§ π β (Clsdβπ½)) β ((intβπ½)β((clsβπ½)β((intβπ½)βπ))) = ((intβπ½)βπ)) |
| 30 | | 2fveq3 6896 |
. . . . 5
β’ (π΄ = ((intβπ½)βπ) β ((intβπ½)β((clsβπ½)βπ΄)) = ((intβπ½)β((clsβπ½)β((intβπ½)βπ)))) |
| 31 | | id 22 |
. . . . 5
β’ (π΄ = ((intβπ½)βπ) β π΄ = ((intβπ½)βπ)) |
| 32 | 30, 31 | eqeq12d 2748 |
. . . 4
β’ (π΄ = ((intβπ½)βπ) β (((intβπ½)β((clsβπ½)βπ΄)) = π΄ β ((intβπ½)β((clsβπ½)β((intβπ½)βπ))) = ((intβπ½)βπ))) |
| 33 | 29, 32 | syl5ibrcom 246 |
. . 3
β’ (((π½ β Top β§ π΄ β π) β§ π β (Clsdβπ½)) β (π΄ = ((intβπ½)βπ) β ((intβπ½)β((clsβπ½)βπ΄)) = π΄)) |
| 34 | 33 | rexlimdva 3155 |
. 2
β’ ((π½ β Top β§ π΄ β π) β (βπ β (Clsdβπ½)π΄ = ((intβπ½)βπ) β ((intβπ½)β((clsβπ½)βπ΄)) = π΄)) |
| 35 | 8, 34 | impbid 211 |
1
β’ ((π½ β Top β§ π΄ β π) β (((intβπ½)β((clsβπ½)βπ΄)) = π΄ β βπ β (Clsdβπ½)π΄ = ((intβπ½)βπ))) |
