elpm2r

Description: Sufficient condition for being a partial function. (Contributed by NM, 31-Dec-2013)

		Ref	Expression
	Assertion	elpm2r	$⊢ ((A \in V \land B \in W) \land (F : C ⟶ A \land C \subseteq B)) \to F \in (A ↑_{𝑝𝑚} B)$

Step	Hyp	Ref	Expression
1		fdm	$⊢ F : C ⟶ A \to dom F = C$
2	1	feq2d	$⊢ F : C ⟶ A \to (F : dom F ⟶ A \leftrightarrow F : C ⟶ A)$
3	1	sseq1d	$⊢ F : C ⟶ A \to (dom F \subseteq B \leftrightarrow C \subseteq B)$
4	2 3	anbi12d	$⊢ F : C ⟶ A \to ((F : dom F ⟶ A \land dom F \subseteq B) \leftrightarrow (F : C ⟶ A \land C \subseteq B))$
5	4	adantr	$⊢ (F : C ⟶ A \land C \subseteq B) \to ((F : dom F ⟶ A \land dom F \subseteq B) \leftrightarrow (F : C ⟶ A \land C \subseteq B))$
6	5	ibir	$⊢ (F : C ⟶ A \land C \subseteq B) \to (F : dom F ⟶ A \land dom F \subseteq B)$
7		elpm2g	$⊢ (A \in V \land B \in W) \to (F \in (A ↑_{𝑝𝑚} B) \leftrightarrow (F : dom F ⟶ A \land dom F \subseteq B))$
8	6 7	imbitrrid	$⊢ (A \in V \land B \in W) \to ((F : C ⟶ A \land C \subseteq B) \to F \in (A ↑_{𝑝𝑚} B))$
9	8	imp	$⊢ ((A \in V \land B \in W) \land (F : C ⟶ A \land C \subseteq B)) \to F \in (A ↑_{𝑝𝑚} B)$

Metamath Proof Explorer