Step | Hyp | Ref
| Expression |
1 | | qtopomap.5 |
. . 3
β’ (π β πΉ β (π½ Cn πΎ)) |
2 | | qtopomap.4 |
. . 3
β’ (π β πΎ β (TopOnβπ)) |
3 | | qtopomap.6 |
. . 3
β’ (π β ran πΉ = π) |
4 | | qtopss 23089 |
. . 3
β’ ((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β πΎ β (π½ qTop πΉ)) |
5 | 1, 2, 3, 4 | syl3anc 1372 |
. 2
β’ (π β πΎ β (π½ qTop πΉ)) |
6 | | cntop1 22614 |
. . . . . . 7
β’ (πΉ β (π½ Cn πΎ) β π½ β Top) |
7 | 1, 6 | syl 17 |
. . . . . 6
β’ (π β π½ β Top) |
8 | | toptopon2 22290 |
. . . . . 6
β’ (π½ β Top β π½ β (TopOnββͺ π½)) |
9 | 7, 8 | sylib 217 |
. . . . 5
β’ (π β π½ β (TopOnββͺ π½)) |
10 | | cnf2 22623 |
. . . . . . . 8
β’ ((π½ β (TopOnββͺ π½)
β§ πΎ β
(TopOnβπ) β§ πΉ β (π½ Cn πΎ)) β πΉ:βͺ π½βΆπ) |
11 | 9, 2, 1, 10 | syl3anc 1372 |
. . . . . . 7
β’ (π β πΉ:βͺ π½βΆπ) |
12 | 11 | ffnd 6673 |
. . . . . 6
β’ (π β πΉ Fn βͺ π½) |
13 | | df-fo 6506 |
. . . . . 6
β’ (πΉ:βͺ
π½βontoβπ β (πΉ Fn βͺ π½ β§ ran πΉ = π)) |
14 | 12, 3, 13 | sylanbrc 584 |
. . . . 5
β’ (π β πΉ:βͺ π½βontoβπ) |
15 | | elqtop3 23077 |
. . . . 5
β’ ((π½ β (TopOnββͺ π½)
β§ πΉ:βͺ π½βontoβπ) β (π¦ β (π½ qTop πΉ) β (π¦ β π β§ (β‘πΉ β π¦) β π½))) |
16 | 9, 14, 15 | syl2anc 585 |
. . . 4
β’ (π β (π¦ β (π½ qTop πΉ) β (π¦ β π β§ (β‘πΉ β π¦) β π½))) |
17 | | foimacnv 6805 |
. . . . . . . 8
β’ ((πΉ:βͺ
π½βontoβπ β§ π¦ β π) β (πΉ β (β‘πΉ β π¦)) = π¦) |
18 | 14, 17 | sylan 581 |
. . . . . . 7
β’ ((π β§ π¦ β π) β (πΉ β (β‘πΉ β π¦)) = π¦) |
19 | 18 | adantrr 716 |
. . . . . 6
β’ ((π β§ (π¦ β π β§ (β‘πΉ β π¦) β π½)) β (πΉ β (β‘πΉ β π¦)) = π¦) |
20 | | imaeq2 6013 |
. . . . . . . 8
β’ (π₯ = (β‘πΉ β π¦) β (πΉ β π₯) = (πΉ β (β‘πΉ β π¦))) |
21 | 20 | eleq1d 2819 |
. . . . . . 7
β’ (π₯ = (β‘πΉ β π¦) β ((πΉ β π₯) β πΎ β (πΉ β (β‘πΉ β π¦)) β πΎ)) |
22 | | qtopomap.7 |
. . . . . . . . 9
β’ ((π β§ π₯ β π½) β (πΉ β π₯) β πΎ) |
23 | 22 | ralrimiva 3140 |
. . . . . . . 8
β’ (π β βπ₯ β π½ (πΉ β π₯) β πΎ) |
24 | 23 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π¦ β π β§ (β‘πΉ β π¦) β π½)) β βπ₯ β π½ (πΉ β π₯) β πΎ) |
25 | | simprr 772 |
. . . . . . 7
β’ ((π β§ (π¦ β π β§ (β‘πΉ β π¦) β π½)) β (β‘πΉ β π¦) β π½) |
26 | 21, 24, 25 | rspcdva 3584 |
. . . . . 6
β’ ((π β§ (π¦ β π β§ (β‘πΉ β π¦) β π½)) β (πΉ β (β‘πΉ β π¦)) β πΎ) |
27 | 19, 26 | eqeltrrd 2835 |
. . . . 5
β’ ((π β§ (π¦ β π β§ (β‘πΉ β π¦) β π½)) β π¦ β πΎ) |
28 | 27 | ex 414 |
. . . 4
β’ (π β ((π¦ β π β§ (β‘πΉ β π¦) β π½) β π¦ β πΎ)) |
29 | 16, 28 | sylbid 239 |
. . 3
β’ (π β (π¦ β (π½ qTop πΉ) β π¦ β πΎ)) |
30 | 29 | ssrdv 3954 |
. 2
β’ (π β (π½ qTop πΉ) β πΎ) |
31 | 5, 30 | eqssd 3965 |
1
β’ (π β πΎ = (π½ qTop πΉ)) |