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 \in Fil (Y) \land A \subseteq Y) \to A = ⋃ (L ↾_{𝑡} A)$

Step	Hyp	Ref	Expression
1		simpr	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to A \subseteq Y$
2		sseqin2	$⊢ A \subseteq Y \leftrightarrow Y \cap A = A$
3	1 2	sylib	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to Y \cap A = A$
4		simpl	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to L \in Fil (Y)$
5		id	$⊢ A \subseteq Y \to A \subseteq Y$
6		filtop	$⊢ L \in Fil (Y) \to Y \in L$
7		ssexg	$⊢ (A \subseteq Y \land Y \in L) \to A \in V$
8	5 6 7	syl2anr	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to A \in V$
9	6	adantr	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to Y \in L$
10		elrestr	$⊢ (L \in Fil (Y) \land A \in V \land Y \in L) \to Y \cap A \in (L ↾_{𝑡} A)$
11	4 8 9 10	syl3anc	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to Y \cap A \in (L ↾_{𝑡} A)$
12	3 11	eqeltrrd	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to A \in (L ↾_{𝑡} A)$
13		elssuni	$⊢ A \in (L ↾_{𝑡} A) \to A \subseteq ⋃ (L ↾_{𝑡} A)$
14	12 13	syl	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to A \subseteq ⋃ (L ↾_{𝑡} A)$
15		restsspw	$⊢ L ↾_{𝑡} A \subseteq 𝒫 A$
16		sspwuni	$⊢ L ↾_{𝑡} A \subseteq 𝒫 A \leftrightarrow ⋃ (L ↾_{𝑡} A) \subseteq A$
17	15 16	mpbi	$⊢ ⋃ (L ↾_{𝑡} A) \subseteq A$
18	17	a1i	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to ⋃ (L ↾_{𝑡} A) \subseteq A$
19	14 18	eqssd	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to A = ⋃ (L ↾_{𝑡} A)$

Metamath Proof Explorer