Metamath Proof Explorer

Theorem trfil3

Description: Conditions for the trace of a filter L to be a filter. (Contributed by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion trfil3 
|- ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> ( ( L |`t A ) e. ( Fil ` A ) <-> -. ( Y \ A ) e. L ) )

Proof

Step Hyp Ref Expression
1 trfil2 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> ( ( L |`t A ) e. ( Fil ` A ) <-> A. v e. L ( v i^i A ) =/= (/) ) )
2 dfral2 
 |-  ( A. v e. L ( v i^i A ) =/= (/) <-> -. E. v e. L -. ( v i^i A ) =/= (/) )
3 nne 
 |-  ( -. ( v i^i A ) =/= (/) <-> ( v i^i A ) = (/) )
4 filelss 
 |-  ( ( L e. ( Fil ` Y ) /\ v e. L ) -> v C_ Y )
5 reldisj 
 |-  ( v C_ Y -> ( ( v i^i A ) = (/) <-> v C_ ( Y \ A ) ) )
6 4 5 syl 
 |-  ( ( L e. ( Fil ` Y ) /\ v e. L ) -> ( ( v i^i A ) = (/) <-> v C_ ( Y \ A ) ) )
7 3 6 syl5bb 
 |-  ( ( L e. ( Fil ` Y ) /\ v e. L ) -> ( -. ( v i^i A ) =/= (/) <-> v C_ ( Y \ A ) ) )
8 7 rexbidva 
 |-  ( L e. ( Fil ` Y ) -> ( E. v e. L -. ( v i^i A ) =/= (/) <-> E. v e. L v C_ ( Y \ A ) ) )
9 8 adantr 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> ( E. v e. L -. ( v i^i A ) =/= (/) <-> E. v e. L v C_ ( Y \ A ) ) )
10 difssd 
 |-  ( A C_ Y -> ( Y \ A ) C_ Y )
11 elfilss 
 |-  ( ( L e. ( Fil ` Y ) /\ ( Y \ A ) C_ Y ) -> ( ( Y \ A ) e. L <-> E. v e. L v C_ ( Y \ A ) ) )
12 10 11 sylan2 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> ( ( Y \ A ) e. L <-> E. v e. L v C_ ( Y \ A ) ) )
13 9 12 bitr4d 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> ( E. v e. L -. ( v i^i A ) =/= (/) <-> ( Y \ A ) e. L ) )
14 13 notbid 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> ( -. E. v e. L -. ( v i^i A ) =/= (/) <-> -. ( Y \ A ) e. L ) )
15 2 14 syl5bb 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> ( A. v e. L ( v i^i A ) =/= (/) <-> -. ( Y \ A ) e. L ) )
16 1 15 bitrd 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> ( ( L |`t A ) e. ( Fil ` A ) <-> -. ( Y \ A ) e. L ) )