Step | Hyp | Ref
| Expression |
1 | | opnregcld.1 |
. . . . 5
β’ π = βͺ
π½ |
2 | 1 | clscld 22421 |
. . . 4
β’ ((π½ β Top β§ π΄ β π) β ((clsβπ½)βπ΄) β (Clsdβπ½)) |
3 | | eqcom 2740 |
. . . . 5
β’
(((intβπ½)β((clsβπ½)βπ΄)) = π΄ β π΄ = ((intβπ½)β((clsβπ½)βπ΄))) |
4 | 3 | biimpi 215 |
. . . 4
β’
(((intβπ½)β((clsβπ½)βπ΄)) = π΄ β π΄ = ((intβπ½)β((clsβπ½)βπ΄))) |
5 | | fveq2 6846 |
. . . . 5
β’ (π = ((clsβπ½)βπ΄) β ((intβπ½)βπ) = ((intβπ½)β((clsβπ½)βπ΄))) |
6 | 5 | rspceeqv 3599 |
. . . 4
β’
((((clsβπ½)βπ΄) β (Clsdβπ½) β§ π΄ = ((intβπ½)β((clsβπ½)βπ΄))) β βπ β (Clsdβπ½)π΄ = ((intβπ½)βπ)) |
7 | 2, 4, 6 | syl2an 597 |
. . 3
β’ (((π½ β Top β§ π΄ β π) β§ ((intβπ½)β((clsβπ½)βπ΄)) = π΄) β βπ β (Clsdβπ½)π΄ = ((intβπ½)βπ)) |
8 | 7 | ex 414 |
. 2
β’ ((π½ β Top β§ π΄ β π) β (((intβπ½)β((clsβπ½)βπ΄)) = π΄ β βπ β (Clsdβπ½)π΄ = ((intβπ½)βπ))) |
9 | | cldrcl 22400 |
. . . . . . 7
β’ (π β (Clsdβπ½) β π½ β Top) |
10 | 1 | cldss 22403 |
. . . . . . 7
β’ (π β (Clsdβπ½) β π β π) |
11 | 1 | ntrss2 22431 |
. . . . . . . . 9
β’ ((π½ β Top β§ π β π) β ((intβπ½)βπ) β π) |
12 | 9, 10, 11 | syl2anc 585 |
. . . . . . . 8
β’ (π β (Clsdβπ½) β ((intβπ½)βπ) β π) |
13 | 1 | clsss2 22446 |
. . . . . . . 8
β’ ((π β (Clsdβπ½) β§ ((intβπ½)βπ) β π) β ((clsβπ½)β((intβπ½)βπ)) β π) |
14 | 12, 13 | mpdan 686 |
. . . . . . 7
β’ (π β (Clsdβπ½) β ((clsβπ½)β((intβπ½)βπ)) β π) |
15 | 1 | ntrss 22429 |
. . . . . . 7
β’ ((π½ β Top β§ π β π β§ ((clsβπ½)β((intβπ½)βπ)) β π) β ((intβπ½)β((clsβπ½)β((intβπ½)βπ))) β ((intβπ½)βπ)) |
16 | 9, 10, 14, 15 | syl3anc 1372 |
. . . . . 6
β’ (π β (Clsdβπ½) β ((intβπ½)β((clsβπ½)β((intβπ½)βπ))) β ((intβπ½)βπ)) |
17 | 1 | ntridm 22442 |
. . . . . . . 8
β’ ((π½ β Top β§ π β π) β ((intβπ½)β((intβπ½)βπ)) = ((intβπ½)βπ)) |
18 | 9, 10, 17 | syl2anc 585 |
. . . . . . 7
β’ (π β (Clsdβπ½) β ((intβπ½)β((intβπ½)βπ)) = ((intβπ½)βπ)) |
19 | 1 | ntrss3 22434 |
. . . . . . . . . 10
β’ ((π½ β Top β§ π β π) β ((intβπ½)βπ) β π) |
20 | 9, 10, 19 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (Clsdβπ½) β ((intβπ½)βπ) β π) |
21 | 1 | clsss3 22433 |
. . . . . . . . 9
β’ ((π½ β Top β§
((intβπ½)βπ) β π) β ((clsβπ½)β((intβπ½)βπ)) β π) |
22 | 9, 20, 21 | syl2anc 585 |
. . . . . . . 8
β’ (π β (Clsdβπ½) β ((clsβπ½)β((intβπ½)βπ)) β π) |
23 | 1 | sscls 22430 |
. . . . . . . . 9
β’ ((π½ β Top β§
((intβπ½)βπ) β π) β ((intβπ½)βπ) β ((clsβπ½)β((intβπ½)βπ))) |
24 | 9, 20, 23 | syl2anc 585 |
. . . . . . . 8
β’ (π β (Clsdβπ½) β ((intβπ½)βπ) β ((clsβπ½)β((intβπ½)βπ))) |
25 | 1 | ntrss 22429 |
. . . . . . . 8
β’ ((π½ β Top β§
((clsβπ½)β((intβπ½)βπ)) β π β§ ((intβπ½)βπ) β ((clsβπ½)β((intβπ½)βπ))) β ((intβπ½)β((intβπ½)βπ)) β ((intβπ½)β((clsβπ½)β((intβπ½)βπ)))) |
26 | 9, 22, 24, 25 | syl3anc 1372 |
. . . . . . 7
β’ (π β (Clsdβπ½) β ((intβπ½)β((intβπ½)βπ)) β ((intβπ½)β((clsβπ½)β((intβπ½)βπ)))) |
27 | 18, 26 | eqsstrrd 3987 |
. . . . . 6
β’ (π β (Clsdβπ½) β ((intβπ½)βπ) β ((intβπ½)β((clsβπ½)β((intβπ½)βπ)))) |
28 | 16, 27 | eqssd 3965 |
. . . . 5
β’ (π β (Clsdβπ½) β ((intβπ½)β((clsβπ½)β((intβπ½)βπ))) = ((intβπ½)βπ)) |
29 | 28 | adantl 483 |
. . . 4
β’ (((π½ β Top β§ π΄ β π) β§ π β (Clsdβπ½)) β ((intβπ½)β((clsβπ½)β((intβπ½)βπ))) = ((intβπ½)βπ)) |
30 | | 2fveq3 6851 |
. . . . 5
β’ (π΄ = ((intβπ½)βπ) β ((intβπ½)β((clsβπ½)βπ΄)) = ((intβπ½)β((clsβπ½)β((intβπ½)βπ)))) |
31 | | id 22 |
. . . . 5
β’ (π΄ = ((intβπ½)βπ) β π΄ = ((intβπ½)βπ)) |
32 | 30, 31 | eqeq12d 2749 |
. . . 4
β’ (π΄ = ((intβπ½)βπ) β (((intβπ½)β((clsβπ½)βπ΄)) = π΄ β ((intβπ½)β((clsβπ½)β((intβπ½)βπ))) = ((intβπ½)βπ))) |
33 | 29, 32 | syl5ibrcom 247 |
. . 3
β’ (((π½ β Top β§ π΄ β π) β§ π β (Clsdβπ½)) β (π΄ = ((intβπ½)βπ) β ((intβπ½)β((clsβπ½)βπ΄)) = π΄)) |
34 | 33 | rexlimdva 3149 |
. 2
β’ ((π½ β Top β§ π΄ β π) β (βπ β (Clsdβπ½)π΄ = ((intβπ½)βπ) β ((intβπ½)β((clsβπ½)βπ΄)) = π΄)) |
35 | 8, 34 | impbid 211 |
1
β’ ((π½ β Top β§ π΄ β π) β (((intβπ½)β((clsβπ½)βπ΄)) = π΄ β βπ β (Clsdβπ½)π΄ = ((intβπ½)βπ))) |