Step | Hyp | Ref
| Expression |
1 | | cnvimass 6080 |
. . . . . . 7
β’ (β‘πΊ β π₯) β dom πΊ |
2 | | simplrr 776 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβontoβπ β§ πΊ:πβΆπ)) β§ π₯ β πΎ) β πΊ:πβΆπ) |
3 | 1, 2 | fssdm 6737 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβontoβπ β§ πΊ:πβΆπ)) β§ π₯ β πΎ) β (β‘πΊ β π₯) β π) |
4 | | simplll 773 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβontoβπ β§ πΊ:πβΆπ)) β§ π₯ β πΎ) β π½ β (TopOnβπ)) |
5 | | simplrl 775 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβontoβπ β§ πΊ:πβΆπ)) β§ π₯ β πΎ) β πΉ:πβontoβπ) |
6 | | elqtop3 23206 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β ((β‘πΊ β π₯) β (π½ qTop πΉ) β ((β‘πΊ β π₯) β π β§ (β‘πΉ β (β‘πΊ β π₯)) β π½))) |
7 | 4, 5, 6 | syl2anc 584 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβontoβπ β§ πΊ:πβΆπ)) β§ π₯ β πΎ) β ((β‘πΊ β π₯) β (π½ qTop πΉ) β ((β‘πΊ β π₯) β π β§ (β‘πΉ β (β‘πΊ β π₯)) β π½))) |
8 | 3, 7 | mpbirand 705 |
. . . . 5
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβontoβπ β§ πΊ:πβΆπ)) β§ π₯ β πΎ) β ((β‘πΊ β π₯) β (π½ qTop πΉ) β (β‘πΉ β (β‘πΊ β π₯)) β π½)) |
9 | | cnvco 5885 |
. . . . . . . 8
β’ β‘(πΊ β πΉ) = (β‘πΉ β β‘πΊ) |
10 | 9 | imaeq1i 6056 |
. . . . . . 7
β’ (β‘(πΊ β πΉ) β π₯) = ((β‘πΉ β β‘πΊ) β π₯) |
11 | | imaco 6250 |
. . . . . . 7
β’ ((β‘πΉ β β‘πΊ) β π₯) = (β‘πΉ β (β‘πΊ β π₯)) |
12 | 10, 11 | eqtri 2760 |
. . . . . 6
β’ (β‘(πΊ β πΉ) β π₯) = (β‘πΉ β (β‘πΊ β π₯)) |
13 | 12 | eleq1i 2824 |
. . . . 5
β’ ((β‘(πΊ β πΉ) β π₯) β π½ β (β‘πΉ β (β‘πΊ β π₯)) β π½) |
14 | 8, 13 | bitr4di 288 |
. . . 4
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβontoβπ β§ πΊ:πβΆπ)) β§ π₯ β πΎ) β ((β‘πΊ β π₯) β (π½ qTop πΉ) β (β‘(πΊ β πΉ) β π₯) β π½)) |
15 | 14 | ralbidva 3175 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβontoβπ β§ πΊ:πβΆπ)) β (βπ₯ β πΎ (β‘πΊ β π₯) β (π½ qTop πΉ) β βπ₯ β πΎ (β‘(πΊ β πΉ) β π₯) β π½)) |
16 | | simprr 771 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβontoβπ β§ πΊ:πβΆπ)) β πΊ:πβΆπ) |
17 | 16 | biantrurd 533 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβontoβπ β§ πΊ:πβΆπ)) β (βπ₯ β πΎ (β‘πΊ β π₯) β (π½ qTop πΉ) β (πΊ:πβΆπ β§ βπ₯ β πΎ (β‘πΊ β π₯) β (π½ qTop πΉ)))) |
18 | | fof 6805 |
. . . . . 6
β’ (πΉ:πβontoβπ β πΉ:πβΆπ) |
19 | 18 | ad2antrl 726 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβontoβπ β§ πΊ:πβΆπ)) β πΉ:πβΆπ) |
20 | | fco 6741 |
. . . . 5
β’ ((πΊ:πβΆπ β§ πΉ:πβΆπ) β (πΊ β πΉ):πβΆπ) |
21 | 16, 19, 20 | syl2anc 584 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβontoβπ β§ πΊ:πβΆπ)) β (πΊ β πΉ):πβΆπ) |
22 | 21 | biantrurd 533 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβontoβπ β§ πΊ:πβΆπ)) β (βπ₯ β πΎ (β‘(πΊ β πΉ) β π₯) β π½ β ((πΊ β πΉ):πβΆπ β§ βπ₯ β πΎ (β‘(πΊ β πΉ) β π₯) β π½))) |
23 | 15, 17, 22 | 3bitr3d 308 |
. 2
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβontoβπ β§ πΊ:πβΆπ)) β ((πΊ:πβΆπ β§ βπ₯ β πΎ (β‘πΊ β π₯) β (π½ qTop πΉ)) β ((πΊ β πΉ):πβΆπ β§ βπ₯ β πΎ (β‘(πΊ β πΉ) β π₯) β π½))) |
24 | | qtoptopon 23207 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β (π½ qTop πΉ) β (TopOnβπ)) |
25 | 24 | ad2ant2r 745 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβontoβπ β§ πΊ:πβΆπ)) β (π½ qTop πΉ) β (TopOnβπ)) |
26 | | simplr 767 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβontoβπ β§ πΊ:πβΆπ)) β πΎ β (TopOnβπ)) |
27 | | iscn 22738 |
. . 3
β’ (((π½ qTop πΉ) β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (πΊ β ((π½ qTop πΉ) Cn πΎ) β (πΊ:πβΆπ β§ βπ₯ β πΎ (β‘πΊ β π₯) β (π½ qTop πΉ)))) |
28 | 25, 26, 27 | syl2anc 584 |
. 2
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβontoβπ β§ πΊ:πβΆπ)) β (πΊ β ((π½ qTop πΉ) Cn πΎ) β (πΊ:πβΆπ β§ βπ₯ β πΎ (β‘πΊ β π₯) β (π½ qTop πΉ)))) |
29 | | iscn 22738 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β ((πΊ β πΉ) β (π½ Cn πΎ) β ((πΊ β πΉ):πβΆπ β§ βπ₯ β πΎ (β‘(πΊ β πΉ) β π₯) β π½))) |
30 | 29 | adantr 481 |
. 2
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβontoβπ β§ πΊ:πβΆπ)) β ((πΊ β πΉ) β (π½ Cn πΎ) β ((πΊ β πΉ):πβΆπ β§ βπ₯ β πΎ (β‘(πΊ β πΉ) β π₯) β π½))) |
31 | 23, 28, 30 | 3bitr4d 310 |
1
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβontoβπ β§ πΊ:πβΆπ)) β (πΊ β ((π½ qTop πΉ) Cn πΎ) β (πΊ β πΉ) β (π½ Cn πΎ))) |