Step | Hyp | Ref
| Expression |
1 | | t1top 22704 |
. . 3
β’ (π½ β Fre β π½ β Top) |
2 | | toptopon2 22290 |
. . 3
β’ (π½ β Top β π½ β (TopOnββͺ π½)) |
3 | 1, 2 | sylib 217 |
. 2
β’ (π½ β Fre β π½ β (TopOnββͺ π½)) |
4 | | biimp 214 |
. . . . . . . 8
β’ ((π₯ β π β π¦ β π) β (π₯ β π β π¦ β π)) |
5 | 4 | ralimi 3083 |
. . . . . . 7
β’
(βπ β
π½ (π₯ β π β π¦ β π) β βπ β π½ (π₯ β π β π¦ β π)) |
6 | 5 | imim1i 63 |
. . . . . 6
β’
((βπ β
π½ (π₯ β π β π¦ β π) β π₯ = π¦) β (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦)) |
7 | 6 | ralimi 3083 |
. . . . 5
β’
(βπ¦ β
βͺ π½(βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦) β βπ¦ β βͺ π½(βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦)) |
8 | 7 | ralimi 3083 |
. . . 4
β’
(βπ₯ β
βͺ π½βπ¦ β βͺ π½(βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦) β βπ₯ β βͺ π½βπ¦ β βͺ π½(βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦)) |
9 | 8 | a1i 11 |
. . 3
β’ (π½ β (TopOnββͺ π½)
β (βπ₯ β
βͺ π½βπ¦ β βͺ π½(βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦) β βπ₯ β βͺ π½βπ¦ β βͺ π½(βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦))) |
10 | | ist1-2 22721 |
. . 3
β’ (π½ β (TopOnββͺ π½)
β (π½ β Fre β
βπ₯ β βͺ π½βπ¦ β βͺ π½(βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦))) |
11 | | ist0-2 22718 |
. . 3
β’ (π½ β (TopOnββͺ π½)
β (π½ β Kol2
β βπ₯ β
βͺ π½βπ¦ β βͺ π½(βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦))) |
12 | 9, 10, 11 | 3imtr4d 294 |
. 2
β’ (π½ β (TopOnββͺ π½)
β (π½ β Fre β
π½ β
Kol2)) |
13 | 3, 12 | mpcom 38 |
1
β’ (π½ β Fre β π½ β Kol2) |