Step | Hyp | Ref
| Expression |
1 | | nfv 1918 |
. . . 4
β’
β²π¦((π½ β Top β§ πΎ β Top) β§ (π
β (Clsdβ(π½ Γt πΎ)) β§ π΄ β π)) |
2 | | nfcv 2908 |
. . . 4
β’
β²π¦(π
β {π΄}) |
3 | | nfrab1 3429 |
. . . 4
β’
β²π¦{π¦ β βͺ πΎ β£ β¨π΄, π¦β© β π
} |
4 | | simprl 770 |
. . . . . . . . . . . 12
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (Clsdβ(π½ Γt πΎ)) β§ π΄ β π)) β π
β (Clsdβ(π½ Γt πΎ))) |
5 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ βͺ (π½
Γt πΎ) =
βͺ (π½ Γt πΎ) |
6 | 5 | cldss 22396 |
. . . . . . . . . . . 12
β’ (π
β (Clsdβ(π½ Γt πΎ)) β π
β βͺ (π½ Γt πΎ)) |
7 | 4, 6 | syl 17 |
. . . . . . . . . . 11
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (Clsdβ(π½ Γt πΎ)) β§ π΄ β π)) β π
β βͺ (π½ Γt πΎ)) |
8 | | imasnopn.1 |
. . . . . . . . . . . . 13
β’ π = βͺ
π½ |
9 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ βͺ πΎ =
βͺ πΎ |
10 | 8, 9 | txuni 22959 |
. . . . . . . . . . . 12
β’ ((π½ β Top β§ πΎ β Top) β (π Γ βͺ πΎ) =
βͺ (π½ Γt πΎ)) |
11 | 10 | adantr 482 |
. . . . . . . . . . 11
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (Clsdβ(π½ Γt πΎ)) β§ π΄ β π)) β (π Γ βͺ πΎ) = βͺ
(π½ Γt
πΎ)) |
12 | 7, 11 | sseqtrrd 3990 |
. . . . . . . . . 10
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (Clsdβ(π½ Γt πΎ)) β§ π΄ β π)) β π
β (π Γ βͺ πΎ)) |
13 | | imass1 6058 |
. . . . . . . . . 10
β’ (π
β (π Γ βͺ πΎ) β (π
β {π΄}) β ((π Γ βͺ πΎ) β {π΄})) |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (Clsdβ(π½ Γt πΎ)) β§ π΄ β π)) β (π
β {π΄}) β ((π Γ βͺ πΎ) β {π΄})) |
15 | | xpimasn 6142 |
. . . . . . . . . 10
β’ (π΄ β π β ((π Γ βͺ πΎ) β {π΄}) = βͺ πΎ) |
16 | 15 | ad2antll 728 |
. . . . . . . . 9
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (Clsdβ(π½ Γt πΎ)) β§ π΄ β π)) β ((π Γ βͺ πΎ) β {π΄}) = βͺ πΎ) |
17 | 14, 16 | sseqtrd 3989 |
. . . . . . . 8
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (Clsdβ(π½ Γt πΎ)) β§ π΄ β π)) β (π
β {π΄}) β βͺ
πΎ) |
18 | 17 | sseld 3948 |
. . . . . . 7
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (Clsdβ(π½ Γt πΎ)) β§ π΄ β π)) β (π¦ β (π
β {π΄}) β π¦ β βͺ πΎ)) |
19 | 18 | pm4.71rd 564 |
. . . . . 6
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (Clsdβ(π½ Γt πΎ)) β§ π΄ β π)) β (π¦ β (π
β {π΄}) β (π¦ β βͺ πΎ β§ π¦ β (π
β {π΄})))) |
20 | | elimasng 6045 |
. . . . . . . . 9
β’ ((π΄ β π β§ π¦ β V) β (π¦ β (π
β {π΄}) β β¨π΄, π¦β© β π
)) |
21 | 20 | elvd 3455 |
. . . . . . . 8
β’ (π΄ β π β (π¦ β (π
β {π΄}) β β¨π΄, π¦β© β π
)) |
22 | 21 | ad2antll 728 |
. . . . . . 7
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (Clsdβ(π½ Γt πΎ)) β§ π΄ β π)) β (π¦ β (π
β {π΄}) β β¨π΄, π¦β© β π
)) |
23 | 22 | anbi2d 630 |
. . . . . 6
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (Clsdβ(π½ Γt πΎ)) β§ π΄ β π)) β ((π¦ β βͺ πΎ β§ π¦ β (π
β {π΄})) β (π¦ β βͺ πΎ β§ β¨π΄, π¦β© β π
))) |
24 | 19, 23 | bitrd 279 |
. . . . 5
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (Clsdβ(π½ Γt πΎ)) β§ π΄ β π)) β (π¦ β (π
β {π΄}) β (π¦ β βͺ πΎ β§ β¨π΄, π¦β© β π
))) |
25 | | rabid 3430 |
. . . . 5
β’ (π¦ β {π¦ β βͺ πΎ β£ β¨π΄, π¦β© β π
} β (π¦ β βͺ πΎ β§ β¨π΄, π¦β© β π
)) |
26 | 24, 25 | bitr4di 289 |
. . . 4
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (Clsdβ(π½ Γt πΎ)) β§ π΄ β π)) β (π¦ β (π
β {π΄}) β π¦ β {π¦ β βͺ πΎ β£ β¨π΄, π¦β© β π
})) |
27 | 1, 2, 3, 26 | eqrd 3968 |
. . 3
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (Clsdβ(π½ Γt πΎ)) β§ π΄ β π)) β (π
β {π΄}) = {π¦ β βͺ πΎ β£ β¨π΄, π¦β© β π
}) |
28 | | eqid 2737 |
. . . 4
β’ (π¦ β βͺ πΎ
β¦ β¨π΄, π¦β©) = (π¦ β βͺ πΎ β¦ β¨π΄, π¦β©) |
29 | 28 | mptpreima 6195 |
. . 3
β’ (β‘(π¦ β βͺ πΎ β¦ β¨π΄, π¦β©) β π
) = {π¦ β βͺ πΎ β£ β¨π΄, π¦β© β π
} |
30 | 27, 29 | eqtr4di 2795 |
. 2
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (Clsdβ(π½ Γt πΎ)) β§ π΄ β π)) β (π
β {π΄}) = (β‘(π¦ β βͺ πΎ β¦ β¨π΄, π¦β©) β π
)) |
31 | 9 | toptopon 22282 |
. . . . . 6
β’ (πΎ β Top β πΎ β (TopOnββͺ πΎ)) |
32 | 31 | biimpi 215 |
. . . . 5
β’ (πΎ β Top β πΎ β (TopOnββͺ πΎ)) |
33 | 32 | ad2antlr 726 |
. . . 4
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (Clsdβ(π½ Γt πΎ)) β§ π΄ β π)) β πΎ β (TopOnββͺ πΎ)) |
34 | 8 | toptopon 22282 |
. . . . . . 7
β’ (π½ β Top β π½ β (TopOnβπ)) |
35 | 34 | biimpi 215 |
. . . . . 6
β’ (π½ β Top β π½ β (TopOnβπ)) |
36 | 35 | ad2antrr 725 |
. . . . 5
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (Clsdβ(π½ Γt πΎ)) β§ π΄ β π)) β π½ β (TopOnβπ)) |
37 | | simprr 772 |
. . . . 5
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (Clsdβ(π½ Γt πΎ)) β§ π΄ β π)) β π΄ β π) |
38 | 33, 36, 37 | cnmptc 23029 |
. . . 4
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (Clsdβ(π½ Γt πΎ)) β§ π΄ β π)) β (π¦ β βͺ πΎ β¦ π΄) β (πΎ Cn π½)) |
39 | 33 | cnmptid 23028 |
. . . 4
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (Clsdβ(π½ Γt πΎ)) β§ π΄ β π)) β (π¦ β βͺ πΎ β¦ π¦) β (πΎ Cn πΎ)) |
40 | 33, 38, 39 | cnmpt1t 23032 |
. . 3
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (Clsdβ(π½ Γt πΎ)) β§ π΄ β π)) β (π¦ β βͺ πΎ β¦ β¨π΄, π¦β©) β (πΎ Cn (π½ Γt πΎ))) |
41 | | cnclima 22635 |
. . 3
β’ (((π¦ β βͺ πΎ
β¦ β¨π΄, π¦β©) β (πΎ Cn (π½ Γt πΎ)) β§ π
β (Clsdβ(π½ Γt πΎ))) β (β‘(π¦ β βͺ πΎ β¦ β¨π΄, π¦β©) β π
) β (ClsdβπΎ)) |
42 | 40, 4, 41 | syl2anc 585 |
. 2
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (Clsdβ(π½ Γt πΎ)) β§ π΄ β π)) β (β‘(π¦ β βͺ πΎ β¦ β¨π΄, π¦β©) β π
) β (ClsdβπΎ)) |
43 | 30, 42 | eqeltrd 2838 |
1
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (Clsdβ(π½ Γt πΎ)) β§ π΄ β π)) β (π
β {π΄}) β (ClsdβπΎ)) |