Step | Hyp | Ref
| Expression |
1 | | opnregcld.1 |
. . . . 5
β’ π = βͺ
π½ |
2 | 1 | ntropn 22423 |
. . . 4
β’ ((π½ β Top β§ π΄ β π) β ((intβπ½)βπ΄) β π½) |
3 | | eqcom 2740 |
. . . . 5
β’
(((clsβπ½)β((intβπ½)βπ΄)) = π΄ β π΄ = ((clsβπ½)β((intβπ½)βπ΄))) |
4 | 3 | biimpi 215 |
. . . 4
β’
(((clsβπ½)β((intβπ½)βπ΄)) = π΄ β π΄ = ((clsβπ½)β((intβπ½)βπ΄))) |
5 | | fveq2 6846 |
. . . . 5
β’ (π = ((intβπ½)βπ΄) β ((clsβπ½)βπ) = ((clsβπ½)β((intβπ½)βπ΄))) |
6 | 5 | rspceeqv 3599 |
. . . 4
β’
((((intβπ½)βπ΄) β π½ β§ π΄ = ((clsβπ½)β((intβπ½)βπ΄))) β βπ β π½ π΄ = ((clsβπ½)βπ)) |
7 | 2, 4, 6 | syl2an 597 |
. . 3
β’ (((π½ β Top β§ π΄ β π) β§ ((clsβπ½)β((intβπ½)βπ΄)) = π΄) β βπ β π½ π΄ = ((clsβπ½)βπ)) |
8 | 7 | ex 414 |
. 2
β’ ((π½ β Top β§ π΄ β π) β (((clsβπ½)β((intβπ½)βπ΄)) = π΄ β βπ β π½ π΄ = ((clsβπ½)βπ))) |
9 | | simpl 484 |
. . . . . . . 8
β’ ((π½ β Top β§ π β π½) β π½ β Top) |
10 | 1 | eltopss 22279 |
. . . . . . . . 9
β’ ((π½ β Top β§ π β π½) β π β π) |
11 | 1 | clsss3 22433 |
. . . . . . . . 9
β’ ((π½ β Top β§ π β π) β ((clsβπ½)βπ) β π) |
12 | 10, 11 | syldan 592 |
. . . . . . . 8
β’ ((π½ β Top β§ π β π½) β ((clsβπ½)βπ) β π) |
13 | 1 | ntrss2 22431 |
. . . . . . . . 9
β’ ((π½ β Top β§
((clsβπ½)βπ) β π) β ((intβπ½)β((clsβπ½)βπ)) β ((clsβπ½)βπ)) |
14 | 12, 13 | syldan 592 |
. . . . . . . 8
β’ ((π½ β Top β§ π β π½) β ((intβπ½)β((clsβπ½)βπ)) β ((clsβπ½)βπ)) |
15 | 1 | clsss 22428 |
. . . . . . . 8
β’ ((π½ β Top β§
((clsβπ½)βπ) β π β§ ((intβπ½)β((clsβπ½)βπ)) β ((clsβπ½)βπ)) β ((clsβπ½)β((intβπ½)β((clsβπ½)βπ))) β ((clsβπ½)β((clsβπ½)βπ))) |
16 | 9, 12, 14, 15 | syl3anc 1372 |
. . . . . . 7
β’ ((π½ β Top β§ π β π½) β ((clsβπ½)β((intβπ½)β((clsβπ½)βπ))) β ((clsβπ½)β((clsβπ½)βπ))) |
17 | 1 | clsidm 22441 |
. . . . . . . 8
β’ ((π½ β Top β§ π β π) β ((clsβπ½)β((clsβπ½)βπ)) = ((clsβπ½)βπ)) |
18 | 10, 17 | syldan 592 |
. . . . . . 7
β’ ((π½ β Top β§ π β π½) β ((clsβπ½)β((clsβπ½)βπ)) = ((clsβπ½)βπ)) |
19 | 16, 18 | sseqtrd 3988 |
. . . . . 6
β’ ((π½ β Top β§ π β π½) β ((clsβπ½)β((intβπ½)β((clsβπ½)βπ))) β ((clsβπ½)βπ)) |
20 | 1 | ntrss3 22434 |
. . . . . . . 8
β’ ((π½ β Top β§
((clsβπ½)βπ) β π) β ((intβπ½)β((clsβπ½)βπ)) β π) |
21 | 12, 20 | syldan 592 |
. . . . . . 7
β’ ((π½ β Top β§ π β π½) β ((intβπ½)β((clsβπ½)βπ)) β π) |
22 | | simpr 486 |
. . . . . . . 8
β’ ((π½ β Top β§ π β π½) β π β π½) |
23 | 1 | sscls 22430 |
. . . . . . . . 9
β’ ((π½ β Top β§ π β π) β π β ((clsβπ½)βπ)) |
24 | 10, 23 | syldan 592 |
. . . . . . . 8
β’ ((π½ β Top β§ π β π½) β π β ((clsβπ½)βπ)) |
25 | 1 | ssntr 22432 |
. . . . . . . 8
β’ (((π½ β Top β§
((clsβπ½)βπ) β π) β§ (π β π½ β§ π β ((clsβπ½)βπ))) β π β ((intβπ½)β((clsβπ½)βπ))) |
26 | 9, 12, 22, 24, 25 | syl22anc 838 |
. . . . . . 7
β’ ((π½ β Top β§ π β π½) β π β ((intβπ½)β((clsβπ½)βπ))) |
27 | 1 | clsss 22428 |
. . . . . . 7
β’ ((π½ β Top β§
((intβπ½)β((clsβπ½)βπ)) β π β§ π β ((intβπ½)β((clsβπ½)βπ))) β ((clsβπ½)βπ) β ((clsβπ½)β((intβπ½)β((clsβπ½)βπ)))) |
28 | 9, 21, 26, 27 | syl3anc 1372 |
. . . . . 6
β’ ((π½ β Top β§ π β π½) β ((clsβπ½)βπ) β ((clsβπ½)β((intβπ½)β((clsβπ½)βπ)))) |
29 | 19, 28 | eqssd 3965 |
. . . . 5
β’ ((π½ β Top β§ π β π½) β ((clsβπ½)β((intβπ½)β((clsβπ½)βπ))) = ((clsβπ½)βπ)) |
30 | 29 | adantlr 714 |
. . . 4
β’ (((π½ β Top β§ π΄ β π) β§ π β π½) β ((clsβπ½)β((intβπ½)β((clsβπ½)βπ))) = ((clsβπ½)βπ)) |
31 | | 2fveq3 6851 |
. . . . 5
β’ (π΄ = ((clsβπ½)βπ) β ((clsβπ½)β((intβπ½)βπ΄)) = ((clsβπ½)β((intβπ½)β((clsβπ½)βπ)))) |
32 | | id 22 |
. . . . 5
β’ (π΄ = ((clsβπ½)βπ) β π΄ = ((clsβπ½)βπ)) |
33 | 31, 32 | eqeq12d 2749 |
. . . 4
β’ (π΄ = ((clsβπ½)βπ) β (((clsβπ½)β((intβπ½)βπ΄)) = π΄ β ((clsβπ½)β((intβπ½)β((clsβπ½)βπ))) = ((clsβπ½)βπ))) |
34 | 30, 33 | syl5ibrcom 247 |
. . 3
β’ (((π½ β Top β§ π΄ β π) β§ π β π½) β (π΄ = ((clsβπ½)βπ) β ((clsβπ½)β((intβπ½)βπ΄)) = π΄)) |
35 | 34 | rexlimdva 3149 |
. 2
β’ ((π½ β Top β§ π΄ β π) β (βπ β π½ π΄ = ((clsβπ½)βπ) β ((clsβπ½)β((intβπ½)βπ΄)) = π΄)) |
36 | 8, 35 | impbid 211 |
1
β’ ((π½ β Top β§ π΄ β π) β (((clsβπ½)β((intβπ½)βπ΄)) = π΄ β βπ β π½ π΄ = ((clsβπ½)βπ))) |