Step | Hyp | Ref
| Expression |
1 | | f2ndres 7999 |
. . 3
β’
(2nd βΎ (π Γ π)):(π Γ π)βΆπ |
2 | 1 | a1i 11 |
. 2
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (2nd βΎ (π Γ π)):(π Γ π)βΆπ) |
3 | | ffn 6717 |
. . . . . . . 8
β’
((2nd βΎ (π Γ π)):(π Γ π)βΆπ β (2nd βΎ (π Γ π)) Fn (π Γ π)) |
4 | | elpreima 7059 |
. . . . . . . 8
β’
((2nd βΎ (π Γ π)) Fn (π Γ π) β (π§ β (β‘(2nd βΎ (π Γ π)) β π€) β (π§ β (π Γ π) β§ ((2nd βΎ (π Γ π))βπ§) β π€))) |
5 | 1, 3, 4 | mp2b 10 |
. . . . . . 7
β’ (π§ β (β‘(2nd βΎ (π Γ π)) β π€) β (π§ β (π Γ π) β§ ((2nd βΎ (π Γ π))βπ§) β π€)) |
6 | | fvres 6910 |
. . . . . . . . . 10
β’ (π§ β (π Γ π) β ((2nd βΎ (π Γ π))βπ§) = (2nd βπ§)) |
7 | 6 | eleq1d 2818 |
. . . . . . . . 9
β’ (π§ β (π Γ π) β (((2nd βΎ (π Γ π))βπ§) β π€ β (2nd βπ§) β π€)) |
8 | | 1st2nd2 8013 |
. . . . . . . . . 10
β’ (π§ β (π Γ π) β π§ = β¨(1st βπ§), (2nd βπ§)β©) |
9 | | xp1st 8006 |
. . . . . . . . . 10
β’ (π§ β (π Γ π) β (1st βπ§) β π) |
10 | | elxp6 8008 |
. . . . . . . . . . . 12
β’ (π§ β (π Γ π€) β (π§ = β¨(1st βπ§), (2nd βπ§)β© β§ ((1st
βπ§) β π β§ (2nd
βπ§) β π€))) |
11 | | anass 469 |
. . . . . . . . . . . 12
β’ (((π§ = β¨(1st
βπ§), (2nd
βπ§)β© β§
(1st βπ§)
β π) β§
(2nd βπ§)
β π€) β (π§ = β¨(1st
βπ§), (2nd
βπ§)β© β§
((1st βπ§)
β π β§
(2nd βπ§)
β π€))) |
12 | 10, 11 | bitr4i 277 |
. . . . . . . . . . 11
β’ (π§ β (π Γ π€) β ((π§ = β¨(1st βπ§), (2nd βπ§)β© β§ (1st
βπ§) β π) β§ (2nd
βπ§) β π€)) |
13 | 12 | baib 536 |
. . . . . . . . . 10
β’ ((π§ = β¨(1st
βπ§), (2nd
βπ§)β© β§
(1st βπ§)
β π) β (π§ β (π Γ π€) β (2nd βπ§) β π€)) |
14 | 8, 9, 13 | syl2anc 584 |
. . . . . . . . 9
β’ (π§ β (π Γ π) β (π§ β (π Γ π€) β (2nd βπ§) β π€)) |
15 | 7, 14 | bitr4d 281 |
. . . . . . . 8
β’ (π§ β (π Γ π) β (((2nd βΎ (π Γ π))βπ§) β π€ β π§ β (π Γ π€))) |
16 | 15 | pm5.32i 575 |
. . . . . . 7
β’ ((π§ β (π Γ π) β§ ((2nd βΎ (π Γ π))βπ§) β π€) β (π§ β (π Γ π) β§ π§ β (π Γ π€))) |
17 | 5, 16 | bitri 274 |
. . . . . 6
β’ (π§ β (β‘(2nd βΎ (π Γ π)) β π€) β (π§ β (π Γ π) β§ π§ β (π Γ π€))) |
18 | | toponss 22428 |
. . . . . . . . . 10
β’ ((π β (TopOnβπ) β§ π€ β π) β π€ β π) |
19 | 18 | adantll 712 |
. . . . . . . . 9
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π) β π€ β π) |
20 | | xpss2 5696 |
. . . . . . . . 9
β’ (π€ β π β (π Γ π€) β (π Γ π)) |
21 | 19, 20 | syl 17 |
. . . . . . . 8
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π) β (π Γ π€) β (π Γ π)) |
22 | 21 | sseld 3981 |
. . . . . . 7
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π) β (π§ β (π Γ π€) β π§ β (π Γ π))) |
23 | 22 | pm4.71rd 563 |
. . . . . 6
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π) β (π§ β (π Γ π€) β (π§ β (π Γ π) β§ π§ β (π Γ π€)))) |
24 | 17, 23 | bitr4id 289 |
. . . . 5
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π) β (π§ β (β‘(2nd βΎ (π Γ π)) β π€) β π§ β (π Γ π€))) |
25 | 24 | eqrdv 2730 |
. . . 4
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π) β (β‘(2nd βΎ (π Γ π)) β π€) = (π Γ π€)) |
26 | | toponmax 22427 |
. . . . . 6
β’ (π
β (TopOnβπ) β π β π
) |
27 | | txopn 23105 |
. . . . . . 7
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π β π
β§ π€ β π)) β (π Γ π€) β (π
Γt π)) |
28 | 27 | expr 457 |
. . . . . 6
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π β π
) β (π€ β π β (π Γ π€) β (π
Γt π))) |
29 | 26, 28 | mpidan 687 |
. . . . 5
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (π€ β π β (π Γ π€) β (π
Γt π))) |
30 | 29 | imp 407 |
. . . 4
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π) β (π Γ π€) β (π
Γt π)) |
31 | 25, 30 | eqeltrd 2833 |
. . 3
β’ (((π
β (TopOnβπ) β§ π β (TopOnβπ)) β§ π€ β π) β (β‘(2nd βΎ (π Γ π)) β π€) β (π
Γt π)) |
32 | 31 | ralrimiva 3146 |
. 2
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β βπ€ β π (β‘(2nd βΎ (π Γ π)) β π€) β (π
Γt π)) |
33 | | txtopon 23094 |
. . 3
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (π
Γt π) β (TopOnβ(π Γ π))) |
34 | | iscn 22738 |
. . 3
β’ (((π
Γt π) β (TopOnβ(π Γ π)) β§ π β (TopOnβπ)) β ((2nd βΎ (π Γ π)) β ((π
Γt π) Cn π) β ((2nd βΎ (π Γ π)):(π Γ π)βΆπ β§ βπ€ β π (β‘(2nd βΎ (π Γ π)) β π€) β (π
Γt π)))) |
35 | 33, 34 | sylancom 588 |
. 2
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β ((2nd βΎ (π Γ π)) β ((π
Γt π) Cn π) β ((2nd βΎ (π Γ π)):(π Γ π)βΆπ β§ βπ€ β π (β‘(2nd βΎ (π Γ π)) β π€) β (π
Γt π)))) |
36 | 2, 32, 35 | mpbir2and 711 |
1
β’ ((π
β (TopOnβπ) β§ π β (TopOnβπ)) β (2nd βΎ (π Γ π)) β ((π
Γt π) Cn π)) |