This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem trfil1

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

Ref Expression
Assertion trfil1 
|- ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> A = U. ( L |`t A ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> A C_ Y )
2 sseqin2 
 |-  ( A C_ Y <-> ( Y i^i A ) = A )
3 1 2 sylib 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> ( Y i^i A ) = A )
4 simpl 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> L e. ( Fil ` Y ) )
5 id 
 |-  ( A C_ Y -> A C_ Y )
6 filtop 
 |-  ( L e. ( Fil ` Y ) -> Y e. L )
7 ssexg 
 |-  ( ( A C_ Y /\ Y e. L ) -> A e. _V )
8 5 6 7 syl2anr 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> A e. _V )
9 6 adantr 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> Y e. L )
10 elrestr 
 |-  ( ( L e. ( Fil ` Y ) /\ A e. _V /\ Y e. L ) -> ( Y i^i A ) e. ( L |`t A ) )
11 4 8 9 10 syl3anc 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> ( Y i^i A ) e. ( L |`t A ) )
12 3 11 eqeltrrd 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> A e. ( L |`t A ) )
13 elssuni 
 |-  ( A e. ( L |`t A ) -> A C_ U. ( L |`t A ) )
14 12 13 syl 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> A C_ U. ( L |`t A ) )
15 restsspw 
 |-  ( L |`t A ) C_ ~P A
16 sspwuni 
 |-  ( ( L |`t A ) C_ ~P A <-> U. ( L |`t A ) C_ A )
17 15 16 mpbi 
 |-  U. ( L |`t A ) C_ A
18 17 a1i 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> U. ( L |`t A ) C_ A )
19 14 18 eqssd 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> A = U. ( L |`t A ) )