Metamath Proof Explorer


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 𝐴 ) )