Step | Hyp | Ref
| Expression |
1 | | iooex 13347 |
. . 3
β’ (,)
β V |
2 | 1 | imaex 7907 |
. 2
β’ ((,)
β (π Γ π)) β V |
3 | | qtopbas.1 |
. . . . . . . . 9
β’ π β
β* |
4 | 3 | sseli 3979 |
. . . . . . . 8
β’ (π§ β π β π§ β β*) |
5 | 3 | sseli 3979 |
. . . . . . . 8
β’ (π€ β π β π€ β β*) |
6 | 4, 5 | anim12i 614 |
. . . . . . 7
β’ ((π§ β π β§ π€ β π) β (π§ β β* β§ π€ β
β*)) |
7 | 3 | sseli 3979 |
. . . . . . . 8
β’ (π£ β π β π£ β β*) |
8 | 3 | sseli 3979 |
. . . . . . . 8
β’ (π’ β π β π’ β β*) |
9 | 7, 8 | anim12i 614 |
. . . . . . 7
β’ ((π£ β π β§ π’ β π) β (π£ β β* β§ π’ β
β*)) |
10 | | iooin 13358 |
. . . . . . 7
β’ (((π§ β β*
β§ π€ β
β*) β§ (π£ β β* β§ π’ β β*))
β ((π§(,)π€) β© (π£(,)π’)) = (if(π§ β€ π£, π£, π§)(,)if(π€ β€ π’, π€, π’))) |
11 | 6, 9, 10 | syl2an 597 |
. . . . . 6
β’ (((π§ β π β§ π€ β π) β§ (π£ β π β§ π’ β π)) β ((π§(,)π€) β© (π£(,)π’)) = (if(π§ β€ π£, π£, π§)(,)if(π€ β€ π’, π€, π’))) |
12 | | ifcl 4574 |
. . . . . . . . 9
β’ ((π£ β π β§ π§ β π) β if(π§ β€ π£, π£, π§) β π) |
13 | 12 | ancoms 460 |
. . . . . . . 8
β’ ((π§ β π β§ π£ β π) β if(π§ β€ π£, π£, π§) β π) |
14 | | ifcl 4574 |
. . . . . . . 8
β’ ((π€ β π β§ π’ β π) β if(π€ β€ π’, π€, π’) β π) |
15 | | df-ov 7412 |
. . . . . . . . 9
β’ (if(π§ β€ π£, π£, π§)(,)if(π€ β€ π’, π€, π’)) = ((,)ββ¨if(π§ β€ π£, π£, π§), if(π€ β€ π’, π€, π’)β©) |
16 | | opelxpi 5714 |
. . . . . . . . . 10
β’
((if(π§ β€ π£, π£, π§) β π β§ if(π€ β€ π’, π€, π’) β π) β β¨if(π§ β€ π£, π£, π§), if(π€ β€ π’, π€, π’)β© β (π Γ π)) |
17 | | ioof 13424 |
. . . . . . . . . . . 12
β’
(,):(β* Γ β*)βΆπ«
β |
18 | | ffun 6721 |
. . . . . . . . . . . 12
β’
((,):(β* Γ β*)βΆπ«
β β Fun (,)) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . 11
β’ Fun
(,) |
20 | | xpss12 5692 |
. . . . . . . . . . . . 13
β’ ((π β β*
β§ π β
β*) β (π Γ π) β (β* Γ
β*)) |
21 | 3, 3, 20 | mp2an 691 |
. . . . . . . . . . . 12
β’ (π Γ π) β (β* Γ
β*) |
22 | 17 | fdmi 6730 |
. . . . . . . . . . . 12
β’ dom (,) =
(β* Γ β*) |
23 | 21, 22 | sseqtrri 4020 |
. . . . . . . . . . 11
β’ (π Γ π) β dom (,) |
24 | | funfvima2 7233 |
. . . . . . . . . . 11
β’ ((Fun (,)
β§ (π Γ π) β dom (,)) β
(β¨if(π§ β€ π£, π£, π§), if(π€ β€ π’, π€, π’)β© β (π Γ π) β ((,)ββ¨if(π§ β€ π£, π£, π§), if(π€ β€ π’, π€, π’)β©) β ((,) β (π Γ π)))) |
25 | 19, 23, 24 | mp2an 691 |
. . . . . . . . . 10
β’
(β¨if(π§ β€
π£, π£, π§), if(π€ β€ π’, π€, π’)β© β (π Γ π) β ((,)ββ¨if(π§ β€ π£, π£, π§), if(π€ β€ π’, π€, π’)β©) β ((,) β (π Γ π))) |
26 | 16, 25 | syl 17 |
. . . . . . . . 9
β’
((if(π§ β€ π£, π£, π§) β π β§ if(π€ β€ π’, π€, π’) β π) β ((,)ββ¨if(π§ β€ π£, π£, π§), if(π€ β€ π’, π€, π’)β©) β ((,) β (π Γ π))) |
27 | 15, 26 | eqeltrid 2838 |
. . . . . . . 8
β’
((if(π§ β€ π£, π£, π§) β π β§ if(π€ β€ π’, π€, π’) β π) β (if(π§ β€ π£, π£, π§)(,)if(π€ β€ π’, π€, π’)) β ((,) β (π Γ π))) |
28 | 13, 14, 27 | syl2an 597 |
. . . . . . 7
β’ (((π§ β π β§ π£ β π) β§ (π€ β π β§ π’ β π)) β (if(π§ β€ π£, π£, π§)(,)if(π€ β€ π’, π€, π’)) β ((,) β (π Γ π))) |
29 | 28 | an4s 659 |
. . . . . 6
β’ (((π§ β π β§ π€ β π) β§ (π£ β π β§ π’ β π)) β (if(π§ β€ π£, π£, π§)(,)if(π€ β€ π’, π€, π’)) β ((,) β (π Γ π))) |
30 | 11, 29 | eqeltrd 2834 |
. . . . 5
β’ (((π§ β π β§ π€ β π) β§ (π£ β π β§ π’ β π)) β ((π§(,)π€) β© (π£(,)π’)) β ((,) β (π Γ π))) |
31 | 30 | ralrimivva 3201 |
. . . 4
β’ ((π§ β π β§ π€ β π) β βπ£ β π βπ’ β π ((π§(,)π€) β© (π£(,)π’)) β ((,) β (π Γ π))) |
32 | 31 | rgen2 3198 |
. . 3
β’
βπ§ β
π βπ€ β π βπ£ β π βπ’ β π ((π§(,)π€) β© (π£(,)π’)) β ((,) β (π Γ π)) |
33 | | ffn 6718 |
. . . . . 6
β’
((,):(β* Γ β*)βΆπ«
β β (,) Fn (β* Γ
β*)) |
34 | 17, 33 | ax-mp 5 |
. . . . 5
β’ (,) Fn
(β* Γ β*) |
35 | | ineq1 4206 |
. . . . . . . 8
β’ (π₯ = ((,)βπ‘) β (π₯ β© π¦) = (((,)βπ‘) β© π¦)) |
36 | 35 | eleq1d 2819 |
. . . . . . 7
β’ (π₯ = ((,)βπ‘) β ((π₯ β© π¦) β ((,) β (π Γ π)) β (((,)βπ‘) β© π¦) β ((,) β (π Γ π)))) |
37 | 36 | ralbidv 3178 |
. . . . . 6
β’ (π₯ = ((,)βπ‘) β (βπ¦ β ((,) β (π Γ π))(π₯ β© π¦) β ((,) β (π Γ π)) β βπ¦ β ((,) β (π Γ π))(((,)βπ‘) β© π¦) β ((,) β (π Γ π)))) |
38 | 37 | ralima 7240 |
. . . . 5
β’ (((,) Fn
(β* Γ β*) β§ (π Γ π) β (β* Γ
β*)) β (βπ₯ β ((,) β (π Γ π))βπ¦ β ((,) β (π Γ π))(π₯ β© π¦) β ((,) β (π Γ π)) β βπ‘ β (π Γ π)βπ¦ β ((,) β (π Γ π))(((,)βπ‘) β© π¦) β ((,) β (π Γ π)))) |
39 | 34, 21, 38 | mp2an 691 |
. . . 4
β’
(βπ₯ β
((,) β (π Γ
π))βπ¦ β ((,) β (π Γ π))(π₯ β© π¦) β ((,) β (π Γ π)) β βπ‘ β (π Γ π)βπ¦ β ((,) β (π Γ π))(((,)βπ‘) β© π¦) β ((,) β (π Γ π))) |
40 | | fveq2 6892 |
. . . . . . . . . 10
β’ (π‘ = β¨π§, π€β© β ((,)βπ‘) = ((,)ββ¨π§, π€β©)) |
41 | | df-ov 7412 |
. . . . . . . . . 10
β’ (π§(,)π€) = ((,)ββ¨π§, π€β©) |
42 | 40, 41 | eqtr4di 2791 |
. . . . . . . . 9
β’ (π‘ = β¨π§, π€β© β ((,)βπ‘) = (π§(,)π€)) |
43 | 42 | ineq1d 4212 |
. . . . . . . 8
β’ (π‘ = β¨π§, π€β© β (((,)βπ‘) β© π¦) = ((π§(,)π€) β© π¦)) |
44 | 43 | eleq1d 2819 |
. . . . . . 7
β’ (π‘ = β¨π§, π€β© β ((((,)βπ‘) β© π¦) β ((,) β (π Γ π)) β ((π§(,)π€) β© π¦) β ((,) β (π Γ π)))) |
45 | 44 | ralbidv 3178 |
. . . . . 6
β’ (π‘ = β¨π§, π€β© β (βπ¦ β ((,) β (π Γ π))(((,)βπ‘) β© π¦) β ((,) β (π Γ π)) β βπ¦ β ((,) β (π Γ π))((π§(,)π€) β© π¦) β ((,) β (π Γ π)))) |
46 | | ineq2 4207 |
. . . . . . . . . 10
β’ (π¦ = ((,)βπ‘) β ((π§(,)π€) β© π¦) = ((π§(,)π€) β© ((,)βπ‘))) |
47 | 46 | eleq1d 2819 |
. . . . . . . . 9
β’ (π¦ = ((,)βπ‘) β (((π§(,)π€) β© π¦) β ((,) β (π Γ π)) β ((π§(,)π€) β© ((,)βπ‘)) β ((,) β (π Γ π)))) |
48 | 47 | ralima 7240 |
. . . . . . . 8
β’ (((,) Fn
(β* Γ β*) β§ (π Γ π) β (β* Γ
β*)) β (βπ¦ β ((,) β (π Γ π))((π§(,)π€) β© π¦) β ((,) β (π Γ π)) β βπ‘ β (π Γ π)((π§(,)π€) β© ((,)βπ‘)) β ((,) β (π Γ π)))) |
49 | 34, 21, 48 | mp2an 691 |
. . . . . . 7
β’
(βπ¦ β
((,) β (π Γ
π))((π§(,)π€) β© π¦) β ((,) β (π Γ π)) β βπ‘ β (π Γ π)((π§(,)π€) β© ((,)βπ‘)) β ((,) β (π Γ π))) |
50 | | fveq2 6892 |
. . . . . . . . . . 11
β’ (π‘ = β¨π£, π’β© β ((,)βπ‘) = ((,)ββ¨π£, π’β©)) |
51 | | df-ov 7412 |
. . . . . . . . . . 11
β’ (π£(,)π’) = ((,)ββ¨π£, π’β©) |
52 | 50, 51 | eqtr4di 2791 |
. . . . . . . . . 10
β’ (π‘ = β¨π£, π’β© β ((,)βπ‘) = (π£(,)π’)) |
53 | 52 | ineq2d 4213 |
. . . . . . . . 9
β’ (π‘ = β¨π£, π’β© β ((π§(,)π€) β© ((,)βπ‘)) = ((π§(,)π€) β© (π£(,)π’))) |
54 | 53 | eleq1d 2819 |
. . . . . . . 8
β’ (π‘ = β¨π£, π’β© β (((π§(,)π€) β© ((,)βπ‘)) β ((,) β (π Γ π)) β ((π§(,)π€) β© (π£(,)π’)) β ((,) β (π Γ π)))) |
55 | 54 | ralxp 5842 |
. . . . . . 7
β’
(βπ‘ β
(π Γ π)((π§(,)π€) β© ((,)βπ‘)) β ((,) β (π Γ π)) β βπ£ β π βπ’ β π ((π§(,)π€) β© (π£(,)π’)) β ((,) β (π Γ π))) |
56 | 49, 55 | bitri 275 |
. . . . . 6
β’
(βπ¦ β
((,) β (π Γ
π))((π§(,)π€) β© π¦) β ((,) β (π Γ π)) β βπ£ β π βπ’ β π ((π§(,)π€) β© (π£(,)π’)) β ((,) β (π Γ π))) |
57 | 45, 56 | bitrdi 287 |
. . . . 5
β’ (π‘ = β¨π§, π€β© β (βπ¦ β ((,) β (π Γ π))(((,)βπ‘) β© π¦) β ((,) β (π Γ π)) β βπ£ β π βπ’ β π ((π§(,)π€) β© (π£(,)π’)) β ((,) β (π Γ π)))) |
58 | 57 | ralxp 5842 |
. . . 4
β’
(βπ‘ β
(π Γ π)βπ¦ β ((,) β (π Γ π))(((,)βπ‘) β© π¦) β ((,) β (π Γ π)) β βπ§ β π βπ€ β π βπ£ β π βπ’ β π ((π§(,)π€) β© (π£(,)π’)) β ((,) β (π Γ π))) |
59 | 39, 58 | bitri 275 |
. . 3
β’
(βπ₯ β
((,) β (π Γ
π))βπ¦ β ((,) β (π Γ π))(π₯ β© π¦) β ((,) β (π Γ π)) β βπ§ β π βπ€ β π βπ£ β π βπ’ β π ((π§(,)π€) β© (π£(,)π’)) β ((,) β (π Γ π))) |
60 | 32, 59 | mpbir 230 |
. 2
β’
βπ₯ β
((,) β (π Γ
π))βπ¦ β ((,) β (π Γ π))(π₯ β© π¦) β ((,) β (π Γ π)) |
61 | | fiinbas 22455 |
. 2
β’ ((((,)
β (π Γ π)) β V β§ βπ₯ β ((,) β (π Γ π))βπ¦ β ((,) β (π Γ π))(π₯ β© π¦) β ((,) β (π Γ π))) β ((,) β (π Γ π)) β TopBases) |
62 | 2, 60, 61 | mp2an 691 |
1
β’ ((,)
β (π Γ π)) β
TopBases |