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

Metamath Proof Explorer

Theorem trfilss

Description: If A is a member of the filter, then the filter truncated to A is a subset of the original filter. (Contributed by Mario Carneiro, 15-Oct-2015)

		Ref	Expression
	Assertion	trfilss	$⊢ (F \in Fil (X) \land A \in F) \to F ↾_{𝑡} A \subseteq F$

Proof

Step	Hyp	Ref	Expression
1		restval	$⊢ (F \in Fil (X) \land A \in F) \to F ↾_{𝑡} A = ran (x \in F ⟼ x \cap A)$
2		filin	$⊢ (F \in Fil (X) \land x \in F \land A \in F) \to x \cap A \in F$
3	2	3expa	$⊢ ((F \in Fil (X) \land x \in F) \land A \in F) \to x \cap A \in F$
4	3	an32s	$⊢ ((F \in Fil (X) \land A \in F) \land x \in F) \to x \cap A \in F$
5	4	fmpttd	$⊢ (F \in Fil (X) \land A \in F) \to (x \in F ⟼ x \cap A) : F ⟶ F$
6	5	frnd	$⊢ (F \in Fil (X) \land A \in F) \to ran (x \in F ⟼ x \cap A) \subseteq F$
7	1 6	eqsstrd	$⊢ (F \in Fil (X) \land A \in F) \to F ↾_{𝑡} A \subseteq F$