k0004lem1

Description: Application of ssin to range of a function. (Contributed by RP, 1-Apr-2021)

		Ref	Expression
	Assertion	k0004lem1	$⊢ D = B \cap C \to ((F : A ⟶ B \land F [A] \subseteq C) \leftrightarrow F : A ⟶ D)$

Step	Hyp	Ref	Expression
1		fnima	$⊢ F Fn A \to F [A] = ran F$
2	1	sseq1d	$⊢ F Fn A \to (F [A] \subseteq C \leftrightarrow ran F \subseteq C)$
3	2	anbi2d	$⊢ F Fn A \to ((ran F \subseteq B \land F [A] \subseteq C) \leftrightarrow (ran F \subseteq B \land ran F \subseteq C))$
4		ssin	$⊢ (ran F \subseteq B \land ran F \subseteq C) \leftrightarrow ran F \subseteq B \cap C$
5	3 4	bitrdi	$⊢ F Fn A \to ((ran F \subseteq B \land F [A] \subseteq C) \leftrightarrow ran F \subseteq B \cap C)$
6	5	pm5.32i	$⊢ (F Fn A \land (ran F \subseteq B \land F [A] \subseteq C)) \leftrightarrow (F Fn A \land ran F \subseteq B \cap C)$
7		df-f	$⊢ F : A ⟶ B \leftrightarrow (F Fn A \land ran F \subseteq B)$
8	7	anbi1i	$⊢ (F : A ⟶ B \land F [A] \subseteq C) \leftrightarrow ((F Fn A \land ran F \subseteq B) \land F [A] \subseteq C)$
9		anass	$⊢ ((F Fn A \land ran F \subseteq B) \land F [A] \subseteq C) \leftrightarrow (F Fn A \land (ran F \subseteq B \land F [A] \subseteq C))$
10	8 9	bitri	$⊢ (F : A ⟶ B \land F [A] \subseteq C) \leftrightarrow (F Fn A \land (ran F \subseteq B \land F [A] \subseteq C))$
11		df-f	$⊢ F : A ⟶ B \cap C \leftrightarrow (F Fn A \land ran F \subseteq B \cap C)$
12	6 10 11	3bitr4i	$⊢ (F : A ⟶ B \land F [A] \subseteq C) \leftrightarrow F : A ⟶ B \cap C$
13		feq3	$⊢ D = B \cap C \to (F : A ⟶ D \leftrightarrow F : A ⟶ B \cap C)$
14	12 13	bitr4id	$⊢ D = B \cap C \to ((F : A ⟶ B \land F [A] \subseteq C) \leftrightarrow F : A ⟶ D)$

Metamath Proof Explorer