Step | Hyp | Ref
| Expression |
1 | | ioorrnopnxrlem.v |
. . . 4
β’ π = Xπ β π ((πΏβπ)(,)(π
βπ)) |
2 | 1 | a1i 11 |
. . 3
β’ (π β π = Xπ β π ((πΏβπ)(,)(π
βπ))) |
3 | | ioorrnopnxrlem.x |
. . . 4
β’ (π β π β Fin) |
4 | | iftrue 4498 |
. . . . . . . 8
β’ ((π΄βπ) = -β β if((π΄βπ) = -β, ((πΉβπ) β 1), (π΄βπ)) = ((πΉβπ) β 1)) |
5 | 4 | adantl 483 |
. . . . . . 7
β’ (((π β§ π β π) β§ (π΄βπ) = -β) β if((π΄βπ) = -β, ((πΉβπ) β 1), (π΄βπ)) = ((πΉβπ) β 1)) |
6 | | ioorrnopnxrlem.f |
. . . . . . . . . . . 12
β’ (π β πΉ β Xπ β π ((π΄βπ)(,)(π΅βπ))) |
7 | 6 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β πΉ β Xπ β π ((π΄βπ)(,)(π΅βπ))) |
8 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β π β π) |
9 | | fvixp2 43523 |
. . . . . . . . . . 11
β’ ((πΉ β Xπ β
π ((π΄βπ)(,)(π΅βπ)) β§ π β π) β (πΉβπ) β ((π΄βπ)(,)(π΅βπ))) |
10 | 7, 8, 9 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (πΉβπ) β ((π΄βπ)(,)(π΅βπ))) |
11 | 10 | elioored 43889 |
. . . . . . . . 9
β’ ((π β§ π β π) β (πΉβπ) β β) |
12 | | 1red 11166 |
. . . . . . . . 9
β’ ((π β§ π β π) β 1 β β) |
13 | 11, 12 | resubcld 11593 |
. . . . . . . 8
β’ ((π β§ π β π) β ((πΉβπ) β 1) β β) |
14 | 13 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β π) β§ (π΄βπ) = -β) β ((πΉβπ) β 1) β β) |
15 | 5, 14 | eqeltrd 2833 |
. . . . . 6
β’ (((π β§ π β π) β§ (π΄βπ) = -β) β if((π΄βπ) = -β, ((πΉβπ) β 1), (π΄βπ)) β β) |
16 | | iffalse 4501 |
. . . . . . . 8
β’ (Β¬
(π΄βπ) = -β β if((π΄βπ) = -β, ((πΉβπ) β 1), (π΄βπ)) = (π΄βπ)) |
17 | 16 | adantl 483 |
. . . . . . 7
β’ (((π β§ π β π) β§ Β¬ (π΄βπ) = -β) β if((π΄βπ) = -β, ((πΉβπ) β 1), (π΄βπ)) = (π΄βπ)) |
18 | | neqne 2948 |
. . . . . . . . 9
β’ (Β¬
(π΄βπ) = -β β (π΄βπ) β -β) |
19 | 18 | adantl 483 |
. . . . . . . 8
β’ (((π β§ π β π) β§ Β¬ (π΄βπ) = -β) β (π΄βπ) β -β) |
20 | | ioorrnopnxrlem.a |
. . . . . . . . . . 11
β’ (π β π΄:πβΆβ*) |
21 | 20 | ffvelcdmda 7041 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (π΄βπ) β
β*) |
22 | 21 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ (π΄βπ) β -β) β (π΄βπ) β
β*) |
23 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ (π΄βπ) β -β) β (π΄βπ) β -β) |
24 | | pnfxr 11219 |
. . . . . . . . . . . 12
β’ +β
β β* |
25 | 24 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β +β β
β*) |
26 | 11 | rexrd 11215 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (πΉβπ) β
β*) |
27 | | ioorrnopnxrlem.b |
. . . . . . . . . . . . . 14
β’ (π β π΅:πβΆβ*) |
28 | 27 | ffvelcdmda 7041 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β (π΅βπ) β
β*) |
29 | | ioogtlb 43835 |
. . . . . . . . . . . . 13
β’ (((π΄βπ) β β* β§ (π΅βπ) β β* β§ (πΉβπ) β ((π΄βπ)(,)(π΅βπ))) β (π΄βπ) < (πΉβπ)) |
30 | 21, 28, 10, 29 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (π΄βπ) < (πΉβπ)) |
31 | 11 | ltpnfd 13052 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (πΉβπ) < +β) |
32 | 21, 26, 25, 30, 31 | xrlttrd 13089 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (π΄βπ) < +β) |
33 | 21, 25, 32 | xrltned 43694 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (π΄βπ) β +β) |
34 | 33 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ (π΄βπ) β -β) β (π΄βπ) β +β) |
35 | 22, 23, 34 | xrred 43702 |
. . . . . . . 8
β’ (((π β§ π β π) β§ (π΄βπ) β -β) β (π΄βπ) β β) |
36 | 19, 35 | syldan 592 |
. . . . . . 7
β’ (((π β§ π β π) β§ Β¬ (π΄βπ) = -β) β (π΄βπ) β β) |
37 | 17, 36 | eqeltrd 2833 |
. . . . . 6
β’ (((π β§ π β π) β§ Β¬ (π΄βπ) = -β) β if((π΄βπ) = -β, ((πΉβπ) β 1), (π΄βπ)) β β) |
38 | 15, 37 | pm2.61dan 812 |
. . . . 5
β’ ((π β§ π β π) β if((π΄βπ) = -β, ((πΉβπ) β 1), (π΄βπ)) β β) |
39 | | ioorrnopnxrlem.l |
. . . . 5
β’ πΏ = (π β π β¦ if((π΄βπ) = -β, ((πΉβπ) β 1), (π΄βπ))) |
40 | 38, 39 | fmptd 7068 |
. . . 4
β’ (π β πΏ:πβΆβ) |
41 | | iftrue 4498 |
. . . . . . . 8
β’ ((π΅βπ) = +β β if((π΅βπ) = +β, ((πΉβπ) + 1), (π΅βπ)) = ((πΉβπ) + 1)) |
42 | 41 | adantl 483 |
. . . . . . 7
β’ (((π β§ π β π) β§ (π΅βπ) = +β) β if((π΅βπ) = +β, ((πΉβπ) + 1), (π΅βπ)) = ((πΉβπ) + 1)) |
43 | 11, 12 | readdcld 11194 |
. . . . . . . 8
β’ ((π β§ π β π) β ((πΉβπ) + 1) β β) |
44 | 43 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β π) β§ (π΅βπ) = +β) β ((πΉβπ) + 1) β β) |
45 | 42, 44 | eqeltrd 2833 |
. . . . . 6
β’ (((π β§ π β π) β§ (π΅βπ) = +β) β if((π΅βπ) = +β, ((πΉβπ) + 1), (π΅βπ)) β β) |
46 | | iffalse 4501 |
. . . . . . . 8
β’ (Β¬
(π΅βπ) = +β β if((π΅βπ) = +β, ((πΉβπ) + 1), (π΅βπ)) = (π΅βπ)) |
47 | 46 | adantl 483 |
. . . . . . 7
β’ (((π β§ π β π) β§ Β¬ (π΅βπ) = +β) β if((π΅βπ) = +β, ((πΉβπ) + 1), (π΅βπ)) = (π΅βπ)) |
48 | | neqne 2948 |
. . . . . . . . 9
β’ (Β¬
(π΅βπ) = +β β (π΅βπ) β +β) |
49 | 48 | adantl 483 |
. . . . . . . 8
β’ (((π β§ π β π) β§ Β¬ (π΅βπ) = +β) β (π΅βπ) β +β) |
50 | 28 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ (π΅βπ) β +β) β (π΅βπ) β
β*) |
51 | | mnfxr 11222 |
. . . . . . . . . . . 12
β’ -β
β β* |
52 | 51 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β -β β
β*) |
53 | 11 | mnfltd 13055 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β -β < (πΉβπ)) |
54 | | iooltub 43850 |
. . . . . . . . . . . . 13
β’ (((π΄βπ) β β* β§ (π΅βπ) β β* β§ (πΉβπ) β ((π΄βπ)(,)(π΅βπ))) β (πΉβπ) < (π΅βπ)) |
55 | 21, 28, 10, 54 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (πΉβπ) < (π΅βπ)) |
56 | 52, 26, 28, 53, 55 | xrlttrd 13089 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β -β < (π΅βπ)) |
57 | 52, 28, 56 | xrgtned 43659 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (π΅βπ) β -β) |
58 | 57 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ (π΅βπ) β +β) β (π΅βπ) β -β) |
59 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ (π΅βπ) β +β) β (π΅βπ) β +β) |
60 | 50, 58, 59 | xrred 43702 |
. . . . . . . 8
β’ (((π β§ π β π) β§ (π΅βπ) β +β) β (π΅βπ) β β) |
61 | 49, 60 | syldan 592 |
. . . . . . 7
β’ (((π β§ π β π) β§ Β¬ (π΅βπ) = +β) β (π΅βπ) β β) |
62 | 47, 61 | eqeltrd 2833 |
. . . . . 6
β’ (((π β§ π β π) β§ Β¬ (π΅βπ) = +β) β if((π΅βπ) = +β, ((πΉβπ) + 1), (π΅βπ)) β β) |
63 | 45, 62 | pm2.61dan 812 |
. . . . 5
β’ ((π β§ π β π) β if((π΅βπ) = +β, ((πΉβπ) + 1), (π΅βπ)) β β) |
64 | | ioorrnopnxrlem.r |
. . . . 5
β’ π
= (π β π β¦ if((π΅βπ) = +β, ((πΉβπ) + 1), (π΅βπ))) |
65 | 63, 64 | fmptd 7068 |
. . . 4
β’ (π β π
:πβΆβ) |
66 | 3, 40, 65 | ioorrnopn 44648 |
. . 3
β’ (π β Xπ β
π ((πΏβπ)(,)(π
βπ)) β
(TopOpenβ(β^βπ))) |
67 | 2, 66 | eqeltrd 2833 |
. 2
β’ (π β π β (TopOpenβ(β^βπ))) |
68 | 6 | elexd 3467 |
. . . . . 6
β’ (π β πΉ β V) |
69 | | ixpfn 8849 |
. . . . . . 7
β’ (πΉ β Xπ β
π ((π΄βπ)(,)(π΅βπ)) β πΉ Fn π) |
70 | 6, 69 | syl 17 |
. . . . . 6
β’ (π β πΉ Fn π) |
71 | 40 | ffvelcdmda 7041 |
. . . . . . . . 9
β’ ((π β§ π β π) β (πΏβπ) β β) |
72 | 71 | rexrd 11215 |
. . . . . . . 8
β’ ((π β§ π β π) β (πΏβπ) β
β*) |
73 | 65 | ffvelcdmda 7041 |
. . . . . . . . 9
β’ ((π β§ π β π) β (π
βπ) β β) |
74 | 73 | rexrd 11215 |
. . . . . . . 8
β’ ((π β§ π β π) β (π
βπ) β
β*) |
75 | 39 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β πΏ = (π β π β¦ if((π΄βπ) = -β, ((πΉβπ) β 1), (π΄βπ)))) |
76 | 38 | elexd 3467 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β if((π΄βπ) = -β, ((πΉβπ) β 1), (π΄βπ)) β V) |
77 | 75, 76 | fvmpt2d 6967 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (πΏβπ) = if((π΄βπ) = -β, ((πΉβπ) β 1), (π΄βπ))) |
78 | 77 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ (π΄βπ) = -β) β (πΏβπ) = if((π΄βπ) = -β, ((πΉβπ) β 1), (π΄βπ))) |
79 | 78, 5 | eqtrd 2772 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ (π΄βπ) = -β) β (πΏβπ) = ((πΉβπ) β 1)) |
80 | 11 | ltm1d 12097 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β ((πΉβπ) β 1) < (πΉβπ)) |
81 | 80 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ (π΄βπ) = -β) β ((πΉβπ) β 1) < (πΉβπ)) |
82 | 79, 81 | eqbrtrd 5133 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ (π΄βπ) = -β) β (πΏβπ) < (πΉβπ)) |
83 | 77 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ Β¬ (π΄βπ) = -β) β (πΏβπ) = if((π΄βπ) = -β, ((πΉβπ) β 1), (π΄βπ))) |
84 | 83, 17 | eqtrd 2772 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ Β¬ (π΄βπ) = -β) β (πΏβπ) = (π΄βπ)) |
85 | 30 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ Β¬ (π΄βπ) = -β) β (π΄βπ) < (πΉβπ)) |
86 | 84, 85 | eqbrtrd 5133 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ Β¬ (π΄βπ) = -β) β (πΏβπ) < (πΉβπ)) |
87 | 82, 86 | pm2.61dan 812 |
. . . . . . . 8
β’ ((π β§ π β π) β (πΏβπ) < (πΉβπ)) |
88 | 11 | ltp1d 12095 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (πΉβπ) < ((πΉβπ) + 1)) |
89 | 88 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ (π΅βπ) = +β) β (πΉβπ) < ((πΉβπ) + 1)) |
90 | 64 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β π
= (π β π β¦ if((π΅βπ) = +β, ((πΉβπ) + 1), (π΅βπ)))) |
91 | 63 | elexd 3467 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β if((π΅βπ) = +β, ((πΉβπ) + 1), (π΅βπ)) β V) |
92 | 90, 91 | fvmpt2d 6967 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β (π
βπ) = if((π΅βπ) = +β, ((πΉβπ) + 1), (π΅βπ))) |
93 | 92 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ (π΅βπ) = +β) β (π
βπ) = if((π΅βπ) = +β, ((πΉβπ) + 1), (π΅βπ))) |
94 | 93, 42 | eqtrd 2772 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ (π΅βπ) = +β) β (π
βπ) = ((πΉβπ) + 1)) |
95 | 94 | eqcomd 2738 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ (π΅βπ) = +β) β ((πΉβπ) + 1) = (π
βπ)) |
96 | 89, 95 | breqtrd 5137 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ (π΅βπ) = +β) β (πΉβπ) < (π
βπ)) |
97 | 55 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ Β¬ (π΅βπ) = +β) β (πΉβπ) < (π΅βπ)) |
98 | 92 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ Β¬ (π΅βπ) = +β) β (π
βπ) = if((π΅βπ) = +β, ((πΉβπ) + 1), (π΅βπ))) |
99 | 98, 47 | eqtrd 2772 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ Β¬ (π΅βπ) = +β) β (π
βπ) = (π΅βπ)) |
100 | 99 | eqcomd 2738 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ Β¬ (π΅βπ) = +β) β (π΅βπ) = (π
βπ)) |
101 | 97, 100 | breqtrd 5137 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ Β¬ (π΅βπ) = +β) β (πΉβπ) < (π
βπ)) |
102 | 96, 101 | pm2.61dan 812 |
. . . . . . . 8
β’ ((π β§ π β π) β (πΉβπ) < (π
βπ)) |
103 | 72, 74, 11, 87, 102 | eliood 43838 |
. . . . . . 7
β’ ((π β§ π β π) β (πΉβπ) β ((πΏβπ)(,)(π
βπ))) |
104 | 103 | ralrimiva 3140 |
. . . . . 6
β’ (π β βπ β π (πΉβπ) β ((πΏβπ)(,)(π
βπ))) |
105 | 68, 70, 104 | 3jca 1129 |
. . . . 5
β’ (π β (πΉ β V β§ πΉ Fn π β§ βπ β π (πΉβπ) β ((πΏβπ)(,)(π
βπ)))) |
106 | | elixp2 8847 |
. . . . 5
β’ (πΉ β Xπ β
π ((πΏβπ)(,)(π
βπ)) β (πΉ β V β§ πΉ Fn π β§ βπ β π (πΉβπ) β ((πΏβπ)(,)(π
βπ)))) |
107 | 105, 106 | sylibr 233 |
. . . 4
β’ (π β πΉ β Xπ β π ((πΏβπ)(,)(π
βπ))) |
108 | 107, 1 | eleqtrrdi 2844 |
. . 3
β’ (π β πΉ β π) |
109 | 21 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ (π΄βπ) = -β) β (π΄βπ) β
β*) |
110 | 72 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ (π΄βπ) = -β) β (πΏβπ) β
β*) |
111 | 15 | mnfltd 13055 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ (π΄βπ) = -β) β -β < if((π΄βπ) = -β, ((πΉβπ) β 1), (π΄βπ))) |
112 | 111, 5 | breqtrd 5137 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ (π΄βπ) = -β) β -β < ((πΉβπ) β 1)) |
113 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ (π΄βπ) = -β) β (π΄βπ) = -β) |
114 | 113, 79 | breq12d 5124 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ (π΄βπ) = -β) β ((π΄βπ) < (πΏβπ) β -β < ((πΉβπ) β 1))) |
115 | 112, 114 | mpbird 257 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ (π΄βπ) = -β) β (π΄βπ) < (πΏβπ)) |
116 | 109, 110,
115 | xrltled 13080 |
. . . . . . . 8
β’ (((π β§ π β π) β§ (π΄βπ) = -β) β (π΄βπ) β€ (πΏβπ)) |
117 | 84 | eqcomd 2738 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ Β¬ (π΄βπ) = -β) β (π΄βπ) = (πΏβπ)) |
118 | 36, 117 | eqled 11268 |
. . . . . . . 8
β’ (((π β§ π β π) β§ Β¬ (π΄βπ) = -β) β (π΄βπ) β€ (πΏβπ)) |
119 | 116, 118 | pm2.61dan 812 |
. . . . . . 7
β’ ((π β§ π β π) β (π΄βπ) β€ (πΏβπ)) |
120 | 74 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ (π΅βπ) = +β) β (π
βπ) β
β*) |
121 | 28 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ (π΅βπ) = +β) β (π΅βπ) β
β*) |
122 | 44 | ltpnfd 13052 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ (π΅βπ) = +β) β ((πΉβπ) + 1) < +β) |
123 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ (π΅βπ) = +β) β (π΅βπ) = +β) |
124 | 94, 123 | breq12d 5124 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ (π΅βπ) = +β) β ((π
βπ) < (π΅βπ) β ((πΉβπ) + 1) < +β)) |
125 | 122, 124 | mpbird 257 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ (π΅βπ) = +β) β (π
βπ) < (π΅βπ)) |
126 | 120, 121,
125 | xrltled 13080 |
. . . . . . . 8
β’ (((π β§ π β π) β§ (π΅βπ) = +β) β (π
βπ) β€ (π΅βπ)) |
127 | 73 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ Β¬ (π΅βπ) = +β) β (π
βπ) β β) |
128 | 127, 99 | eqled 11268 |
. . . . . . . 8
β’ (((π β§ π β π) β§ Β¬ (π΅βπ) = +β) β (π
βπ) β€ (π΅βπ)) |
129 | 126, 128 | pm2.61dan 812 |
. . . . . . 7
β’ ((π β§ π β π) β (π
βπ) β€ (π΅βπ)) |
130 | | ioossioo 13369 |
. . . . . . 7
β’ ((((π΄βπ) β β* β§ (π΅βπ) β β*) β§ ((π΄βπ) β€ (πΏβπ) β§ (π
βπ) β€ (π΅βπ))) β ((πΏβπ)(,)(π
βπ)) β ((π΄βπ)(,)(π΅βπ))) |
131 | 21, 28, 119, 129, 130 | syl22anc 838 |
. . . . . 6
β’ ((π β§ π β π) β ((πΏβπ)(,)(π
βπ)) β ((π΄βπ)(,)(π΅βπ))) |
132 | 131 | ralrimiva 3140 |
. . . . 5
β’ (π β βπ β π ((πΏβπ)(,)(π
βπ)) β ((π΄βπ)(,)(π΅βπ))) |
133 | | ss2ixp 8856 |
. . . . 5
β’
(βπ β
π ((πΏβπ)(,)(π
βπ)) β ((π΄βπ)(,)(π΅βπ)) β Xπ β π ((πΏβπ)(,)(π
βπ)) β Xπ β π ((π΄βπ)(,)(π΅βπ))) |
134 | 132, 133 | syl 17 |
. . . 4
β’ (π β Xπ β
π ((πΏβπ)(,)(π
βπ)) β Xπ β π ((π΄βπ)(,)(π΅βπ))) |
135 | 2, 134 | eqsstrd 3986 |
. . 3
β’ (π β π β Xπ β π ((π΄βπ)(,)(π΅βπ))) |
136 | 108, 135 | jca 513 |
. 2
β’ (π β (πΉ β π β§ π β Xπ β π ((π΄βπ)(,)(π΅βπ)))) |
137 | | eleq2 2822 |
. . . 4
β’ (π£ = π β (πΉ β π£ β πΉ β π)) |
138 | | sseq1 3973 |
. . . 4
β’ (π£ = π β (π£ β Xπ β π ((π΄βπ)(,)(π΅βπ)) β π β Xπ β π ((π΄βπ)(,)(π΅βπ)))) |
139 | 137, 138 | anbi12d 632 |
. . 3
β’ (π£ = π β ((πΉ β π£ β§ π£ β Xπ β π ((π΄βπ)(,)(π΅βπ))) β (πΉ β π β§ π β Xπ β π ((π΄βπ)(,)(π΅βπ))))) |
140 | 139 | rspcev 3583 |
. 2
β’ ((π β
(TopOpenβ(β^βπ)) β§ (πΉ β π β§ π β Xπ β π ((π΄βπ)(,)(π΅βπ)))) β βπ£ β (TopOpenβ(β^βπ))(πΉ β π£ β§ π£ β Xπ β π ((π΄βπ)(,)(π΅βπ)))) |
141 | 67, 136, 140 | syl2anc 585 |
1
β’ (π β βπ£ β (TopOpenβ(β^βπ))(πΉ β π£ β§ π£ β Xπ β π ((π΄βπ)(,)(π΅βπ)))) |