fmss

Description: A finer filter produces a finer image filter. (Contributed by Jeff Hankins, 16-Nov-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

		Ref	Expression
	Assertion	fmss	$⊢ ((X \in A \land B \in fBas (Y) \land C \in fBas (Y)) \land (F : Y ⟶ X \land B \subseteq C)) \to (X FilMap F) (B) \subseteq (X FilMap F) (C)$

Proof

Step	Hyp	Ref	Expression
1		simpl2	$⊢ ((X \in A \land B \in fBas (Y) \land C \in fBas (Y)) \land (F : Y ⟶ X \land B \subseteq C)) \to B \in fBas (Y)$
2		simprl	$⊢ ((X \in A \land B \in fBas (Y) \land C \in fBas (Y)) \land (F : Y ⟶ X \land B \subseteq C)) \to F : Y ⟶ X$
3		simpl1	$⊢ ((X \in A \land B \in fBas (Y) \land C \in fBas (Y)) \land (F : Y ⟶ X \land B \subseteq C)) \to X \in A$
4		eqid	$⊢ ran (y \in B ⟼ F [y]) = ran (y \in B ⟼ F [y])$
5	4	fbasrn	$⊢ (B \in fBas (Y) \land F : Y ⟶ X \land X \in A) \to ran (y \in B ⟼ F [y]) \in fBas (X)$
6	1 2 3 5	syl3anc	$⊢ ((X \in A \land B \in fBas (Y) \land C \in fBas (Y)) \land (F : Y ⟶ X \land B \subseteq C)) \to ran (y \in B ⟼ F [y]) \in fBas (X)$
7		simpl3	$⊢ ((X \in A \land B \in fBas (Y) \land C \in fBas (Y)) \land (F : Y ⟶ X \land B \subseteq C)) \to C \in fBas (Y)$
8		eqid	$⊢ ran (y \in C ⟼ F [y]) = ran (y \in C ⟼ F [y])$
9	8	fbasrn	$⊢ (C \in fBas (Y) \land F : Y ⟶ X \land X \in A) \to ran (y \in C ⟼ F [y]) \in fBas (X)$
10	7 2 3 9	syl3anc	$⊢ ((X \in A \land B \in fBas (Y) \land C \in fBas (Y)) \land (F : Y ⟶ X \land B \subseteq C)) \to ran (y \in C ⟼ F [y]) \in fBas (X)$
11		resmpt	$⊢ B \subseteq C \to {(y \in C ⟼ F [y]) ↾}_{B} = (y \in B ⟼ F [y])$
12	11	ad2antll	$⊢ ((X \in A \land B \in fBas (Y) \land C \in fBas (Y)) \land (F : Y ⟶ X \land B \subseteq C)) \to {(y \in C ⟼ F [y]) ↾}_{B} = (y \in B ⟼ F [y])$
13		resss	$⊢ {(y \in C ⟼ F [y]) ↾}_{B} \subseteq (y \in C ⟼ F [y])$
14	12 13	eqsstrrdi	$⊢ ((X \in A \land B \in fBas (Y) \land C \in fBas (Y)) \land (F : Y ⟶ X \land B \subseteq C)) \to (y \in B ⟼ F [y]) \subseteq (y \in C ⟼ F [y])$
15		rnss	$⊢ (y \in B ⟼ F [y]) \subseteq (y \in C ⟼ F [y]) \to ran (y \in B ⟼ F [y]) \subseteq ran (y \in C ⟼ F [y])$
16	14 15	syl	$⊢ ((X \in A \land B \in fBas (Y) \land C \in fBas (Y)) \land (F : Y ⟶ X \land B \subseteq C)) \to ran (y \in B ⟼ F [y]) \subseteq ran (y \in C ⟼ F [y])$
17		fgss	$⊢ (ran (y \in B ⟼ F [y]) \in fBas (X) \land ran (y \in C ⟼ F [y]) \in fBas (X) \land ran (y \in B ⟼ F [y]) \subseteq ran (y \in C ⟼ F [y])) \to X filGen ran (y \in B ⟼ F [y]) \subseteq X filGen ran (y \in C ⟼ F [y])$
18	6 10 16 17	syl3anc	$⊢ ((X \in A \land B \in fBas (Y) \land C \in fBas (Y)) \land (F : Y ⟶ X \land B \subseteq C)) \to X filGen ran (y \in B ⟼ F [y]) \subseteq X filGen ran (y \in C ⟼ F [y])$
19		fmval	$⊢ (X \in A \land B \in fBas (Y) \land F : Y ⟶ X) \to (X FilMap F) (B) = X filGen ran (y \in B ⟼ F [y])$
20	3 1 2 19	syl3anc	$⊢ ((X \in A \land B \in fBas (Y) \land C \in fBas (Y)) \land (F : Y ⟶ X \land B \subseteq C)) \to (X FilMap F) (B) = X filGen ran (y \in B ⟼ F [y])$
21		fmval	$⊢ (X \in A \land C \in fBas (Y) \land F : Y ⟶ X) \to (X FilMap F) (C) = X filGen ran (y \in C ⟼ F [y])$
22	3 7 2 21	syl3anc	$⊢ ((X \in A \land B \in fBas (Y) \land C \in fBas (Y)) \land (F : Y ⟶ X \land B \subseteq C)) \to (X FilMap F) (C) = X filGen ran (y \in C ⟼ F [y])$
23	18 20 22	3sstr4d	$⊢ ((X \in A \land B \in fBas (Y) \land C \in fBas (Y)) \land (F : Y ⟶ X \land B \subseteq C)) \to (X FilMap F) (B) \subseteq (X FilMap F) (C)$

Metamath Proof Explorer

Theorem fmss

Proof