Theorem fpmd

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

	Ref	Expression
Hypotheses	fpmd.a	|- ( ph -> A e. V )
	fpmd.b	|- ( ph -> B e. W )
	fpmd.c	|- ( ph -> C C_ A )
	fpmd.f	|- ( ph -> F : C --> B )
Assertion	fpmd	|- ( ph -> F e. ( B ^pm A ) )

Proof

Step	Hyp	Ref	Expression
1		fpmd.a	|- ( ph -> A e. V )
2		fpmd.b	|- ( ph -> B e. W )
3		fpmd.c	|- ( ph -> C C_ A )
4		fpmd.f	|- ( ph -> F : C --> B )
5		elpm2r	|- ( ( ( B e. W /\ A e. V ) /\ ( F : C --> B /\ C C_ A ) ) -> F e. ( B ^pm A ) )
6	2 1 4 3 5	syl22anc	|- ( ph -> F e. ( B ^pm A ) )