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	⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝐴 = ∪ ( 𝐿 ↾t 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝐴 ⊆ 𝑌 )
2		sseqin2	⊢ ( 𝐴 ⊆ 𝑌 ↔ ( 𝑌 ∩ 𝐴 ) = 𝐴 )
3	1 2	sylib	⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( 𝑌 ∩ 𝐴 ) = 𝐴 )
4		simpl	⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝐿 ∈ ( Fil ‘ 𝑌 ) )
5		id	⊢ ( 𝐴 ⊆ 𝑌 → 𝐴 ⊆ 𝑌 )
6		filtop	⊢ ( 𝐿 ∈ ( Fil ‘ 𝑌 ) → 𝑌 ∈ 𝐿 )
7		ssexg	⊢ ( ( 𝐴 ⊆ 𝑌 ∧ 𝑌 ∈ 𝐿 ) → 𝐴 ∈ V )
8	5 6 7	syl2anr	⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝐴 ∈ V )
9	6	adantr	⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝑌 ∈ 𝐿 )
10		elrestr	⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ∈ V ∧ 𝑌 ∈ 𝐿 ) → ( 𝑌 ∩ 𝐴 ) ∈ ( 𝐿 ↾t 𝐴 ) )
11	4 8 9 10	syl3anc	⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( 𝑌 ∩ 𝐴 ) ∈ ( 𝐿 ↾t 𝐴 ) )
12	3 11	eqeltrrd	⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝐴 ∈ ( 𝐿 ↾t 𝐴 ) )
13		elssuni	⊢ ( 𝐴 ∈ ( 𝐿 ↾t 𝐴 ) → 𝐴 ⊆ ∪ ( 𝐿 ↾t 𝐴 ) )
14	12 13	syl	⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝐴 ⊆ ∪ ( 𝐿 ↾t 𝐴 ) )
15		restsspw	⊢ ( 𝐿 ↾t 𝐴 ) ⊆ 𝒫 𝐴
16		sspwuni	⊢ ( ( 𝐿 ↾t 𝐴 ) ⊆ 𝒫 𝐴 ↔ ∪ ( 𝐿 ↾t 𝐴 ) ⊆ 𝐴 )
17	15 16	mpbi	⊢ ∪ ( 𝐿 ↾t 𝐴 ) ⊆ 𝐴
18	17	a1i	⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ∪ ( 𝐿 ↾t 𝐴 ) ⊆ 𝐴 )
19	14 18	eqssd	⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝐴 = ∪ ( 𝐿 ↾t 𝐴 ) )