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 ) )