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