Metamath Proof Explorer

Theorem elfilss

Description: An element belongs to a filter iff any element below it does. (Contributed by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion elfilss 
|- ( ( F e. ( Fil ` X ) /\ A C_ X ) -> ( A e. F <-> E. t e. F t C_ A ) )

Proof

Step Hyp Ref Expression
1 ibar 
 |-  ( A C_ X -> ( E. t e. F t C_ A <-> ( A C_ X /\ E. t e. F t C_ A ) ) )
2 1 adantl 
 |-  ( ( F e. ( Fil ` X ) /\ A C_ X ) -> ( E. t e. F t C_ A <-> ( A C_ X /\ E. t e. F t C_ A ) ) )
3 filfbas 
 |-  ( F e. ( Fil ` X ) -> F e. ( fBas ` X ) )
4 elfg 
 |-  ( F e. ( fBas ` X ) -> ( A e. ( X filGen F ) <-> ( A C_ X /\ E. t e. F t C_ A ) ) )
5 3 4 syl 
 |-  ( F e. ( Fil ` X ) -> ( A e. ( X filGen F ) <-> ( A C_ X /\ E. t e. F t C_ A ) ) )
6 5 adantr 
 |-  ( ( F e. ( Fil ` X ) /\ A C_ X ) -> ( A e. ( X filGen F ) <-> ( A C_ X /\ E. t e. F t C_ A ) ) )
7 fgfil 
 |-  ( F e. ( Fil ` X ) -> ( X filGen F ) = F )
8 7 eleq2d 
 |-  ( F e. ( Fil ` X ) -> ( A e. ( X filGen F ) <-> A e. F ) )
9 8 adantr 
 |-  ( ( F e. ( Fil ` X ) /\ A C_ X ) -> ( A e. ( X filGen F ) <-> A e. F ) )
10 2 6 9 3bitr2rd 
 |-  ( ( F e. ( Fil ` X ) /\ A C_ X ) -> ( A e. F <-> E. t e. F t C_ A ) )