Step | Hyp | Ref
| Expression |
1 | | f1stres 6150 |
. . 3
β’
(1st βΎ (π Γ π)):(π Γ π)βΆπ |
2 | 1 | a1i 9 |
. 2
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (1st βΎ (π Γ π)):(π Γ π)βΆπ) |
3 | | ffn 5357 |
. . . . . . . 8
β’
((1st βΎ (π Γ π)):(π Γ π)βΆπ β (1st βΎ (π Γ π)) Fn (π Γ π)) |
4 | | elpreima 5627 |
. . . . . . . 8
β’
((1st βΎ (π Γ π)) Fn (π Γ π) β (π§ β (β‘(1st βΎ (π Γ π)) β π€) β (π§ β (π Γ π) β§ ((1st βΎ (π Γ π))βπ§) β π€))) |
5 | 1, 3, 4 | mp2b 8 |
. . . . . . 7
β’ (π§ β (β‘(1st βΎ (π Γ π)) β π€) β (π§ β (π Γ π) β§ ((1st βΎ (π Γ π))βπ§) β π€)) |
6 | | fvres 5531 |
. . . . . . . . . 10
β’ (π§ β (π Γ π) β ((1st βΎ (π Γ π))βπ§) = (1st βπ§)) |
7 | 6 | eleq1d 2244 |
. . . . . . . . 9
β’ (π§ β (π Γ π) β (((1st βΎ (π Γ π))βπ§) β π€ β (1st βπ§) β π€)) |
8 | | 1st2nd2 6166 |
. . . . . . . . . 10
β’ (π§ β (π Γ π) β π§ = β¨(1st βπ§), (2nd βπ§)β©) |
9 | | xp2nd 6157 |
. . . . . . . . . 10
β’ (π§ β (π Γ π) β (2nd βπ§) β π) |
10 | | elxp6 6160 |
. . . . . . . . . . . 12
β’ (π§ β (π€ Γ π) β (π§ = β¨(1st βπ§), (2nd βπ§)β© β§ ((1st
βπ§) β π€ β§ (2nd
βπ§) β π))) |
11 | | anass 401 |
. . . . . . . . . . . 12
β’ (((π§ = β¨(1st
βπ§), (2nd
βπ§)β© β§
(1st βπ§)
β π€) β§
(2nd βπ§)
β π) β (π§ = β¨(1st
βπ§), (2nd
βπ§)β© β§
((1st βπ§)
β π€ β§
(2nd βπ§)
β π))) |
12 | | an32 562 |
. . . . . . . . . . . 12
β’ (((π§ = β¨(1st
βπ§), (2nd
βπ§)β© β§
(1st βπ§)
β π€) β§
(2nd βπ§)
β π) β ((π§ = β¨(1st
βπ§), (2nd
βπ§)β© β§
(2nd βπ§)
β π) β§
(1st βπ§)
β π€)) |
13 | 10, 11, 12 | 3bitr2i 208 |
. . . . . . . . . . 11
β’ (π§ β (π€ Γ π) β ((π§ = β¨(1st βπ§), (2nd βπ§)β© β§ (2nd
βπ§) β π) β§ (1st
βπ§) β π€)) |
14 | 13 | baib 919 |
. . . . . . . . . 10
β’ ((π§ = β¨(1st
βπ§), (2nd
βπ§)β© β§
(2nd βπ§)
β π) β (π§ β (π€ Γ π) β (1st βπ§) β π€)) |
15 | 8, 9, 14 | syl2anc 411 |
. . . . . . . . 9
β’ (π§ β (π Γ π) β (π§ β (π€ Γ π) β (1st βπ§) β π€)) |
16 | 7, 15 | bitr4d 191 |
. . . . . . . 8
β’ (π§ β (π Γ π) β (((1st βΎ (π Γ π))βπ§) β π€ β π§ β (π€ Γ π))) |
17 | 16 | pm5.32i 454 |
. . . . . . 7
β’ ((π§ β (π Γ π) β§ ((1st βΎ (π Γ π))βπ§) β π€) β (π§ β (π Γ π) β§ π§ β (π€ Γ π))) |
18 | 5, 17 | bitri 184 |
. . . . . 6
β’ (π§ β (β‘(1st βΎ (π Γ π)) β π€) β (π§ β (π Γ π) β§ π§ β (π€ Γ π))) |
19 | | toponss 13017 |
. . . . . . . . . 10
β’ ((π
β (TopOnβπ) β§ π€ β π
) β π€ β π) |
20 | 19 | adantlr 477 |
. . . . . . . . 9
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π
) β π€ β π) |
21 | | xpss1 4730 |
. . . . . . . . 9
β’ (π€ β π β (π€ Γ π) β (π Γ π)) |
22 | 20, 21 | syl 14 |
. . . . . . . 8
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π
) β (π€ Γ π) β (π Γ π)) |
23 | 22 | sseld 3152 |
. . . . . . 7
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π
) β (π§ β (π€ Γ π) β π§ β (π Γ π))) |
24 | 23 | pm4.71rd 394 |
. . . . . 6
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π
) β (π§ β (π€ Γ π) β (π§ β (π Γ π) β§ π§ β (π€ Γ π)))) |
25 | 18, 24 | bitr4id 199 |
. . . . 5
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π
) β (π§ β (β‘(1st βΎ (π Γ π)) β π€) β π§ β (π€ Γ π))) |
26 | 25 | eqrdv 2173 |
. . . 4
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π
) β (β‘(1st βΎ (π Γ π)) β π€) = (π€ Γ π)) |
27 | | toponmax 13016 |
. . . . . 6
β’ (π β (TopOnβπ) β π β π) |
28 | 27 | ad2antlr 489 |
. . . . 5
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π
) β π β π) |
29 | | txopn 13258 |
. . . . . 6
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π€ β π
β§ π β π)) β (π€ Γ π) β (π
Γt π)) |
30 | 29 | anassrs 400 |
. . . . 5
β’ ((((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π
) β§ π β π) β (π€ Γ π) β (π
Γt π)) |
31 | 28, 30 | mpdan 421 |
. . . 4
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π
) β (π€ Γ π) β (π
Γt π)) |
32 | 26, 31 | eqeltrd 2252 |
. . 3
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π
) β (β‘(1st βΎ (π Γ π)) β π€) β (π
Γt π)) |
33 | 32 | ralrimiva 2548 |
. 2
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β βπ€ β π
(β‘(1st βΎ (π Γ π)) β π€) β (π
Γt π)) |
34 | | txtopon 13255 |
. . 3
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (π
Γt π) β (TopOnβ(π Γ π))) |
35 | | simpl 109 |
. . 3
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β π
β (TopOnβπ)) |
36 | | iscn 13190 |
. . 3
β’ (((π
Γt π) β (TopOnβ(π Γ π)) β§ π
β (TopOnβπ)) β ((1st βΎ (π Γ π)) β ((π
Γt π) Cn π
) β ((1st βΎ (π Γ π)):(π Γ π)βΆπ β§ βπ€ β π
(β‘(1st βΎ (π Γ π)) β π€) β (π
Γt π)))) |
37 | 34, 35, 36 | syl2anc 411 |
. 2
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β ((1st βΎ (π Γ π)) β ((π
Γt π) Cn π
) β ((1st βΎ (π Γ π)):(π Γ π)βΆπ β§ βπ€ β π
(β‘(1st βΎ (π Γ π)) β π€) β (π
Γt π)))) |
38 | 2, 33, 37 | mpbir2and 944 |
1
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (1st βΎ (π Γ π)) β ((π
Γt π) Cn π
)) |