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 FFilXAFF𝑡AF

Proof

Step Hyp Ref Expression
1 restval FFilXAFF𝑡A=ranxFxA
2 filin FFilXxFAFxAF
3 2 3expa FFilXxFAFxAF
4 3 an32s FFilXAFxFxAF
5 4 fmpttd FFilXAFxFxA:FF
6 5 frnd FFilXAFranxFxAF
7 1 6 eqsstrd FFilXAFF𝑡AF