Step |
Hyp |
Ref |
Expression |
1 |
|
neifg.1 |
|- X = U. J |
2 |
1
|
opnfbas |
|- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> { x e. J | S C_ x } e. ( fBas ` X ) ) |
3 |
|
fgval |
|- ( { x e. J | S C_ x } e. ( fBas ` X ) -> ( X filGen { x e. J | S C_ x } ) = { t e. ~P X | ( { x e. J | S C_ x } i^i ~P t ) =/= (/) } ) |
4 |
2 3
|
syl |
|- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( X filGen { x e. J | S C_ x } ) = { t e. ~P X | ( { x e. J | S C_ x } i^i ~P t ) =/= (/) } ) |
5 |
|
pweq |
|- ( t = u -> ~P t = ~P u ) |
6 |
5
|
ineq2d |
|- ( t = u -> ( { x e. J | S C_ x } i^i ~P t ) = ( { x e. J | S C_ x } i^i ~P u ) ) |
7 |
6
|
neeq1d |
|- ( t = u -> ( ( { x e. J | S C_ x } i^i ~P t ) =/= (/) <-> ( { x e. J | S C_ x } i^i ~P u ) =/= (/) ) ) |
8 |
7
|
elrab |
|- ( u e. { t e. ~P X | ( { x e. J | S C_ x } i^i ~P t ) =/= (/) } <-> ( u e. ~P X /\ ( { x e. J | S C_ x } i^i ~P u ) =/= (/) ) ) |
9 |
|
velpw |
|- ( u e. ~P X <-> u C_ X ) |
10 |
9
|
a1i |
|- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( u e. ~P X <-> u C_ X ) ) |
11 |
|
n0 |
|- ( ( { x e. J | S C_ x } i^i ~P u ) =/= (/) <-> E. z z e. ( { x e. J | S C_ x } i^i ~P u ) ) |
12 |
|
elin |
|- ( z e. ( { x e. J | S C_ x } i^i ~P u ) <-> ( z e. { x e. J | S C_ x } /\ z e. ~P u ) ) |
13 |
|
sseq2 |
|- ( x = z -> ( S C_ x <-> S C_ z ) ) |
14 |
13
|
elrab |
|- ( z e. { x e. J | S C_ x } <-> ( z e. J /\ S C_ z ) ) |
15 |
|
velpw |
|- ( z e. ~P u <-> z C_ u ) |
16 |
14 15
|
anbi12i |
|- ( ( z e. { x e. J | S C_ x } /\ z e. ~P u ) <-> ( ( z e. J /\ S C_ z ) /\ z C_ u ) ) |
17 |
12 16
|
bitri |
|- ( z e. ( { x e. J | S C_ x } i^i ~P u ) <-> ( ( z e. J /\ S C_ z ) /\ z C_ u ) ) |
18 |
17
|
exbii |
|- ( E. z z e. ( { x e. J | S C_ x } i^i ~P u ) <-> E. z ( ( z e. J /\ S C_ z ) /\ z C_ u ) ) |
19 |
11 18
|
bitri |
|- ( ( { x e. J | S C_ x } i^i ~P u ) =/= (/) <-> E. z ( ( z e. J /\ S C_ z ) /\ z C_ u ) ) |
20 |
19
|
a1i |
|- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( ( { x e. J | S C_ x } i^i ~P u ) =/= (/) <-> E. z ( ( z e. J /\ S C_ z ) /\ z C_ u ) ) ) |
21 |
10 20
|
anbi12d |
|- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( ( u e. ~P X /\ ( { x e. J | S C_ x } i^i ~P u ) =/= (/) ) <-> ( u C_ X /\ E. z ( ( z e. J /\ S C_ z ) /\ z C_ u ) ) ) ) |
22 |
|
anass |
|- ( ( ( z e. J /\ S C_ z ) /\ z C_ u ) <-> ( z e. J /\ ( S C_ z /\ z C_ u ) ) ) |
23 |
22
|
exbii |
|- ( E. z ( ( z e. J /\ S C_ z ) /\ z C_ u ) <-> E. z ( z e. J /\ ( S C_ z /\ z C_ u ) ) ) |
24 |
|
df-rex |
|- ( E. z e. J ( S C_ z /\ z C_ u ) <-> E. z ( z e. J /\ ( S C_ z /\ z C_ u ) ) ) |
25 |
23 24
|
bitr4i |
|- ( E. z ( ( z e. J /\ S C_ z ) /\ z C_ u ) <-> E. z e. J ( S C_ z /\ z C_ u ) ) |
26 |
25
|
anbi2i |
|- ( ( u C_ X /\ E. z ( ( z e. J /\ S C_ z ) /\ z C_ u ) ) <-> ( u C_ X /\ E. z e. J ( S C_ z /\ z C_ u ) ) ) |
27 |
1
|
isnei |
|- ( ( J e. Top /\ S C_ X ) -> ( u e. ( ( nei ` J ) ` S ) <-> ( u C_ X /\ E. z e. J ( S C_ z /\ z C_ u ) ) ) ) |
28 |
27
|
3adant3 |
|- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( u e. ( ( nei ` J ) ` S ) <-> ( u C_ X /\ E. z e. J ( S C_ z /\ z C_ u ) ) ) ) |
29 |
26 28
|
bitr4id |
|- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( ( u C_ X /\ E. z ( ( z e. J /\ S C_ z ) /\ z C_ u ) ) <-> u e. ( ( nei ` J ) ` S ) ) ) |
30 |
21 29
|
bitrd |
|- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( ( u e. ~P X /\ ( { x e. J | S C_ x } i^i ~P u ) =/= (/) ) <-> u e. ( ( nei ` J ) ` S ) ) ) |
31 |
8 30
|
syl5bb |
|- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( u e. { t e. ~P X | ( { x e. J | S C_ x } i^i ~P t ) =/= (/) } <-> u e. ( ( nei ` J ) ` S ) ) ) |
32 |
31
|
eqrdv |
|- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> { t e. ~P X | ( { x e. J | S C_ x } i^i ~P t ) =/= (/) } = ( ( nei ` J ) ` S ) ) |
33 |
4 32
|
eqtrd |
|- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( X filGen { x e. J | S C_ x } ) = ( ( nei ` J ) ` S ) ) |