Theorem fpmg

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

	Ref	Expression
Assertion	fpmg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝐹 ∈ ( 𝐵 ↑pm 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ssid	⊢ 𝐴 ⊆ 𝐴
2		elpm2r	⊢ ( ( ( 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐴 ) ) → 𝐹 ∈ ( 𝐵 ↑pm 𝐴 ) )
3	1 2	mpanr2	⊢ ( ( ( 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝐹 ∈ ( 𝐵 ↑pm 𝐴 ) )
4	3	3impa	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝐹 ∈ ( 𝐵 ↑pm 𝐴 ) )
5	4	3com12	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝐹 ∈ ( 𝐵 ↑pm 𝐴 ) )