Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . 5
β’ ((((π
β Top β§ π β Top) β§ (π β β
β§ π β β
)) β§ (π
Γt π) β Comp) β (π
Γt π) β Comp) |
2 | | simplrr 777 |
. . . . . . 7
β’ ((((π
β Top β§ π β Top) β§ (π β β
β§ π β β
)) β§ (π
Γt π) β Comp) β π β β
) |
3 | | fo1stres 7951 |
. . . . . . 7
β’ (π β β
β
(1st βΎ (π
Γ π)):(π Γ π)βontoβπ) |
4 | 2, 3 | syl 17 |
. . . . . 6
β’ ((((π
β Top β§ π β Top) β§ (π β β
β§ π β β
)) β§ (π
Γt π) β Comp) β
(1st βΎ (π
Γ π)):(π Γ π)βontoβπ) |
5 | | txcmpb.1 |
. . . . . . . . 9
β’ π = βͺ
π
|
6 | | txcmpb.2 |
. . . . . . . . 9
β’ π = βͺ
π |
7 | 5, 6 | txuni 22966 |
. . . . . . . 8
β’ ((π
β Top β§ π β Top) β (π Γ π) = βͺ (π
Γt π)) |
8 | 7 | ad2antrr 725 |
. . . . . . 7
β’ ((((π
β Top β§ π β Top) β§ (π β β
β§ π β β
)) β§ (π
Γt π) β Comp) β (π Γ π) = βͺ (π
Γt π)) |
9 | | foeq2 6757 |
. . . . . . 7
β’ ((π Γ π) = βͺ (π
Γt π) β ((1st
βΎ (π Γ π)):(π Γ π)βontoβπ β (1st βΎ (π Γ π)):βͺ (π
Γt π)βontoβπ)) |
10 | 8, 9 | syl 17 |
. . . . . 6
β’ ((((π
β Top β§ π β Top) β§ (π β β
β§ π β β
)) β§ (π
Γt π) β Comp) β
((1st βΎ (π
Γ π)):(π Γ π)βontoβπ β (1st βΎ (π Γ π)):βͺ (π
Γt π)βontoβπ)) |
11 | 4, 10 | mpbid 231 |
. . . . 5
β’ ((((π
β Top β§ π β Top) β§ (π β β
β§ π β β
)) β§ (π
Γt π) β Comp) β
(1st βΎ (π
Γ π)):βͺ (π
Γt π)βontoβπ) |
12 | 5 | toptopon 22289 |
. . . . . . 7
β’ (π
β Top β π
β (TopOnβπ)) |
13 | 6 | toptopon 22289 |
. . . . . . 7
β’ (π β Top β π β (TopOnβπ)) |
14 | | tx1cn 22983 |
. . . . . . 7
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (1st βΎ (π Γ π)) β ((π
Γt π) Cn π
)) |
15 | 12, 13, 14 | syl2anb 599 |
. . . . . 6
β’ ((π
β Top β§ π β Top) β
(1st βΎ (π
Γ π)) β ((π
Γt π) Cn π
)) |
16 | 15 | ad2antrr 725 |
. . . . 5
β’ ((((π
β Top β§ π β Top) β§ (π β β
β§ π β β
)) β§ (π
Γt π) β Comp) β
(1st βΎ (π
Γ π)) β ((π
Γt π) Cn π
)) |
17 | 5 | cncmp 22766 |
. . . . 5
β’ (((π
Γt π) β Comp β§
(1st βΎ (π
Γ π)):βͺ (π
Γt π)βontoβπ β§ (1st βΎ (π Γ π)) β ((π
Γt π) Cn π
)) β π
β Comp) |
18 | 1, 11, 16, 17 | syl3anc 1372 |
. . . 4
β’ ((((π
β Top β§ π β Top) β§ (π β β
β§ π β β
)) β§ (π
Γt π) β Comp) β π
β Comp) |
19 | | simplrl 776 |
. . . . . . 7
β’ ((((π
β Top β§ π β Top) β§ (π β β
β§ π β β
)) β§ (π
Γt π) β Comp) β π β β
) |
20 | | fo2ndres 7952 |
. . . . . . 7
β’ (π β β
β
(2nd βΎ (π
Γ π)):(π Γ π)βontoβπ) |
21 | 19, 20 | syl 17 |
. . . . . 6
β’ ((((π
β Top β§ π β Top) β§ (π β β
β§ π β β
)) β§ (π
Γt π) β Comp) β
(2nd βΎ (π
Γ π)):(π Γ π)βontoβπ) |
22 | | foeq2 6757 |
. . . . . . 7
β’ ((π Γ π) = βͺ (π
Γt π) β ((2nd
βΎ (π Γ π)):(π Γ π)βontoβπ β (2nd βΎ (π Γ π)):βͺ (π
Γt π)βontoβπ)) |
23 | 8, 22 | syl 17 |
. . . . . 6
β’ ((((π
β Top β§ π β Top) β§ (π β β
β§ π β β
)) β§ (π
Γt π) β Comp) β
((2nd βΎ (π
Γ π)):(π Γ π)βontoβπ β (2nd βΎ (π Γ π)):βͺ (π
Γt π)βontoβπ)) |
24 | 21, 23 | mpbid 231 |
. . . . 5
β’ ((((π
β Top β§ π β Top) β§ (π β β
β§ π β β
)) β§ (π
Γt π) β Comp) β
(2nd βΎ (π
Γ π)):βͺ (π
Γt π)βontoβπ) |
25 | | tx2cn 22984 |
. . . . . . 7
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (2nd βΎ (π Γ π)) β ((π
Γt π) Cn π)) |
26 | 12, 13, 25 | syl2anb 599 |
. . . . . 6
β’ ((π
β Top β§ π β Top) β
(2nd βΎ (π
Γ π)) β ((π
Γt π) Cn π)) |
27 | 26 | ad2antrr 725 |
. . . . 5
β’ ((((π
β Top β§ π β Top) β§ (π β β
β§ π β β
)) β§ (π
Γt π) β Comp) β
(2nd βΎ (π
Γ π)) β ((π
Γt π) Cn π)) |
28 | 6 | cncmp 22766 |
. . . . 5
β’ (((π
Γt π) β Comp β§
(2nd βΎ (π
Γ π)):βͺ (π
Γt π)βontoβπ β§ (2nd βΎ (π Γ π)) β ((π
Γt π) Cn π)) β π β Comp) |
29 | 1, 24, 27, 28 | syl3anc 1372 |
. . . 4
β’ ((((π
β Top β§ π β Top) β§ (π β β
β§ π β β
)) β§ (π
Γt π) β Comp) β π β Comp) |
30 | 18, 29 | jca 513 |
. . 3
β’ ((((π
β Top β§ π β Top) β§ (π β β
β§ π β β
)) β§ (π
Γt π) β Comp) β (π
β Comp β§ π β Comp)) |
31 | 30 | ex 414 |
. 2
β’ (((π
β Top β§ π β Top) β§ (π β β
β§ π β β
)) β ((π
Γt π) β Comp β (π
β Comp β§ π β Comp))) |
32 | | txcmp 23017 |
. 2
β’ ((π
β Comp β§ π β Comp) β (π
Γt π) β Comp) |
33 | 31, 32 | impbid1 224 |
1
β’ (((π
β Top β§ π β Top) β§ (π β β
β§ π β β
)) β ((π
Γt π) β Comp β (π
β Comp β§ π β Comp))) |