Step | Hyp | Ref
| Expression |
1 | | f1stres 7950 |
. . 3
β’
(1st βΎ (π Γ π)):(π Γ π)βΆπ |
2 | 1 | a1i 11 |
. 2
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (1st βΎ (π Γ π)):(π Γ π)βΆπ) |
3 | | ffn 6673 |
. . . . . . . 8
β’
((1st βΎ (π Γ π)):(π Γ π)βΆπ β (1st βΎ (π Γ π)) Fn (π Γ π)) |
4 | | elpreima 7013 |
. . . . . . . 8
β’
((1st βΎ (π Γ π)) Fn (π Γ π) β (π§ β (β‘(1st βΎ (π Γ π)) β π€) β (π§ β (π Γ π) β§ ((1st βΎ (π Γ π))βπ§) β π€))) |
5 | 1, 3, 4 | mp2b 10 |
. . . . . . 7
β’ (π§ β (β‘(1st βΎ (π Γ π)) β π€) β (π§ β (π Γ π) β§ ((1st βΎ (π Γ π))βπ§) β π€)) |
6 | | fvres 6866 |
. . . . . . . . . 10
β’ (π§ β (π Γ π) β ((1st βΎ (π Γ π))βπ§) = (1st βπ§)) |
7 | 6 | eleq1d 2823 |
. . . . . . . . 9
β’ (π§ β (π Γ π) β (((1st βΎ (π Γ π))βπ§) β π€ β (1st βπ§) β π€)) |
8 | | 1st2nd2 7965 |
. . . . . . . . . 10
β’ (π§ β (π Γ π) β π§ = β¨(1st βπ§), (2nd βπ§)β©) |
9 | | xp2nd 7959 |
. . . . . . . . . 10
β’ (π§ β (π Γ π) β (2nd βπ§) β π) |
10 | | elxp6 7960 |
. . . . . . . . . . . 12
β’ (π§ β (π€ Γ π) β (π§ = β¨(1st βπ§), (2nd βπ§)β© β§ ((1st
βπ§) β π€ β§ (2nd
βπ§) β π))) |
11 | | anass 470 |
. . . . . . . . . . . 12
β’ (((π§ = β¨(1st
βπ§), (2nd
βπ§)β© β§
(1st βπ§)
β π€) β§
(2nd βπ§)
β π) β (π§ = β¨(1st
βπ§), (2nd
βπ§)β© β§
((1st βπ§)
β π€ β§
(2nd βπ§)
β π))) |
12 | | an32 645 |
. . . . . . . . . . . 12
β’ (((π§ = β¨(1st
βπ§), (2nd
βπ§)β© β§
(1st βπ§)
β π€) β§
(2nd βπ§)
β π) β ((π§ = β¨(1st
βπ§), (2nd
βπ§)β© β§
(2nd βπ§)
β π) β§
(1st βπ§)
β π€)) |
13 | 10, 11, 12 | 3bitr2i 299 |
. . . . . . . . . . 11
β’ (π§ β (π€ Γ π) β ((π§ = β¨(1st βπ§), (2nd βπ§)β© β§ (2nd
βπ§) β π) β§ (1st
βπ§) β π€)) |
14 | 13 | baib 537 |
. . . . . . . . . 10
β’ ((π§ = β¨(1st
βπ§), (2nd
βπ§)β© β§
(2nd βπ§)
β π) β (π§ β (π€ Γ π) β (1st βπ§) β π€)) |
15 | 8, 9, 14 | syl2anc 585 |
. . . . . . . . 9
β’ (π§ β (π Γ π) β (π§ β (π€ Γ π) β (1st βπ§) β π€)) |
16 | 7, 15 | bitr4d 282 |
. . . . . . . 8
β’ (π§ β (π Γ π) β (((1st βΎ (π Γ π))βπ§) β π€ β π§ β (π€ Γ π))) |
17 | 16 | pm5.32i 576 |
. . . . . . 7
β’ ((π§ β (π Γ π) β§ ((1st βΎ (π Γ π))βπ§) β π€) β (π§ β (π Γ π) β§ π§ β (π€ Γ π))) |
18 | 5, 17 | bitri 275 |
. . . . . 6
β’ (π§ β (β‘(1st βΎ (π Γ π)) β π€) β (π§ β (π Γ π) β§ π§ β (π€ Γ π))) |
19 | | toponss 22292 |
. . . . . . . . . 10
β’ ((π
β (TopOnβπ) β§ π€ β π
) β π€ β π) |
20 | 19 | adantlr 714 |
. . . . . . . . 9
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π
) β π€ β π) |
21 | | xpss1 5657 |
. . . . . . . . 9
β’ (π€ β π β (π€ Γ π) β (π Γ π)) |
22 | 20, 21 | syl 17 |
. . . . . . . 8
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π
) β (π€ Γ π) β (π Γ π)) |
23 | 22 | sseld 3948 |
. . . . . . 7
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π
) β (π§ β (π€ Γ π) β π§ β (π Γ π))) |
24 | 23 | pm4.71rd 564 |
. . . . . 6
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π
) β (π§ β (π€ Γ π) β (π§ β (π Γ π) β§ π§ β (π€ Γ π)))) |
25 | 18, 24 | bitr4id 290 |
. . . . 5
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π
) β (π§ β (β‘(1st βΎ (π Γ π)) β π€) β π§ β (π€ Γ π))) |
26 | 25 | eqrdv 2735 |
. . . 4
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π
) β (β‘(1st βΎ (π Γ π)) β π€) = (π€ Γ π)) |
27 | | toponmax 22291 |
. . . . . 6
β’ (π β (TopOnβπ) β π β π) |
28 | 27 | ad2antlr 726 |
. . . . 5
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π
) β π β π) |
29 | | txopn 22969 |
. . . . . 6
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π€ β π
β§ π β π)) β (π€ Γ π) β (π
Γt π)) |
30 | 29 | anassrs 469 |
. . . . 5
β’ ((((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π
) β§ π β π) β (π€ Γ π) β (π
Γt π)) |
31 | 28, 30 | mpdan 686 |
. . . 4
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π
) β (π€ Γ π) β (π
Γt π)) |
32 | 26, 31 | eqeltrd 2838 |
. . 3
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π
) β (β‘(1st βΎ (π Γ π)) β π€) β (π
Γt π)) |
33 | 32 | ralrimiva 3144 |
. 2
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β βπ€ β π
(β‘(1st βΎ (π Γ π)) β π€) β (π
Γt π)) |
34 | | txtopon 22958 |
. . 3
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (π
Γt π) β (TopOnβ(π Γ π))) |
35 | | simpl 484 |
. . 3
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β π
β (TopOnβπ)) |
36 | | iscn 22602 |
. . 3
β’ (((π
Γt π) β (TopOnβ(π Γ π)) β§ π
β (TopOnβπ)) β ((1st βΎ (π Γ π)) β ((π
Γt π) Cn π
) β ((1st βΎ (π Γ π)):(π Γ π)βΆπ β§ βπ€ β π
(β‘(1st βΎ (π Γ π)) β π€) β (π
Γt π)))) |
37 | 34, 35, 36 | syl2anc 585 |
. 2
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β ((1st βΎ (π Γ π)) β ((π
Γt π) Cn π
) β ((1st βΎ (π Γ π)):(π Γ π)βΆπ β§ βπ€ β π
(β‘(1st βΎ (π Γ π)) β π€) β (π
Γt π)))) |
38 | 2, 33, 37 | mpbir2and 712 |
1
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (1st βΎ (π Γ π)) β ((π
Γt π) Cn π
)) |