fin

Description: Mapping into an intersection. (Contributed by NM, 14-Sep-1999) (Proof shortened by Andrew Salmon, 17-Sep-2011)

		Ref	Expression
	Assertion	fin	$⊢ F : A ⟶ B \cap C \leftrightarrow (F : A ⟶ B \land F : A ⟶ C)$

Step	Hyp	Ref	Expression
1		ssin	$⊢ (ran F \subseteq B \land ran F \subseteq C) \leftrightarrow ran F \subseteq B \cap C$
2	1	anbi2i	$⊢ (F Fn A \land (ran F \subseteq B \land ran F \subseteq C)) \leftrightarrow (F Fn A \land ran F \subseteq B \cap C)$
3		anandi	$⊢ (F Fn A \land (ran F \subseteq B \land ran F \subseteq C)) \leftrightarrow ((F Fn A \land ran F \subseteq B) \land (F Fn A \land ran F \subseteq C))$
4	2 3	bitr3i	$⊢ (F Fn A \land ran F \subseteq B \cap C) \leftrightarrow ((F Fn A \land ran F \subseteq B) \land (F Fn A \land ran F \subseteq C))$
5		df-f	$⊢ F : A ⟶ B \cap C \leftrightarrow (F Fn A \land ran F \subseteq B \cap C)$
6		df-f	$⊢ F : A ⟶ B \leftrightarrow (F Fn A \land ran F \subseteq B)$
7		df-f	$⊢ F : A ⟶ C \leftrightarrow (F Fn A \land ran F \subseteq C)$
8	6 7	anbi12i	$⊢ (F : A ⟶ B \land F : A ⟶ C) \leftrightarrow ((F Fn A \land ran F \subseteq B) \land (F Fn A \land ran F \subseteq C))$
9	4 5 8	3bitr4i	$⊢ F : A ⟶ B \cap C \leftrightarrow (F : A ⟶ B \land F : A ⟶ C)$

Metamath Proof Explorer