Theorem fdivpm

Description: The quotient of two functions into the complex numbers is a partial function. (Contributed by AV, 16-May-2020)

	Ref	Expression
Assertion	fdivpm

Proof

Step	Hyp	Ref	Expression
1		cnex	$$⊢ℂ\in \mathrm{V}$$
2	1	a1i	$$⊢\left(F:A⟶ℂ\wedge G:A⟶ℂ\wedge A\in V\right)\to ℂ\in \mathrm{V}$$
3		simp3	$$⊢\left(F:A⟶ℂ\wedge G:A⟶ℂ\wedge A\in V\right)\to A\in V$$
4		fdivmptf
5		suppssdm	$$⊢G\mathrm{supp}0\subseteq \mathrm{dom}G$$
6		fdm	$$⊢G:A⟶ℂ\to \mathrm{dom}G=A$$
7	6	eqcomd	$$⊢G:A⟶ℂ\to A=\mathrm{dom}G$$
8	7	3ad2ant2	$$⊢\left(F:A⟶ℂ\wedge G:A⟶ℂ\wedge A\in V\right)\to A=\mathrm{dom}G$$
9	5 8	sseqtrrid	$$⊢\left(F:A⟶ℂ\wedge G:A⟶ℂ\wedge A\in V\right)\to G\mathrm{supp}0\subseteq A$$
10		elpm2r
11	2 3 4 9 10	syl22anc