| 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
|
bitrid |
|- ( 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 ) ) ) |