Step | Hyp | Ref
| Expression |
1 | | f2ndres 7950 |
. . 3
β’
(2nd βΎ (π Γ π)):(π Γ π)βΆπ |
2 | 1 | a1i 11 |
. 2
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (2nd βΎ (π Γ π)):(π Γ π)βΆπ) |
3 | | ffn 6672 |
. . . . . . . 8
β’
((2nd βΎ (π Γ π)):(π Γ π)βΆπ β (2nd βΎ (π Γ π)) Fn (π Γ π)) |
4 | | elpreima 7012 |
. . . . . . . 8
β’
((2nd βΎ (π Γ π)) Fn (π Γ π) β (π§ β (β‘(2nd βΎ (π Γ π)) β π€) β (π§ β (π Γ π) β§ ((2nd βΎ (π Γ π))βπ§) β π€))) |
5 | 1, 3, 4 | mp2b 10 |
. . . . . . 7
β’ (π§ β (β‘(2nd βΎ (π Γ π)) β π€) β (π§ β (π Γ π) β§ ((2nd βΎ (π Γ π))βπ§) β π€)) |
6 | | fvres 6865 |
. . . . . . . . . 10
β’ (π§ β (π Γ π) β ((2nd βΎ (π Γ π))βπ§) = (2nd βπ§)) |
7 | 6 | eleq1d 2819 |
. . . . . . . . 9
β’ (π§ β (π Γ π) β (((2nd βΎ (π Γ π))βπ§) β π€ β (2nd βπ§) β π€)) |
8 | | 1st2nd2 7964 |
. . . . . . . . . 10
β’ (π§ β (π Γ π) β π§ = β¨(1st βπ§), (2nd βπ§)β©) |
9 | | xp1st 7957 |
. . . . . . . . . 10
β’ (π§ β (π Γ π) β (1st βπ§) β π) |
10 | | elxp6 7959 |
. . . . . . . . . . . 12
β’ (π§ β (π Γ π€) β (π§ = β¨(1st βπ§), (2nd βπ§)β© β§ ((1st
βπ§) β π β§ (2nd
βπ§) β π€))) |
11 | | anass 470 |
. . . . . . . . . . . 12
β’ (((π§ = β¨(1st
βπ§), (2nd
βπ§)β© β§
(1st βπ§)
β π) β§
(2nd βπ§)
β π€) β (π§ = β¨(1st
βπ§), (2nd
βπ§)β© β§
((1st βπ§)
β π β§
(2nd βπ§)
β π€))) |
12 | 10, 11 | bitr4i 278 |
. . . . . . . . . . 11
β’ (π§ β (π Γ π€) β ((π§ = β¨(1st βπ§), (2nd βπ§)β© β§ (1st
βπ§) β π) β§ (2nd
βπ§) β π€)) |
13 | 12 | baib 537 |
. . . . . . . . . 10
β’ ((π§ = β¨(1st
βπ§), (2nd
βπ§)β© β§
(1st βπ§)
β π) β (π§ β (π Γ π€) β (2nd βπ§) β π€)) |
14 | 8, 9, 13 | syl2anc 585 |
. . . . . . . . 9
β’ (π§ β (π Γ π) β (π§ β (π Γ π€) β (2nd βπ§) β π€)) |
15 | 7, 14 | bitr4d 282 |
. . . . . . . 8
β’ (π§ β (π Γ π) β (((2nd βΎ (π Γ π))βπ§) β π€ β π§ β (π Γ π€))) |
16 | 15 | pm5.32i 576 |
. . . . . . 7
β’ ((π§ β (π Γ π) β§ ((2nd βΎ (π Γ π))βπ§) β π€) β (π§ β (π Γ π) β§ π§ β (π Γ π€))) |
17 | 5, 16 | bitri 275 |
. . . . . 6
β’ (π§ β (β‘(2nd βΎ (π Γ π)) β π€) β (π§ β (π Γ π) β§ π§ β (π Γ π€))) |
18 | | toponss 22299 |
. . . . . . . . . 10
β’ ((π β (TopOnβπ) β§ π€ β π) β π€ β π) |
19 | 18 | adantll 713 |
. . . . . . . . 9
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π) β π€ β π) |
20 | | xpss2 5657 |
. . . . . . . . 9
β’ (π€ β π β (π Γ π€) β (π Γ π)) |
21 | 19, 20 | syl 17 |
. . . . . . . 8
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π) β (π Γ π€) β (π Γ π)) |
22 | 21 | sseld 3947 |
. . . . . . 7
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π) β (π§ β (π Γ π€) β π§ β (π Γ π))) |
23 | 22 | pm4.71rd 564 |
. . . . . 6
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π) β (π§ β (π Γ π€) β (π§ β (π Γ π) β§ π§ β (π Γ π€)))) |
24 | 17, 23 | bitr4id 290 |
. . . . 5
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π) β (π§ β (β‘(2nd βΎ (π Γ π)) β π€) β π§ β (π Γ π€))) |
25 | 24 | eqrdv 2731 |
. . . 4
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π) β (β‘(2nd βΎ (π Γ π)) β π€) = (π Γ π€)) |
26 | | toponmax 22298 |
. . . . . 6
β’ (π
β (TopOnβπ) β π β π
) |
27 | | txopn 22976 |
. . . . . . 7
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π
β§ π€ β π)) β (π Γ π€) β (π
Γt π)) |
28 | 27 | expr 458 |
. . . . . 6
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π β π
) β (π€ β π β (π Γ π€) β (π
Γt π))) |
29 | 26, 28 | mpidan 688 |
. . . . 5
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (π€ β π β (π Γ π€) β (π
Γt π))) |
30 | 29 | imp 408 |
. . . 4
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π) β (π Γ π€) β (π
Γt π)) |
31 | 25, 30 | eqeltrd 2834 |
. . 3
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π) β (β‘(2nd βΎ (π Γ π)) β π€) β (π
Γt π)) |
32 | 31 | ralrimiva 3140 |
. 2
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β βπ€ β π (β‘(2nd βΎ (π Γ π)) β π€) β (π
Γt π)) |
33 | | txtopon 22965 |
. . 3
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (π
Γt π) β (TopOnβ(π Γ π))) |
34 | | iscn 22609 |
. . 3
β’ (((π
Γt π) β (TopOnβ(π Γ π)) β§ π β (TopOnβπ)) β ((2nd βΎ (π Γ π)) β ((π
Γt π) Cn π) β ((2nd βΎ (π Γ π)):(π Γ π)βΆπ β§ βπ€ β π (β‘(2nd βΎ (π Γ π)) β π€) β (π
Γt π)))) |
35 | 33, 34 | sylancom 589 |
. 2
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β ((2nd βΎ (π Γ π)) β ((π
Γt π) Cn π) β ((2nd βΎ (π Γ π)):(π Γ π)βΆπ β§ βπ€ β π (β‘(2nd βΎ (π Γ π)) β π€) β (π
Γt π)))) |
36 | 2, 32, 35 | mpbir2and 712 |
1
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (2nd βΎ (π Γ π)) β ((π
Γt π) Cn π)) |