Metamath Proof Explorer

Theorem fiss

Description: Subset relationship for function fi . (Contributed by Jeff Hankins, 7-Oct-2009) (Revised by Mario Carneiro, 24-Nov-2013)

		Ref	Expression
	Assertion	fiss	$⊢ (B \in V \land A \subseteq B) \to fi (A) \subseteq fi (B)$

Proof

Step	Hyp	Ref	Expression
1		sstr2	$⊢ A \subseteq B \to (B \subseteq y \to A \subseteq y)$
2	1	adantl	$⊢ (B \in V \land A \subseteq B) \to (B \subseteq y \to A \subseteq y)$
3	2	anim1d	$⊢ (B \in V \land A \subseteq B) \to ((B \subseteq y \land \forall x \in y \forall z \in y x \cap z \in y) \to (A \subseteq y \land \forall x \in y \forall z \in y x \cap z \in y))$
4	3	ss2abdv	$⊢ (B \in V \land A \subseteq B) \to \{y \| (B \subseteq y \land \forall x \in y \forall z \in y x \cap z \in y)\} \subseteq \{y \| (A \subseteq y \land \forall x \in y \forall z \in y x \cap z \in y)\}$
5		intss	$⊢ \{y \| (B \subseteq y \land \forall x \in y \forall z \in y x \cap z \in y)\} \subseteq \{y \| (A \subseteq y \land \forall x \in y \forall z \in y x \cap z \in y)\} \to ⋂ \{y \| (A \subseteq y \land \forall x \in y \forall z \in y x \cap z \in y)\} \subseteq ⋂ \{y \| (B \subseteq y \land \forall x \in y \forall z \in y x \cap z \in y)\}$
6	4 5	syl	$⊢ (B \in V \land A \subseteq B) \to ⋂ \{y \| (A \subseteq y \land \forall x \in y \forall z \in y x \cap z \in y)\} \subseteq ⋂ \{y \| (B \subseteq y \land \forall x \in y \forall z \in y x \cap z \in y)\}$
7		ssexg	$⊢ (A \subseteq B \land B \in V) \to A \in V$
8	7	ancoms	$⊢ (B \in V \land A \subseteq B) \to A \in V$
9		dffi2	$⊢ A \in V \to fi (A) = ⋂ \{y \| (A \subseteq y \land \forall x \in y \forall z \in y x \cap z \in y)\}$
10	8 9	syl	$⊢ (B \in V \land A \subseteq B) \to fi (A) = ⋂ \{y \| (A \subseteq y \land \forall x \in y \forall z \in y x \cap z \in y)\}$
11		dffi2	$⊢ B \in V \to fi (B) = ⋂ \{y \| (B \subseteq y \land \forall x \in y \forall z \in y x \cap z \in y)\}$
12	11	adantr	$⊢ (B \in V \land A \subseteq B) \to fi (B) = ⋂ \{y \| (B \subseteq y \land \forall x \in y \forall z \in y x \cap z \in y)\}$
13	6 10 12	3sstr4d	$⊢ (B \in V \land A \subseteq B) \to fi (A) \subseteq fi (B)$