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	$$⊢\left(F\in \mathrm{Fil}\left(X\right)\wedge A\in F\right)\to F{\upharpoonright }_{𝑡}A\subseteq F$$

Proof

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