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 | | ioorrnopnxr.x |
. . . . . . . 8
β’ (π β π β Fin) |
25 | 24 | ad2antrr 724 |
. . . . . . 7
β’ (((π β§ π β β
) β§ π β Xπ β π ((π΄βπ)(,)(π΅βπ))) β π β Fin) |
26 | | ioorrnopnxr.a |
. . . . . . . 8
β’ (π β π΄:πβΆβ*) |
27 | 26 | ad2antrr 724 |
. . . . . . 7
β’ (((π β§ π β β
) β§ π β Xπ β π ((π΄βπ)(,)(π΅βπ))) β π΄:πβΆβ*) |
28 | | ioorrnopnxr.b |
. . . . . . . 8
β’ (π β π΅:πβΆβ*) |
29 | 28 | ad2antrr 724 |
. . . . . . 7
β’ (((π β§ π β β
) β§ π β Xπ β π ((π΄βπ)(,)(π΅βπ))) β π΅:πβΆβ*) |
30 | 21 | biimpri 227 |
. . . . . . . 8
β’ (π β Xπ β
π ((π΄βπ)(,)(π΅βπ)) β π β Xπ β π ((π΄βπ)(,)(π΅βπ))) |
31 | 30 | adantl 482 |
. . . . . . 7
β’ (((π β§ π β β
) β§ π β Xπ β π ((π΄βπ)(,)(π΅βπ))) β π β Xπ β π ((π΄βπ)(,)(π΅βπ))) |
32 | | fveq2 6862 |
. . . . . . . . . 10
β’ (π = π β (π΄βπ) = (π΄βπ)) |
33 | 32 | eqeq1d 2733 |
. . . . . . . . 9
β’ (π = π β ((π΄βπ) = -β β (π΄βπ) = -β)) |
34 | | fveq2 6862 |
. . . . . . . . . 10
β’ (π = π β (πβπ) = (πβπ)) |
35 | 34 | oveq1d 7392 |
. . . . . . . . 9
β’ (π = π β ((πβπ) β 1) = ((πβπ) β 1)) |
36 | 33, 35, 32 | ifbieq12d 4534 |
. . . . . . . 8
β’ (π = π β if((π΄βπ) = -β, ((πβπ) β 1), (π΄βπ)) = if((π΄βπ) = -β, ((πβπ) β 1), (π΄βπ))) |
37 | 36 | cbvmptv 5238 |
. . . . . . 7
β’ (π β π β¦ if((π΄βπ) = -β, ((πβπ) β 1), (π΄βπ))) = (π β π β¦ if((π΄βπ) = -β, ((πβπ) β 1), (π΄βπ))) |
38 | | fveq2 6862 |
. . . . . . . . . 10
β’ (π = π β (π΅βπ) = (π΅βπ)) |
39 | 38 | eqeq1d 2733 |
. . . . . . . . 9
β’ (π = π β ((π΅βπ) = +β β (π΅βπ) = +β)) |
40 | 34 | oveq1d 7392 |
. . . . . . . . 9
β’ (π = π β ((πβπ) + 1) = ((πβπ) + 1)) |
41 | 39, 40, 38 | ifbieq12d 4534 |
. . . . . . . 8
β’ (π = π β if((π΅βπ) = +β, ((πβπ) + 1), (π΅βπ)) = if((π΅βπ) = +β, ((πβπ) + 1), (π΅βπ))) |
42 | 41 | cbvmptv 5238 |
. . . . . . 7
β’ (π β π β¦ if((π΅βπ) = +β, ((πβπ) + 1), (π΅βπ))) = (π β π β¦ if((π΅βπ) = +β, ((πβπ) + 1), (π΅βπ))) |
43 | | eqid 2731 |
. . . . . . 7
β’ Xπ β
π (((π β π β¦ if((π΄βπ) = -β, ((πβπ) β 1), (π΄βπ)))βπ)(,)((π β π β¦ if((π΅βπ) = +β, ((πβπ) + 1), (π΅βπ)))βπ)) = Xπ β π (((π β π β¦ if((π΄βπ) = -β, ((πβπ) β 1), (π΄βπ)))βπ)(,)((π β π β¦ if((π΅βπ) = +β, ((πβπ) + 1), (π΅βπ)))βπ)) |
44 | 25, 27, 29, 31, 37, 42, 43 | ioorrnopnxrlem 44700 |
. . . . . 6
β’ (((π β§ π β β
) β§ π β Xπ β π ((π΄βπ)(,)(π΅βπ))) β βπ£ β (TopOpenβ(β^βπ))(π β π£ β§ π£ β Xπ β π ((π΄βπ)(,)(π΅βπ)))) |
45 | 23, 44 | syldan 591 |
. . . . 5
β’ (((π β§ π β β
) β§ π β Xπ β π ((π΄βπ)(,)(π΅βπ))) β βπ£ β (TopOpenβ(β^βπ))(π β π£ β§ π£ β Xπ β π ((π΄βπ)(,)(π΅βπ)))) |
46 | 45 | ralrimiva 3145 |
. . . 4
β’ ((π β§ π β β
) β βπ β X
π β π ((π΄βπ)(,)(π΅βπ))βπ£ β (TopOpenβ(β^βπ))(π β π£ β§ π£ β Xπ β π ((π΄βπ)(,)(π΅βπ)))) |
47 | | eqid 2731 |
. . . . . . . 8
β’
(TopOpenβ(β^βπ)) = (TopOpenβ(β^βπ)) |
48 | 47 | rrxtop 44683 |
. . . . . . 7
β’ (π β Fin β
(TopOpenβ(β^βπ)) β Top) |
49 | 24, 48 | syl 17 |
. . . . . 6
β’ (π β
(TopOpenβ(β^βπ)) β Top) |
50 | 49 | adantr 481 |
. . . . 5
β’ ((π β§ π β β
) β
(TopOpenβ(β^βπ)) β Top) |
51 | | eltop2 22377 |
. . . . 5
β’
((TopOpenβ(β^βπ)) β Top β (Xπ β
π ((π΄βπ)(,)(π΅βπ)) β
(TopOpenβ(β^βπ)) β βπ β X π β π ((π΄βπ)(,)(π΅βπ))βπ£ β (TopOpenβ(β^βπ))(π β π£ β§ π£ β Xπ β π ((π΄βπ)(,)(π΅βπ))))) |
52 | 50, 51 | syl 17 |
. . . 4
β’ ((π β§ π β β
) β (Xπ β
π ((π΄βπ)(,)(π΅βπ)) β
(TopOpenβ(β^βπ)) β βπ β X π β π ((π΄βπ)(,)(π΅βπ))βπ£ β (TopOpenβ(β^βπ))(π β π£ β§ π£ β Xπ β π ((π΄βπ)(,)(π΅βπ))))) |
53 | 46, 52 | mpbird 256 |
. . 3
β’ ((π β§ π β β
) β Xπ β
π ((π΄βπ)(,)(π΅βπ)) β
(TopOpenβ(β^βπ))) |
54 | 16, 53 | syldan 591 |
. 2
β’ ((π β§ Β¬ π = β
) β Xπ β
π ((π΄βπ)(,)(π΅βπ)) β
(TopOpenβ(β^βπ))) |
55 | 14, 54 | pm2.61dan 811 |
1
β’ (π β Xπ β
π ((π΄βπ)(,)(π΅βπ)) β
(TopOpenβ(β^βπ))) |