fpmg

Description: A total function is a partial function. (Contributed by Mario Carneiro, 31-Dec-2013)

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

Step	Hyp	Ref	Expression
1		ssid	$⊢ A \subseteq A$
2		elpm2r	$⊢ ((B \in W \land A \in V) \land (F : A ⟶ B \land A \subseteq A)) \to F \in (B ↑_{𝑝𝑚} A)$
3	1 2	mpanr2	$⊢ ((B \in W \land A \in V) \land F : A ⟶ B) \to F \in (B ↑_{𝑝𝑚} A)$
4	3	3impa	$⊢ (B \in W \land A \in V \land F : A ⟶ B) \to F \in (B ↑_{𝑝𝑚} A)$
5	4	3com12	$⊢ (A \in V \land B \in W \land F : A ⟶ B) \to F \in (B ↑_{𝑝𝑚} A)$

Metamath Proof Explorer