Theorem fpmd

Description: A total function is a partial function. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	fpmd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	fpmd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	fpmd.c	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
	fpmd.f	⊢ ( 𝜑 → 𝐹 : 𝐶 ⟶ 𝐵 )
Assertion	fpmd	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐵 ↑pm 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		fpmd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		fpmd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		fpmd.c	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
4		fpmd.f	⊢ ( 𝜑 → 𝐹 : 𝐶 ⟶ 𝐵 )
5		elpm2r	⊢ ( ( ( 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 ⟶ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) ) → 𝐹 ∈ ( 𝐵 ↑pm 𝐴 ) )
6	2 1 4 3 5	syl22anc	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐵 ↑pm 𝐴 ) )