| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-fil |
|- Fil = ( z e. _V |-> { f e. ( fBas ` z ) | A. x e. ~P z ( ( f i^i ~P x ) =/= (/) -> x e. f ) } ) |
| 2 |
|
pweq |
|- ( z = X -> ~P z = ~P X ) |
| 3 |
2
|
adantr |
|- ( ( z = X /\ f = F ) -> ~P z = ~P X ) |
| 4 |
|
ineq1 |
|- ( f = F -> ( f i^i ~P x ) = ( F i^i ~P x ) ) |
| 5 |
4
|
neeq1d |
|- ( f = F -> ( ( f i^i ~P x ) =/= (/) <-> ( F i^i ~P x ) =/= (/) ) ) |
| 6 |
|
eleq2 |
|- ( f = F -> ( x e. f <-> x e. F ) ) |
| 7 |
5 6
|
imbi12d |
|- ( f = F -> ( ( ( f i^i ~P x ) =/= (/) -> x e. f ) <-> ( ( F i^i ~P x ) =/= (/) -> x e. F ) ) ) |
| 8 |
7
|
adantl |
|- ( ( z = X /\ f = F ) -> ( ( ( f i^i ~P x ) =/= (/) -> x e. f ) <-> ( ( F i^i ~P x ) =/= (/) -> x e. F ) ) ) |
| 9 |
3 8
|
raleqbidv |
|- ( ( z = X /\ f = F ) -> ( A. x e. ~P z ( ( f i^i ~P x ) =/= (/) -> x e. f ) <-> A. x e. ~P X ( ( F i^i ~P x ) =/= (/) -> x e. F ) ) ) |
| 10 |
|
fveq2 |
|- ( z = X -> ( fBas ` z ) = ( fBas ` X ) ) |
| 11 |
|
fvex |
|- ( fBas ` z ) e. _V |
| 12 |
|
elfvdm |
|- ( F e. ( fBas ` X ) -> X e. dom fBas ) |
| 13 |
1 9 10 11 12
|
elmptrab2 |
|- ( F e. ( Fil ` X ) <-> ( F e. ( fBas ` X ) /\ A. x e. ~P X ( ( F i^i ~P x ) =/= (/) -> x e. F ) ) ) |