Step |
Hyp |
Ref |
Expression |
1 |
|
fgval |
|- ( F e. ( fBas ` X ) -> ( X filGen F ) = { y e. ~P X | ( F i^i ~P y ) =/= (/) } ) |
2 |
1
|
eleq2d |
|- ( F e. ( fBas ` X ) -> ( A e. ( X filGen F ) <-> A e. { y e. ~P X | ( F i^i ~P y ) =/= (/) } ) ) |
3 |
|
pweq |
|- ( y = A -> ~P y = ~P A ) |
4 |
3
|
ineq2d |
|- ( y = A -> ( F i^i ~P y ) = ( F i^i ~P A ) ) |
5 |
4
|
neeq1d |
|- ( y = A -> ( ( F i^i ~P y ) =/= (/) <-> ( F i^i ~P A ) =/= (/) ) ) |
6 |
5
|
elrab |
|- ( A e. { y e. ~P X | ( F i^i ~P y ) =/= (/) } <-> ( A e. ~P X /\ ( F i^i ~P A ) =/= (/) ) ) |
7 |
|
elfvdm |
|- ( F e. ( fBas ` X ) -> X e. dom fBas ) |
8 |
|
elpw2g |
|- ( X e. dom fBas -> ( A e. ~P X <-> A C_ X ) ) |
9 |
7 8
|
syl |
|- ( F e. ( fBas ` X ) -> ( A e. ~P X <-> A C_ X ) ) |
10 |
|
elin |
|- ( x e. ( F i^i ~P A ) <-> ( x e. F /\ x e. ~P A ) ) |
11 |
|
velpw |
|- ( x e. ~P A <-> x C_ A ) |
12 |
11
|
anbi2i |
|- ( ( x e. F /\ x e. ~P A ) <-> ( x e. F /\ x C_ A ) ) |
13 |
10 12
|
bitri |
|- ( x e. ( F i^i ~P A ) <-> ( x e. F /\ x C_ A ) ) |
14 |
13
|
exbii |
|- ( E. x x e. ( F i^i ~P A ) <-> E. x ( x e. F /\ x C_ A ) ) |
15 |
|
n0 |
|- ( ( F i^i ~P A ) =/= (/) <-> E. x x e. ( F i^i ~P A ) ) |
16 |
|
df-rex |
|- ( E. x e. F x C_ A <-> E. x ( x e. F /\ x C_ A ) ) |
17 |
14 15 16
|
3bitr4i |
|- ( ( F i^i ~P A ) =/= (/) <-> E. x e. F x C_ A ) |
18 |
17
|
a1i |
|- ( F e. ( fBas ` X ) -> ( ( F i^i ~P A ) =/= (/) <-> E. x e. F x C_ A ) ) |
19 |
9 18
|
anbi12d |
|- ( F e. ( fBas ` X ) -> ( ( A e. ~P X /\ ( F i^i ~P A ) =/= (/) ) <-> ( A C_ X /\ E. x e. F x C_ A ) ) ) |
20 |
6 19
|
syl5bb |
|- ( F e. ( fBas ` X ) -> ( A e. { y e. ~P X | ( F i^i ~P y ) =/= (/) } <-> ( A C_ X /\ E. x e. F x C_ A ) ) ) |
21 |
2 20
|
bitrd |
|- ( F e. ( fBas ` X ) -> ( A e. ( X filGen F ) <-> ( A C_ X /\ E. x e. F x C_ A ) ) ) |