Step | Hyp | Ref
| Expression |
1 | | p0ex 5359 |
. . . . . 6
β’ {β
}
β V |
2 | 1 | prid2 4744 |
. . . . 5
β’ {β
}
β {β
, {β
}} |
3 | 2 | a1i 11 |
. . . 4
β’ (π = β
β {β
}
β {β
, {β
}}) |
4 | | ixpeq1 8868 |
. . . . . 6
β’ (π = β
β Xπ β
π ((π΄βπ)(,)(π΅βπ)) = Xπ β β
((π΄βπ)(,)(π΅βπ))) |
5 | | ixp0x 8886 |
. . . . . . 7
β’ Xπ β
β
((π΄βπ)(,)(π΅βπ)) = {β
} |
6 | 5 | a1i 11 |
. . . . . 6
β’ (π = β
β Xπ β
β
((π΄βπ)(,)(π΅βπ)) = {β
}) |
7 | 4, 6 | eqtrd 2771 |
. . . . 5
β’ (π = β
β Xπ β
π ((π΄βπ)(,)(π΅βπ)) = {β
}) |
8 | | 2fveq3 6867 |
. . . . . 6
β’ (π = β
β
(TopOpenβ(β^βπ)) =
(TopOpenβ(β^ββ
))) |
9 | | rrxtopn0b 44690 |
. . . . . . 7
β’
(TopOpenβ(β^ββ
)) = {β
,
{β
}} |
10 | 9 | a1i 11 |
. . . . . 6
β’ (π = β
β
(TopOpenβ(β^ββ
)) = {β
,
{β
}}) |
11 | 8, 10 | eqtrd 2771 |
. . . . 5
β’ (π = β
β
(TopOpenβ(β^βπ)) = {β
, {β
}}) |
12 | 7, 11 | eleq12d 2826 |
. . . 4
β’ (π = β
β (Xπ β
π ((π΄βπ)(,)(π΅βπ)) β
(TopOpenβ(β^βπ)) β {β
} β {β
,
{β
}})) |
13 | 3, 12 | mpbird 256 |
. . 3
β’ (π = β
β Xπ β
π ((π΄βπ)(,)(π΅βπ)) β
(TopOpenβ(β^βπ))) |
14 | 13 | adantl 482 |
. 2
β’ ((π β§ π = β
) β Xπ β
π ((π΄βπ)(,)(π΅βπ)) β
(TopOpenβ(β^βπ))) |
15 | | neqne 2947 |
. . . 4
β’ (Β¬
π = β
β π β β
) |
16 | 15 | adantl 482 |
. . 3
β’ ((π β§ Β¬ π = β
) β π β β
) |
17 | | fveq2 6862 |
. . . . . . . . . . 11
β’ (π = π β (π΄βπ) = (π΄βπ)) |
18 | | fveq2 6862 |
. . . . . . . . . . 11
β’ (π = π β (π΅βπ) = (π΅βπ)) |
19 | 17, 18 | oveq12d 7395 |
. . . . . . . . . 10
β’ (π = π β ((π΄βπ)(,)(π΅βπ)) = ((π΄βπ)(,)(π΅βπ))) |
20 | 19 | cbvixpv 8875 |
. . . . . . . . 9
β’ Xπ β
π ((π΄βπ)(,)(π΅βπ)) = Xπ β π ((π΄βπ)(,)(π΅βπ)) |
21 | 20 | eleq2i 2824 |
. . . . . . . 8
β’ (π β Xπ β
π ((π΄βπ)(,)(π΅βπ)) β π β Xπ β π ((π΄βπ)(,)(π΅βπ))) |
22 | 21 | biimpi 215 |
. . . . . . 7
β’ (π β Xπ β
π ((π΄βπ)(,)(π΅βπ)) β π β Xπ β π ((π΄βπ)(,)(π΅βπ))) |
23 | 22 | adantl 482 |
. . . . . 6
β’ (((π β§ π β β
) β§ π β Xπ β π ((π΄βπ)(,)(π΅βπ))) β π β Xπ β π ((π΄βπ)(,)(π΅βπ))) |
24 | | ioorrnopn.x |
. . . . . . . . 9
β’ (π β π β Fin) |
25 | 24 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ π β β
) β§ π β Xπ β π ((π΄βπ)(,)(π΅βπ))) β π β Fin) |
26 | 21, 25 | sylan2br 595 |
. . . . . . 7
β’ (((π β§ π β β
) β§ π β Xπ β π ((π΄βπ)(,)(π΅βπ))) β π β Fin) |
27 | | simplr 767 |
. . . . . . . 8
β’ (((π β§ π β β
) β§ π β Xπ β π ((π΄βπ)(,)(π΅βπ))) β π β β
) |
28 | 21, 27 | sylan2br 595 |
. . . . . . 7
β’ (((π β§ π β β
) β§ π β Xπ β π ((π΄βπ)(,)(π΅βπ))) β π β β
) |
29 | | ioorrnopn.a |
. . . . . . . . 9
β’ (π β π΄:πβΆβ) |
30 | 29 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ π β β
) β§ π β Xπ β π ((π΄βπ)(,)(π΅βπ))) β π΄:πβΆβ) |
31 | 21, 30 | sylan2br 595 |
. . . . . . 7
β’ (((π β§ π β β
) β§ π β Xπ β π ((π΄βπ)(,)(π΅βπ))) β π΄:πβΆβ) |
32 | | ioorrnopn.b |
. . . . . . . . 9
β’ (π β π΅:πβΆβ) |
33 | 32 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ π β β
) β§ π β Xπ β π ((π΄βπ)(,)(π΅βπ))) β π΅:πβΆβ) |
34 | 21, 33 | sylan2br 595 |
. . . . . . 7
β’ (((π β§ π β β
) β§ π β Xπ β π ((π΄βπ)(,)(π΅βπ))) β π΅:πβΆβ) |
35 | | simpr 485 |
. . . . . . . 8
β’ (((π β§ π β β
) β§ π β Xπ β π ((π΄βπ)(,)(π΅βπ))) β π β Xπ β π ((π΄βπ)(,)(π΅βπ))) |
36 | 21, 35 | sylan2br 595 |
. . . . . . 7
β’ (((π β§ π β β
) β§ π β Xπ β π ((π΄βπ)(,)(π΅βπ))) β π β Xπ β π ((π΄βπ)(,)(π΅βπ))) |
37 | | eqid 2731 |
. . . . . . 7
β’ ran
(π β π β¦ if(((π΅βπ) β (πβπ)) β€ ((πβπ) β (π΄βπ)), ((π΅βπ) β (πβπ)), ((πβπ) β (π΄βπ)))) = ran (π β π β¦ if(((π΅βπ) β (πβπ)) β€ ((πβπ) β (π΄βπ)), ((π΅βπ) β (πβπ)), ((πβπ) β (π΄βπ)))) |
38 | | fveq2 6862 |
. . . . . . . . . . . . 13
β’ (π = π β (π΅βπ) = (π΅βπ)) |
39 | | fveq2 6862 |
. . . . . . . . . . . . 13
β’ (π = π β (πβπ) = (πβπ)) |
40 | 38, 39 | oveq12d 7395 |
. . . . . . . . . . . 12
β’ (π = π β ((π΅βπ) β (πβπ)) = ((π΅βπ) β (πβπ))) |
41 | | fveq2 6862 |
. . . . . . . . . . . . 13
β’ (π = π β (π΄βπ) = (π΄βπ)) |
42 | 39, 41 | oveq12d 7395 |
. . . . . . . . . . . 12
β’ (π = π β ((πβπ) β (π΄βπ)) = ((πβπ) β (π΄βπ))) |
43 | 40, 42 | breq12d 5138 |
. . . . . . . . . . 11
β’ (π = π β (((π΅βπ) β (πβπ)) β€ ((πβπ) β (π΄βπ)) β ((π΅βπ) β (πβπ)) β€ ((πβπ) β (π΄βπ)))) |
44 | 43, 40, 42 | ifbieq12d 4534 |
. . . . . . . . . 10
β’ (π = π β if(((π΅βπ) β (πβπ)) β€ ((πβπ) β (π΄βπ)), ((π΅βπ) β (πβπ)), ((πβπ) β (π΄βπ))) = if(((π΅βπ) β (πβπ)) β€ ((πβπ) β (π΄βπ)), ((π΅βπ) β (πβπ)), ((πβπ) β (π΄βπ)))) |
45 | 44 | cbvmptv 5238 |
. . . . . . . . 9
β’ (π β π β¦ if(((π΅βπ) β (πβπ)) β€ ((πβπ) β (π΄βπ)), ((π΅βπ) β (πβπ)), ((πβπ) β (π΄βπ)))) = (π β π β¦ if(((π΅βπ) β (πβπ)) β€ ((πβπ) β (π΄βπ)), ((π΅βπ) β (πβπ)), ((πβπ) β (π΄βπ)))) |
46 | 45 | rneqi 5912 |
. . . . . . . 8
β’ ran
(π β π β¦ if(((π΅βπ) β (πβπ)) β€ ((πβπ) β (π΄βπ)), ((π΅βπ) β (πβπ)), ((πβπ) β (π΄βπ)))) = ran (π β π β¦ if(((π΅βπ) β (πβπ)) β€ ((πβπ) β (π΄βπ)), ((π΅βπ) β (πβπ)), ((πβπ) β (π΄βπ)))) |
47 | 46 | infeq1i 9438 |
. . . . . . 7
β’ inf(ran
(π β π β¦ if(((π΅βπ) β (πβπ)) β€ ((πβπ) β (π΄βπ)), ((π΅βπ) β (πβπ)), ((πβπ) β (π΄βπ)))), β, < ) = inf(ran (π β π β¦ if(((π΅βπ) β (πβπ)) β€ ((πβπ) β (π΄βπ)), ((π΅βπ) β (πβπ)), ((πβπ) β (π΄βπ)))), β, < ) |
48 | | eqid 2731 |
. . . . . . 7
β’ (π(ballβ(π β (β βm π), π β (β βm π) β¦
(ββΞ£π
β π (((πβπ) β (πβπ))β2))))inf(ran (π β π β¦ if(((π΅βπ) β (πβπ)) β€ ((πβπ) β (π΄βπ)), ((π΅βπ) β (πβπ)), ((πβπ) β (π΄βπ)))), β, < )) = (π(ballβ(π β (β βm π), π β (β βm π) β¦
(ββΞ£π
β π (((πβπ) β (πβπ))β2))))inf(ran (π β π β¦ if(((π΅βπ) β (πβπ)) β€ ((πβπ) β (π΄βπ)), ((π΅βπ) β (πβπ)), ((πβπ) β (π΄βπ)))), β, < )) |
49 | | fveq1 6861 |
. . . . . . . . . . . 12
β’ (π = π β (πβπ) = (πβπ)) |
50 | 49 | oveq1d 7392 |
. . . . . . . . . . 11
β’ (π = π β ((πβπ) β (πβπ)) = ((πβπ) β (πβπ))) |
51 | 50 | oveq1d 7392 |
. . . . . . . . . 10
β’ (π = π β (((πβπ) β (πβπ))β2) = (((πβπ) β (πβπ))β2)) |
52 | 51 | sumeq2sdv 15615 |
. . . . . . . . 9
β’ (π = π β Ξ£π β π (((πβπ) β (πβπ))β2) = Ξ£π β π (((πβπ) β (πβπ))β2)) |
53 | 52 | fveq2d 6866 |
. . . . . . . 8
β’ (π = π β (ββΞ£π β π (((πβπ) β (πβπ))β2)) = (ββΞ£π β π (((πβπ) β (πβπ))β2))) |
54 | | fveq1 6861 |
. . . . . . . . . . . 12
β’ (π = β β (πβπ) = (ββπ)) |
55 | 54 | oveq2d 7393 |
. . . . . . . . . . 11
β’ (π = β β ((πβπ) β (πβπ)) = ((πβπ) β (ββπ))) |
56 | 55 | oveq1d 7392 |
. . . . . . . . . 10
β’ (π = β β (((πβπ) β (πβπ))β2) = (((πβπ) β (ββπ))β2)) |
57 | 56 | sumeq2sdv 15615 |
. . . . . . . . 9
β’ (π = β β Ξ£π β π (((πβπ) β (πβπ))β2) = Ξ£π β π (((πβπ) β (ββπ))β2)) |
58 | 57 | fveq2d 6866 |
. . . . . . . 8
β’ (π = β β (ββΞ£π β π (((πβπ) β (πβπ))β2)) = (ββΞ£π β π (((πβπ) β (ββπ))β2))) |
59 | 53, 58 | cbvmpov 7472 |
. . . . . . 7
β’ (π β (β
βm π),
π β (β
βm π)
β¦ (ββΞ£π β π (((πβπ) β (πβπ))β2))) = (π β (β βm π), β β (β βm π) β¦
(ββΞ£π
β π (((πβπ) β (ββπ))β2))) |
60 | 26, 28, 31, 34, 36, 37, 47, 48, 59 | ioorrnopnlem 44698 |
. . . . . 6
β’ (((π β§ π β β
) β§ π β Xπ β π ((π΄βπ)(,)(π΅βπ))) β βπ£ β (TopOpenβ(β^βπ))(π β π£ β§ π£ β Xπ β π ((π΄βπ)(,)(π΅βπ)))) |
61 | 23, 60 | syldan 591 |
. . . . 5
β’ (((π β§ π β β
) β§ π β Xπ β π ((π΄βπ)(,)(π΅βπ))) β βπ£ β (TopOpenβ(β^βπ))(π β π£ β§ π£ β Xπ β π ((π΄βπ)(,)(π΅βπ)))) |
62 | 61 | ralrimiva 3145 |
. . . 4
β’ ((π β§ π β β
) β βπ β X
π β π ((π΄βπ)(,)(π΅βπ))βπ£ β (TopOpenβ(β^βπ))(π β π£ β§ π£ β Xπ β π ((π΄βπ)(,)(π΅βπ)))) |
63 | | eqid 2731 |
. . . . . . . 8
β’
(TopOpenβ(β^βπ)) = (TopOpenβ(β^βπ)) |
64 | 63 | rrxtop 44683 |
. . . . . . 7
β’ (π β Fin β
(TopOpenβ(β^βπ)) β Top) |
65 | 24, 64 | syl 17 |
. . . . . 6
β’ (π β
(TopOpenβ(β^βπ)) β Top) |
66 | 65 | adantr 481 |
. . . . 5
β’ ((π β§ π β β
) β
(TopOpenβ(β^βπ)) β Top) |
67 | | eltop2 22377 |
. . . . 5
β’
((TopOpenβ(β^βπ)) β Top β (Xπ β
π ((π΄βπ)(,)(π΅βπ)) β
(TopOpenβ(β^βπ)) β βπ β X π β π ((π΄βπ)(,)(π΅βπ))βπ£ β (TopOpenβ(β^βπ))(π β π£ β§ π£ β Xπ β π ((π΄βπ)(,)(π΅βπ))))) |
68 | 66, 67 | syl 17 |
. . . 4
β’ ((π β§ π β β
) β (Xπ β
π ((π΄βπ)(,)(π΅βπ)) β
(TopOpenβ(β^βπ)) β βπ β X π β π ((π΄βπ)(,)(π΅βπ))βπ£ β (TopOpenβ(β^βπ))(π β π£ β§ π£ β Xπ β π ((π΄βπ)(,)(π΅βπ))))) |
69 | 62, 68 | mpbird 256 |
. . 3
β’ ((π β§ π β β
) β Xπ β
π ((π΄βπ)(,)(π΅βπ)) β
(TopOpenβ(β^βπ))) |
70 | 16, 69 | syldan 591 |
. 2
β’ ((π β§ Β¬ π = β
) β Xπ β
π ((π΄βπ)(,)(π΅βπ)) β
(TopOpenβ(β^βπ))) |
71 | 14, 70 | pm2.61dan 811 |
1
β’ (π β Xπ β
π ((π΄βπ)(,)(π΅βπ)) β
(TopOpenβ(β^βπ))) |