Step |
Hyp |
Ref |
Expression |
1 |
|
flimval.1 |
|- X = U. J |
2 |
1
|
topopn |
|- ( J e. Top -> X e. J ) |
3 |
2
|
adantr |
|- ( ( J e. Top /\ F e. U. ran Fil ) -> X e. J ) |
4 |
|
rabexg |
|- ( X e. J -> { x e. X | ( ( ( nei ` J ) ` { x } ) C_ F /\ F C_ ~P X ) } e. _V ) |
5 |
3 4
|
syl |
|- ( ( J e. Top /\ F e. U. ran Fil ) -> { x e. X | ( ( ( nei ` J ) ` { x } ) C_ F /\ F C_ ~P X ) } e. _V ) |
6 |
|
simpl |
|- ( ( j = J /\ f = F ) -> j = J ) |
7 |
6
|
unieqd |
|- ( ( j = J /\ f = F ) -> U. j = U. J ) |
8 |
7 1
|
eqtr4di |
|- ( ( j = J /\ f = F ) -> U. j = X ) |
9 |
6
|
fveq2d |
|- ( ( j = J /\ f = F ) -> ( nei ` j ) = ( nei ` J ) ) |
10 |
9
|
fveq1d |
|- ( ( j = J /\ f = F ) -> ( ( nei ` j ) ` { x } ) = ( ( nei ` J ) ` { x } ) ) |
11 |
|
simpr |
|- ( ( j = J /\ f = F ) -> f = F ) |
12 |
10 11
|
sseq12d |
|- ( ( j = J /\ f = F ) -> ( ( ( nei ` j ) ` { x } ) C_ f <-> ( ( nei ` J ) ` { x } ) C_ F ) ) |
13 |
8
|
pweqd |
|- ( ( j = J /\ f = F ) -> ~P U. j = ~P X ) |
14 |
11 13
|
sseq12d |
|- ( ( j = J /\ f = F ) -> ( f C_ ~P U. j <-> F C_ ~P X ) ) |
15 |
12 14
|
anbi12d |
|- ( ( j = J /\ f = F ) -> ( ( ( ( nei ` j ) ` { x } ) C_ f /\ f C_ ~P U. j ) <-> ( ( ( nei ` J ) ` { x } ) C_ F /\ F C_ ~P X ) ) ) |
16 |
8 15
|
rabeqbidv |
|- ( ( j = J /\ f = F ) -> { x e. U. j | ( ( ( nei ` j ) ` { x } ) C_ f /\ f C_ ~P U. j ) } = { x e. X | ( ( ( nei ` J ) ` { x } ) C_ F /\ F C_ ~P X ) } ) |
17 |
|
df-flim |
|- fLim = ( j e. Top , f e. U. ran Fil |-> { x e. U. j | ( ( ( nei ` j ) ` { x } ) C_ f /\ f C_ ~P U. j ) } ) |
18 |
16 17
|
ovmpoga |
|- ( ( J e. Top /\ F e. U. ran Fil /\ { x e. X | ( ( ( nei ` J ) ` { x } ) C_ F /\ F C_ ~P X ) } e. _V ) -> ( J fLim F ) = { x e. X | ( ( ( nei ` J ) ` { x } ) C_ F /\ F C_ ~P X ) } ) |
19 |
5 18
|
mpd3an3 |
|- ( ( J e. Top /\ F e. U. ran Fil ) -> ( J fLim F ) = { x e. X | ( ( ( nei ` J ) ` { x } ) C_ F /\ F C_ ~P X ) } ) |