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	⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 /f 𝐺 ) ∈ ( ℝ ↑pm 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		reex	⊢ ℝ ∈ V
2	1	a1i	⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ 𝑉 ) → ℝ ∈ V )
3		simp3	⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
4		refdivmptf	⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 /f 𝐺 ) : ( 𝐺 supp 0 ) ⟶ ℝ )
5		suppssdm	⊢ ( 𝐺 supp 0 ) ⊆ dom 𝐺
6		fdm	⊢ ( 𝐺 : 𝐴 ⟶ ℝ → dom 𝐺 = 𝐴 )
7	6	eqcomd	⊢ ( 𝐺 : 𝐴 ⟶ ℝ → 𝐴 = dom 𝐺 )
8	7	3ad2ant2	⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ 𝑉 ) → 𝐴 = dom 𝐺 )
9	5 8	sseqtrrid	⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ 𝑉 ) → ( 𝐺 supp 0 ) ⊆ 𝐴 )
10		elpm2r	⊢ ( ( ( ℝ ∈ V ∧ 𝐴 ∈ 𝑉 ) ∧ ( ( 𝐹 /f 𝐺 ) : ( 𝐺 supp 0 ) ⟶ ℝ ∧ ( 𝐺 supp 0 ) ⊆ 𝐴 ) ) → ( 𝐹 /f 𝐺 ) ∈ ( ℝ ↑pm 𝐴 ) )
11	2 3 4 9 10	syl22anc	⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 /f 𝐺 ) ∈ ( ℝ ↑pm 𝐴 ) )