Theorem refdivpm

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

	Ref	Expression
Assertion	refdivpm

Proof

Step	Hyp	Ref	Expression
1		reex	$$⊢ℝ\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		refdivmptf
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