Step | Hyp | Ref
| Expression |
1 | | imasnopn.2 |
. . . . . . 7
β’ π = βͺ
πΎ |
2 | 1 | toptopon 22282 |
. . . . . 6
β’ (πΎ β Top β πΎ β (TopOnβπ)) |
3 | 2 | biimpi 215 |
. . . . 5
β’ (πΎ β Top β πΎ β (TopOnβπ)) |
4 | 3 | ad2antlr 726 |
. . . 4
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β πΎ β (TopOnβπ)) |
5 | | imasnopn.1 |
. . . . . . . 8
β’ π = βͺ
π½ |
6 | 5 | toptopon 22282 |
. . . . . . 7
β’ (π½ β Top β π½ β (TopOnβπ)) |
7 | 6 | biimpi 215 |
. . . . . 6
β’ (π½ β Top β π½ β (TopOnβπ)) |
8 | 7 | ad2antrr 725 |
. . . . 5
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β π½ β (TopOnβπ)) |
9 | | simprr 772 |
. . . . 5
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β π΄ β π) |
10 | 4, 8, 9 | cnmptc 23029 |
. . . 4
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β (π¦ β π β¦ π΄) β (πΎ Cn π½)) |
11 | 4 | cnmptid 23028 |
. . . 4
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β (π¦ β π β¦ π¦) β (πΎ Cn πΎ)) |
12 | 4, 10, 11 | cnmpt1t 23032 |
. . 3
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β (π¦ β π β¦ β¨π΄, π¦β©) β (πΎ Cn (π½ Γt πΎ))) |
13 | | simprl 770 |
. . . 4
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β π
β (π Γ π)) |
14 | 5, 1 | txuni 22959 |
. . . . 5
β’ ((π½ β Top β§ πΎ β Top) β (π Γ π) = βͺ (π½ Γt πΎ)) |
15 | 14 | adantr 482 |
. . . 4
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β (π Γ π) = βͺ (π½ Γt πΎ)) |
16 | 13, 15 | sseqtrd 3989 |
. . 3
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β π
β βͺ (π½ Γt πΎ)) |
17 | | eqid 2737 |
. . . 4
β’ βͺ (π½
Γt πΎ) =
βͺ (π½ Γt πΎ) |
18 | 17 | cncls2i 22637 |
. . 3
β’ (((π¦ β π β¦ β¨π΄, π¦β©) β (πΎ Cn (π½ Γt πΎ)) β§ π
β βͺ (π½ Γt πΎ)) β ((clsβπΎ)β(β‘(π¦ β π β¦ β¨π΄, π¦β©) β π
)) β (β‘(π¦ β π β¦ β¨π΄, π¦β©) β ((clsβ(π½ Γt πΎ))βπ
))) |
19 | 12, 16, 18 | syl2anc 585 |
. 2
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β ((clsβπΎ)β(β‘(π¦ β π β¦ β¨π΄, π¦β©) β π
)) β (β‘(π¦ β π β¦ β¨π΄, π¦β©) β ((clsβ(π½ Γt πΎ))βπ
))) |
20 | | nfv 1918 |
. . . . 5
β’
β²π¦((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) |
21 | | nfcv 2908 |
. . . . 5
β’
β²π¦(π
β {π΄}) |
22 | | nfrab1 3429 |
. . . . 5
β’
β²π¦{π¦ β π β£ β¨π΄, π¦β© β π
} |
23 | | imass1 6058 |
. . . . . . . . . . 11
β’ (π
β (π Γ π) β (π
β {π΄}) β ((π Γ π) β {π΄})) |
24 | 13, 23 | syl 17 |
. . . . . . . . . 10
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β (π
β {π΄}) β ((π Γ π) β {π΄})) |
25 | | xpimasn 6142 |
. . . . . . . . . . 11
β’ (π΄ β π β ((π Γ π) β {π΄}) = π) |
26 | 25 | ad2antll 728 |
. . . . . . . . . 10
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β ((π Γ π) β {π΄}) = π) |
27 | 24, 26 | sseqtrd 3989 |
. . . . . . . . 9
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β (π
β {π΄}) β π) |
28 | 27 | sseld 3948 |
. . . . . . . 8
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β (π¦ β (π
β {π΄}) β π¦ β π)) |
29 | 28 | pm4.71rd 564 |
. . . . . . 7
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β (π¦ β (π
β {π΄}) β (π¦ β π β§ π¦ β (π
β {π΄})))) |
30 | | elimasng 6045 |
. . . . . . . . . 10
β’ ((π΄ β π β§ π¦ β V) β (π¦ β (π
β {π΄}) β β¨π΄, π¦β© β π
)) |
31 | 30 | elvd 3455 |
. . . . . . . . 9
β’ (π΄ β π β (π¦ β (π
β {π΄}) β β¨π΄, π¦β© β π
)) |
32 | 31 | ad2antll 728 |
. . . . . . . 8
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β (π¦ β (π
β {π΄}) β β¨π΄, π¦β© β π
)) |
33 | 32 | anbi2d 630 |
. . . . . . 7
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β ((π¦ β π β§ π¦ β (π
β {π΄})) β (π¦ β π β§ β¨π΄, π¦β© β π
))) |
34 | 29, 33 | bitrd 279 |
. . . . . 6
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β (π¦ β (π
β {π΄}) β (π¦ β π β§ β¨π΄, π¦β© β π
))) |
35 | | rabid 3430 |
. . . . . 6
β’ (π¦ β {π¦ β π β£ β¨π΄, π¦β© β π
} β (π¦ β π β§ β¨π΄, π¦β© β π
)) |
36 | 34, 35 | bitr4di 289 |
. . . . 5
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β (π¦ β (π
β {π΄}) β π¦ β {π¦ β π β£ β¨π΄, π¦β© β π
})) |
37 | 20, 21, 22, 36 | eqrd 3968 |
. . . 4
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β (π
β {π΄}) = {π¦ β π β£ β¨π΄, π¦β© β π
}) |
38 | | eqid 2737 |
. . . . 5
β’ (π¦ β π β¦ β¨π΄, π¦β©) = (π¦ β π β¦ β¨π΄, π¦β©) |
39 | 38 | mptpreima 6195 |
. . . 4
β’ (β‘(π¦ β π β¦ β¨π΄, π¦β©) β π
) = {π¦ β π β£ β¨π΄, π¦β© β π
} |
40 | 37, 39 | eqtr4di 2795 |
. . 3
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β (π
β {π΄}) = (β‘(π¦ β π β¦ β¨π΄, π¦β©) β π
)) |
41 | 40 | fveq2d 6851 |
. 2
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β ((clsβπΎ)β(π
β {π΄})) = ((clsβπΎ)β(β‘(π¦ β π β¦ β¨π΄, π¦β©) β π
))) |
42 | | nfcv 2908 |
. . . 4
β’
β²π¦(((clsβ(π½ Γt πΎ))βπ
) β {π΄}) |
43 | | nfrab1 3429 |
. . . 4
β’
β²π¦{π¦ β π β£ β¨π΄, π¦β© β ((clsβ(π½ Γt πΎ))βπ
)} |
44 | | txtop 22936 |
. . . . . . . . . . . . 13
β’ ((π½ β Top β§ πΎ β Top) β (π½ Γt πΎ) β Top) |
45 | 44 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β (π½ Γt πΎ) β Top) |
46 | 17 | clsss3 22426 |
. . . . . . . . . . . 12
β’ (((π½ Γt πΎ) β Top β§ π
β βͺ (π½
Γt πΎ))
β ((clsβ(π½
Γt πΎ))βπ
) β βͺ
(π½ Γt
πΎ)) |
47 | 45, 16, 46 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β ((clsβ(π½ Γt πΎ))βπ
) β βͺ
(π½ Γt
πΎ)) |
48 | 47, 15 | sseqtrrd 3990 |
. . . . . . . . . 10
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β ((clsβ(π½ Γt πΎ))βπ
) β (π Γ π)) |
49 | | imass1 6058 |
. . . . . . . . . 10
β’
(((clsβ(π½
Γt πΎ))βπ
) β (π Γ π) β (((clsβ(π½ Γt πΎ))βπ
) β {π΄}) β ((π Γ π) β {π΄})) |
50 | 48, 49 | syl 17 |
. . . . . . . . 9
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β (((clsβ(π½ Γt πΎ))βπ
) β {π΄}) β ((π Γ π) β {π΄})) |
51 | 50, 26 | sseqtrd 3989 |
. . . . . . . 8
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β (((clsβ(π½ Γt πΎ))βπ
) β {π΄}) β π) |
52 | 51 | sseld 3948 |
. . . . . . 7
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β (π¦ β (((clsβ(π½ Γt πΎ))βπ
) β {π΄}) β π¦ β π)) |
53 | 52 | pm4.71rd 564 |
. . . . . 6
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β (π¦ β (((clsβ(π½ Γt πΎ))βπ
) β {π΄}) β (π¦ β π β§ π¦ β (((clsβ(π½ Γt πΎ))βπ
) β {π΄})))) |
54 | | elimasng 6045 |
. . . . . . . . 9
β’ ((π΄ β π β§ π¦ β V) β (π¦ β (((clsβ(π½ Γt πΎ))βπ
) β {π΄}) β β¨π΄, π¦β© β ((clsβ(π½ Γt πΎ))βπ
))) |
55 | 54 | elvd 3455 |
. . . . . . . 8
β’ (π΄ β π β (π¦ β (((clsβ(π½ Γt πΎ))βπ
) β {π΄}) β β¨π΄, π¦β© β ((clsβ(π½ Γt πΎ))βπ
))) |
56 | 55 | ad2antll 728 |
. . . . . . 7
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β (π¦ β (((clsβ(π½ Γt πΎ))βπ
) β {π΄}) β β¨π΄, π¦β© β ((clsβ(π½ Γt πΎ))βπ
))) |
57 | 56 | anbi2d 630 |
. . . . . 6
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β ((π¦ β π β§ π¦ β (((clsβ(π½ Γt πΎ))βπ
) β {π΄})) β (π¦ β π β§ β¨π΄, π¦β© β ((clsβ(π½ Γt πΎ))βπ
)))) |
58 | 53, 57 | bitrd 279 |
. . . . 5
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β (π¦ β (((clsβ(π½ Γt πΎ))βπ
) β {π΄}) β (π¦ β π β§ β¨π΄, π¦β© β ((clsβ(π½ Γt πΎ))βπ
)))) |
59 | | rabid 3430 |
. . . . 5
β’ (π¦ β {π¦ β π β£ β¨π΄, π¦β© β ((clsβ(π½ Γt πΎ))βπ
)} β (π¦ β π β§ β¨π΄, π¦β© β ((clsβ(π½ Γt πΎ))βπ
))) |
60 | 58, 59 | bitr4di 289 |
. . . 4
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β (π¦ β (((clsβ(π½ Γt πΎ))βπ
) β {π΄}) β π¦ β {π¦ β π β£ β¨π΄, π¦β© β ((clsβ(π½ Γt πΎ))βπ
)})) |
61 | 20, 42, 43, 60 | eqrd 3968 |
. . 3
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β (((clsβ(π½ Γt πΎ))βπ
) β {π΄}) = {π¦ β π β£ β¨π΄, π¦β© β ((clsβ(π½ Γt πΎ))βπ
)}) |
62 | 38 | mptpreima 6195 |
. . 3
β’ (β‘(π¦ β π β¦ β¨π΄, π¦β©) β ((clsβ(π½ Γt πΎ))βπ
)) = {π¦ β π β£ β¨π΄, π¦β© β ((clsβ(π½ Γt πΎ))βπ
)} |
63 | 61, 62 | eqtr4di 2795 |
. 2
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β (((clsβ(π½ Γt πΎ))βπ
) β {π΄}) = (β‘(π¦ β π β¦ β¨π΄, π¦β©) β ((clsβ(π½ Γt πΎ))βπ
))) |
64 | 19, 41, 63 | 3sstr4d 3996 |
1
β’ (((π½ β Top β§ πΎ β Top) β§ (π
β (π Γ π) β§ π΄ β π)) β ((clsβπΎ)β(π
β {π΄})) β (((clsβ(π½ Γt πΎ))βπ
) β {π΄})) |