Step |
Hyp |
Ref |
Expression |
1 |
|
isfil |
|- ( F e. ( Fil ` X ) <-> ( F e. ( fBas ` X ) /\ A. x e. ~P X ( ( F i^i ~P x ) =/= (/) -> x e. F ) ) ) |
2 |
1
|
simprbi |
|- ( F e. ( Fil ` X ) -> A. x e. ~P X ( ( F i^i ~P x ) =/= (/) -> x e. F ) ) |
3 |
2
|
adantr |
|- ( ( F e. ( Fil ` X ) /\ ( A e. F /\ B C_ X /\ A C_ B ) ) -> A. x e. ~P X ( ( F i^i ~P x ) =/= (/) -> x e. F ) ) |
4 |
|
elfvdm |
|- ( F e. ( Fil ` X ) -> X e. dom Fil ) |
5 |
|
simp2 |
|- ( ( A e. F /\ B C_ X /\ A C_ B ) -> B C_ X ) |
6 |
|
elpw2g |
|- ( X e. dom Fil -> ( B e. ~P X <-> B C_ X ) ) |
7 |
6
|
biimpar |
|- ( ( X e. dom Fil /\ B C_ X ) -> B e. ~P X ) |
8 |
4 5 7
|
syl2an |
|- ( ( F e. ( Fil ` X ) /\ ( A e. F /\ B C_ X /\ A C_ B ) ) -> B e. ~P X ) |
9 |
|
simpr1 |
|- ( ( F e. ( Fil ` X ) /\ ( A e. F /\ B C_ X /\ A C_ B ) ) -> A e. F ) |
10 |
|
simpr3 |
|- ( ( F e. ( Fil ` X ) /\ ( A e. F /\ B C_ X /\ A C_ B ) ) -> A C_ B ) |
11 |
9 10
|
elpwd |
|- ( ( F e. ( Fil ` X ) /\ ( A e. F /\ B C_ X /\ A C_ B ) ) -> A e. ~P B ) |
12 |
|
inelcm |
|- ( ( A e. F /\ A e. ~P B ) -> ( F i^i ~P B ) =/= (/) ) |
13 |
9 11 12
|
syl2anc |
|- ( ( F e. ( Fil ` X ) /\ ( A e. F /\ B C_ X /\ A C_ B ) ) -> ( F i^i ~P B ) =/= (/) ) |
14 |
|
pweq |
|- ( x = B -> ~P x = ~P B ) |
15 |
14
|
ineq2d |
|- ( x = B -> ( F i^i ~P x ) = ( F i^i ~P B ) ) |
16 |
15
|
neeq1d |
|- ( x = B -> ( ( F i^i ~P x ) =/= (/) <-> ( F i^i ~P B ) =/= (/) ) ) |
17 |
|
eleq1 |
|- ( x = B -> ( x e. F <-> B e. F ) ) |
18 |
16 17
|
imbi12d |
|- ( x = B -> ( ( ( F i^i ~P x ) =/= (/) -> x e. F ) <-> ( ( F i^i ~P B ) =/= (/) -> B e. F ) ) ) |
19 |
18
|
rspccv |
|- ( A. x e. ~P X ( ( F i^i ~P x ) =/= (/) -> x e. F ) -> ( B e. ~P X -> ( ( F i^i ~P B ) =/= (/) -> B e. F ) ) ) |
20 |
3 8 13 19
|
syl3c |
|- ( ( F e. ( Fil ` X ) /\ ( A e. F /\ B C_ X /\ A C_ B ) ) -> B e. F ) |