Step | Hyp | Ref
| Expression |
1 | | iooex 9907 |
. . 3
β’ (,)
β V |
2 | 1 | imaex 4984 |
. 2
β’ ((,)
β (π Γ π)) β V |
3 | | qtopbas.1 |
. . . . . . . . 9
β’ π β
β* |
4 | 3 | sseli 3152 |
. . . . . . . 8
β’ (π§ β π β π§ β β*) |
5 | 3 | sseli 3152 |
. . . . . . . 8
β’ (π€ β π β π€ β β*) |
6 | 4, 5 | anim12i 338 |
. . . . . . 7
β’ ((π§ β π β§ π€ β π) β (π§ β β* β§ π€ β
β*)) |
7 | 3 | sseli 3152 |
. . . . . . . 8
β’ (π£ β π β π£ β β*) |
8 | 3 | sseli 3152 |
. . . . . . . 8
β’ (π’ β π β π’ β β*) |
9 | 7, 8 | anim12i 338 |
. . . . . . 7
β’ ((π£ β π β§ π’ β π) β (π£ β β* β§ π’ β
β*)) |
10 | | iooinsup 11285 |
. . . . . . 7
β’ (((π§ β β*
β§ π€ β
β*) β§ (π£ β β* β§ π’ β β*))
β ((π§(,)π€) β© (π£(,)π’)) = (sup({π§, π£}, β*, < )(,)inf({π€, π’}, β*, <
))) |
11 | 6, 9, 10 | syl2an 289 |
. . . . . 6
β’ (((π§ β π β§ π€ β π) β§ (π£ β π β§ π’ β π)) β ((π§(,)π€) β© (π£(,)π’)) = (sup({π§, π£}, β*, < )(,)inf({π€, π’}, β*, <
))) |
12 | | qtopbas.max |
. . . . . . . . . . 11
β’ ((π₯ β π β§ π¦ β π) β sup({π₯, π¦}, β*, < ) β π) |
13 | 12 | rgen2a 2531 |
. . . . . . . . . 10
β’
βπ₯ β
π βπ¦ β π sup({π₯, π¦}, β*, < ) β π |
14 | | preq12 3672 |
. . . . . . . . . . . . . 14
β’ ((π₯ = π£ β§ π¦ = π§) β {π₯, π¦} = {π£, π§}) |
15 | | prcom 3669 |
. . . . . . . . . . . . . 14
β’ {π£, π§} = {π§, π£} |
16 | 14, 15 | eqtrdi 2226 |
. . . . . . . . . . . . 13
β’ ((π₯ = π£ β§ π¦ = π§) β {π₯, π¦} = {π§, π£}) |
17 | 16 | supeq1d 6986 |
. . . . . . . . . . . 12
β’ ((π₯ = π£ β§ π¦ = π§) β sup({π₯, π¦}, β*, < ) = sup({π§, π£}, β*, <
)) |
18 | 17 | eleq1d 2246 |
. . . . . . . . . . 11
β’ ((π₯ = π£ β§ π¦ = π§) β (sup({π₯, π¦}, β*, < ) β π β sup({π§, π£}, β*, < ) β π)) |
19 | 18 | rspc2gv 2854 |
. . . . . . . . . 10
β’ ((π£ β π β§ π§ β π) β (βπ₯ β π βπ¦ β π sup({π₯, π¦}, β*, < ) β π β sup({π§, π£}, β*, < ) β π)) |
20 | 13, 19 | mpi 15 |
. . . . . . . . 9
β’ ((π£ β π β§ π§ β π) β sup({π§, π£}, β*, < ) β π) |
21 | 20 | ancoms 268 |
. . . . . . . 8
β’ ((π§ β π β§ π£ β π) β sup({π§, π£}, β*, < ) β π) |
22 | | qtopbas.min |
. . . . . . . . . 10
β’ ((π₯ β π β§ π¦ β π) β inf({π₯, π¦}, β*, < ) β π) |
23 | 22 | rgen2a 2531 |
. . . . . . . . 9
β’
βπ₯ β
π βπ¦ β π inf({π₯, π¦}, β*, < ) β π |
24 | | preq12 3672 |
. . . . . . . . . . . 12
β’ ((π₯ = π€ β§ π¦ = π’) β {π₯, π¦} = {π€, π’}) |
25 | 24 | infeq1d 7011 |
. . . . . . . . . . 11
β’ ((π₯ = π€ β§ π¦ = π’) β inf({π₯, π¦}, β*, < ) = inf({π€, π’}, β*, <
)) |
26 | 25 | eleq1d 2246 |
. . . . . . . . . 10
β’ ((π₯ = π€ β§ π¦ = π’) β (inf({π₯, π¦}, β*, < ) β π β inf({π€, π’}, β*, < ) β π)) |
27 | 26 | rspc2gv 2854 |
. . . . . . . . 9
β’ ((π€ β π β§ π’ β π) β (βπ₯ β π βπ¦ β π inf({π₯, π¦}, β*, < ) β π β inf({π€, π’}, β*, < ) β π)) |
28 | 23, 27 | mpi 15 |
. . . . . . . 8
β’ ((π€ β π β§ π’ β π) β inf({π€, π’}, β*, < ) β π) |
29 | | df-ov 5878 |
. . . . . . . . 9
β’
(sup({π§, π£}, β*, <
)(,)inf({π€, π’}, β*, < ))
= ((,)ββ¨sup({π§,
π£}, β*,
< ), inf({π€, π’}, β*, <
)β©) |
30 | | opelxpi 4659 |
. . . . . . . . . 10
β’
((sup({π§, π£}, β*, < )
β π β§ inf({π€, π’}, β*, < ) β π) β β¨sup({π§, π£}, β*, < ), inf({π€, π’}, β*, < )β© β
(π Γ π)) |
31 | | ioof 9971 |
. . . . . . . . . . . 12
β’
(,):(β* Γ β*)βΆπ«
β |
32 | | ffun 5369 |
. . . . . . . . . . . 12
β’
((,):(β* Γ β*)βΆπ«
β β Fun (,)) |
33 | 31, 32 | ax-mp 5 |
. . . . . . . . . . 11
β’ Fun
(,) |
34 | | xpss12 4734 |
. . . . . . . . . . . . 13
β’ ((π β β*
β§ π β
β*) β (π Γ π) β (β* Γ
β*)) |
35 | 3, 3, 34 | mp2an 426 |
. . . . . . . . . . . 12
β’ (π Γ π) β (β* Γ
β*) |
36 | 31 | fdmi 5374 |
. . . . . . . . . . . 12
β’ dom (,) =
(β* Γ β*) |
37 | 35, 36 | sseqtrri 3191 |
. . . . . . . . . . 11
β’ (π Γ π) β dom (,) |
38 | | funfvima2 5750 |
. . . . . . . . . . 11
β’ ((Fun (,)
β§ (π Γ π) β dom (,)) β
(β¨sup({π§, π£}, β*, < ),
inf({π€, π’}, β*, < )β© β
(π Γ π) β
((,)ββ¨sup({π§,
π£}, β*,
< ), inf({π€, π’}, β*, <
)β©) β ((,) β (π Γ π)))) |
39 | 33, 37, 38 | mp2an 426 |
. . . . . . . . . 10
β’
(β¨sup({π§, π£}, β*, < ),
inf({π€, π’}, β*, < )β© β
(π Γ π) β
((,)ββ¨sup({π§,
π£}, β*,
< ), inf({π€, π’}, β*, <
)β©) β ((,) β (π Γ π))) |
40 | 30, 39 | syl 14 |
. . . . . . . . 9
β’
((sup({π§, π£}, β*, < )
β π β§ inf({π€, π’}, β*, < ) β π) β
((,)ββ¨sup({π§,
π£}, β*,
< ), inf({π€, π’}, β*, <
)β©) β ((,) β (π Γ π))) |
41 | 29, 40 | eqeltrid 2264 |
. . . . . . . 8
β’
((sup({π§, π£}, β*, < )
β π β§ inf({π€, π’}, β*, < ) β π) β (sup({π§, π£}, β*, < )(,)inf({π€, π’}, β*, < )) β ((,)
β (π Γ π))) |
42 | 21, 28, 41 | syl2an 289 |
. . . . . . 7
β’ (((π§ β π β§ π£ β π) β§ (π€ β π β§ π’ β π)) β (sup({π§, π£}, β*, < )(,)inf({π€, π’}, β*, < )) β ((,)
β (π Γ π))) |
43 | 42 | an4s 588 |
. . . . . 6
β’ (((π§ β π β§ π€ β π) β§ (π£ β π β§ π’ β π)) β (sup({π§, π£}, β*, < )(,)inf({π€, π’}, β*, < )) β ((,)
β (π Γ π))) |
44 | 11, 43 | eqeltrd 2254 |
. . . . 5
β’ (((π§ β π β§ π€ β π) β§ (π£ β π β§ π’ β π)) β ((π§(,)π€) β© (π£(,)π’)) β ((,) β (π Γ π))) |
45 | 44 | ralrimivva 2559 |
. . . 4
β’ ((π§ β π β§ π€ β π) β βπ£ β π βπ’ β π ((π§(,)π€) β© (π£(,)π’)) β ((,) β (π Γ π))) |
46 | 45 | rgen2a 2531 |
. . 3
β’
βπ§ β
π βπ€ β π βπ£ β π βπ’ β π ((π§(,)π€) β© (π£(,)π’)) β ((,) β (π Γ π)) |
47 | | ffn 5366 |
. . . . . 6
β’
((,):(β* Γ β*)βΆπ«
β β (,) Fn (β* Γ
β*)) |
48 | 31, 47 | ax-mp 5 |
. . . . 5
β’ (,) Fn
(β* Γ β*) |
49 | | ineq1 3330 |
. . . . . . . 8
β’ (π₯ = ((,)βπ‘) β (π₯ β© π¦) = (((,)βπ‘) β© π¦)) |
50 | 49 | eleq1d 2246 |
. . . . . . 7
β’ (π₯ = ((,)βπ‘) β ((π₯ β© π¦) β ((,) β (π Γ π)) β (((,)βπ‘) β© π¦) β ((,) β (π Γ π)))) |
51 | 50 | ralbidv 2477 |
. . . . . 6
β’ (π₯ = ((,)βπ‘) β (βπ¦ β ((,) β (π Γ π))(π₯ β© π¦) β ((,) β (π Γ π)) β βπ¦ β ((,) β (π Γ π))(((,)βπ‘) β© π¦) β ((,) β (π Γ π)))) |
52 | 51 | ralima 5757 |
. . . . 5
β’ (((,) Fn
(β* Γ β*) β§ (π Γ π) β (β* Γ
β*)) β (βπ₯ β ((,) β (π Γ π))βπ¦ β ((,) β (π Γ π))(π₯ β© π¦) β ((,) β (π Γ π)) β βπ‘ β (π Γ π)βπ¦ β ((,) β (π Γ π))(((,)βπ‘) β© π¦) β ((,) β (π Γ π)))) |
53 | 48, 35, 52 | mp2an 426 |
. . . 4
β’
(βπ₯ β
((,) β (π Γ
π))βπ¦ β ((,) β (π Γ π))(π₯ β© π¦) β ((,) β (π Γ π)) β βπ‘ β (π Γ π)βπ¦ β ((,) β (π Γ π))(((,)βπ‘) β© π¦) β ((,) β (π Γ π))) |
54 | | fveq2 5516 |
. . . . . . . . . 10
β’ (π‘ = β¨π§, π€β© β ((,)βπ‘) = ((,)ββ¨π§, π€β©)) |
55 | | df-ov 5878 |
. . . . . . . . . 10
β’ (π§(,)π€) = ((,)ββ¨π§, π€β©) |
56 | 54, 55 | eqtr4di 2228 |
. . . . . . . . 9
β’ (π‘ = β¨π§, π€β© β ((,)βπ‘) = (π§(,)π€)) |
57 | 56 | ineq1d 3336 |
. . . . . . . 8
β’ (π‘ = β¨π§, π€β© β (((,)βπ‘) β© π¦) = ((π§(,)π€) β© π¦)) |
58 | 57 | eleq1d 2246 |
. . . . . . 7
β’ (π‘ = β¨π§, π€β© β ((((,)βπ‘) β© π¦) β ((,) β (π Γ π)) β ((π§(,)π€) β© π¦) β ((,) β (π Γ π)))) |
59 | 58 | ralbidv 2477 |
. . . . . 6
β’ (π‘ = β¨π§, π€β© β (βπ¦ β ((,) β (π Γ π))(((,)βπ‘) β© π¦) β ((,) β (π Γ π)) β βπ¦ β ((,) β (π Γ π))((π§(,)π€) β© π¦) β ((,) β (π Γ π)))) |
60 | | ineq2 3331 |
. . . . . . . . . 10
β’ (π¦ = ((,)βπ‘) β ((π§(,)π€) β© π¦) = ((π§(,)π€) β© ((,)βπ‘))) |
61 | 60 | eleq1d 2246 |
. . . . . . . . 9
β’ (π¦ = ((,)βπ‘) β (((π§(,)π€) β© π¦) β ((,) β (π Γ π)) β ((π§(,)π€) β© ((,)βπ‘)) β ((,) β (π Γ π)))) |
62 | 61 | ralima 5757 |
. . . . . . . 8
β’ (((,) Fn
(β* Γ β*) β§ (π Γ π) β (β* Γ
β*)) β (βπ¦ β ((,) β (π Γ π))((π§(,)π€) β© π¦) β ((,) β (π Γ π)) β βπ‘ β (π Γ π)((π§(,)π€) β© ((,)βπ‘)) β ((,) β (π Γ π)))) |
63 | 48, 35, 62 | mp2an 426 |
. . . . . . 7
β’
(βπ¦ β
((,) β (π Γ
π))((π§(,)π€) β© π¦) β ((,) β (π Γ π)) β βπ‘ β (π Γ π)((π§(,)π€) β© ((,)βπ‘)) β ((,) β (π Γ π))) |
64 | | fveq2 5516 |
. . . . . . . . . . 11
β’ (π‘ = β¨π£, π’β© β ((,)βπ‘) = ((,)ββ¨π£, π’β©)) |
65 | | df-ov 5878 |
. . . . . . . . . . 11
β’ (π£(,)π’) = ((,)ββ¨π£, π’β©) |
66 | 64, 65 | eqtr4di 2228 |
. . . . . . . . . 10
β’ (π‘ = β¨π£, π’β© β ((,)βπ‘) = (π£(,)π’)) |
67 | 66 | ineq2d 3337 |
. . . . . . . . 9
β’ (π‘ = β¨π£, π’β© β ((π§(,)π€) β© ((,)βπ‘)) = ((π§(,)π€) β© (π£(,)π’))) |
68 | 67 | eleq1d 2246 |
. . . . . . . 8
β’ (π‘ = β¨π£, π’β© β (((π§(,)π€) β© ((,)βπ‘)) β ((,) β (π Γ π)) β ((π§(,)π€) β© (π£(,)π’)) β ((,) β (π Γ π)))) |
69 | 68 | ralxp 4771 |
. . . . . . 7
β’
(βπ‘ β
(π Γ π)((π§(,)π€) β© ((,)βπ‘)) β ((,) β (π Γ π)) β βπ£ β π βπ’ β π ((π§(,)π€) β© (π£(,)π’)) β ((,) β (π Γ π))) |
70 | 63, 69 | bitri 184 |
. . . . . 6
β’
(βπ¦ β
((,) β (π Γ
π))((π§(,)π€) β© π¦) β ((,) β (π Γ π)) β βπ£ β π βπ’ β π ((π§(,)π€) β© (π£(,)π’)) β ((,) β (π Γ π))) |
71 | 59, 70 | bitrdi 196 |
. . . . 5
β’ (π‘ = β¨π§, π€β© β (βπ¦ β ((,) β (π Γ π))(((,)βπ‘) β© π¦) β ((,) β (π Γ π)) β βπ£ β π βπ’ β π ((π§(,)π€) β© (π£(,)π’)) β ((,) β (π Γ π)))) |
72 | 71 | ralxp 4771 |
. . . 4
β’
(βπ‘ β
(π Γ π)βπ¦ β ((,) β (π Γ π))(((,)βπ‘) β© π¦) β ((,) β (π Γ π)) β βπ§ β π βπ€ β π βπ£ β π βπ’ β π ((π§(,)π€) β© (π£(,)π’)) β ((,) β (π Γ π))) |
73 | 53, 72 | bitri 184 |
. . 3
β’
(βπ₯ β
((,) β (π Γ
π))βπ¦ β ((,) β (π Γ π))(π₯ β© π¦) β ((,) β (π Γ π)) β βπ§ β π βπ€ β π βπ£ β π βπ’ β π ((π§(,)π€) β© (π£(,)π’)) β ((,) β (π Γ π))) |
74 | 46, 73 | mpbir 146 |
. 2
β’
βπ₯ β
((,) β (π Γ
π))βπ¦ β ((,) β (π Γ π))(π₯ β© π¦) β ((,) β (π Γ π)) |
75 | | fiinbas 13552 |
. 2
β’ ((((,)
β (π Γ π)) β V β§ βπ₯ β ((,) β (π Γ π))βπ¦ β ((,) β (π Γ π))(π₯ β© π¦) β ((,) β (π Γ π))) β ((,) β (π Γ π)) β TopBases) |
76 | 2, 74, 75 | mp2an 426 |
1
β’ ((,)
β (π Γ π)) β
TopBases |