Step | Hyp | Ref
| Expression |
1 | | t1top 22681 |
. . . . . 6
β’ (π½ β Fre β π½ β Top) |
2 | | t1sep.1 |
. . . . . . 7
β’ π = βͺ
π½ |
3 | 2 | toptopon 22266 |
. . . . . 6
β’ (π½ β Top β π½ β (TopOnβπ)) |
4 | 1, 3 | sylib 217 |
. . . . 5
β’ (π½ β Fre β π½ β (TopOnβπ)) |
5 | | ist1-2 22698 |
. . . . 5
β’ (π½ β (TopOnβπ) β (π½ β Fre β βπ₯ β π βπ¦ β π (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦))) |
6 | 4, 5 | syl 17 |
. . . 4
β’ (π½ β Fre β (π½ β Fre β βπ₯ β π βπ¦ β π (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦))) |
7 | 6 | ibi 266 |
. . 3
β’ (π½ β Fre β βπ₯ β π βπ¦ β π (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦)) |
8 | | eleq1 2825 |
. . . . . . 7
β’ (π₯ = π΄ β (π₯ β π β π΄ β π)) |
9 | 8 | imbi1d 341 |
. . . . . 6
β’ (π₯ = π΄ β ((π₯ β π β π¦ β π) β (π΄ β π β π¦ β π))) |
10 | 9 | ralbidv 3174 |
. . . . 5
β’ (π₯ = π΄ β (βπ β π½ (π₯ β π β π¦ β π) β βπ β π½ (π΄ β π β π¦ β π))) |
11 | | eqeq1 2740 |
. . . . 5
β’ (π₯ = π΄ β (π₯ = π¦ β π΄ = π¦)) |
12 | 10, 11 | imbi12d 344 |
. . . 4
β’ (π₯ = π΄ β ((βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦) β (βπ β π½ (π΄ β π β π¦ β π) β π΄ = π¦))) |
13 | | eleq1 2825 |
. . . . . . 7
β’ (π¦ = π΅ β (π¦ β π β π΅ β π)) |
14 | 13 | imbi2d 340 |
. . . . . 6
β’ (π¦ = π΅ β ((π΄ β π β π¦ β π) β (π΄ β π β π΅ β π))) |
15 | 14 | ralbidv 3174 |
. . . . 5
β’ (π¦ = π΅ β (βπ β π½ (π΄ β π β π¦ β π) β βπ β π½ (π΄ β π β π΅ β π))) |
16 | | eqeq2 2748 |
. . . . 5
β’ (π¦ = π΅ β (π΄ = π¦ β π΄ = π΅)) |
17 | 15, 16 | imbi12d 344 |
. . . 4
β’ (π¦ = π΅ β ((βπ β π½ (π΄ β π β π¦ β π) β π΄ = π¦) β (βπ β π½ (π΄ β π β π΅ β π) β π΄ = π΅))) |
18 | 12, 17 | rspc2v 3590 |
. . 3
β’ ((π΄ β π β§ π΅ β π) β (βπ₯ β π βπ¦ β π (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦) β (βπ β π½ (π΄ β π β π΅ β π) β π΄ = π΅))) |
19 | 7, 18 | mpan9 507 |
. 2
β’ ((π½ β Fre β§ (π΄ β π β§ π΅ β π)) β (βπ β π½ (π΄ β π β π΅ β π) β π΄ = π΅)) |
20 | 19 | 3impb 1115 |
1
β’ ((π½ β Fre β§ π΄ β π β§ π΅ β π) β (βπ β π½ (π΄ β π β π΅ β π) β π΄ = π΅)) |