This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fpm

Description: A total function is a partial function. (Contributed by NM, 15-Nov-2007) (Revised by Mario Carneiro, 31-Dec-2013)

Ref Expression
Hypotheses elmap.1 ⊢ 𝐴 ∈ V
elmap.2 ⊢ 𝐵 ∈ V
Assertion fpm ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 ∈ ( 𝐵 ↑pm 𝐴 ) )

Proof

Step Hyp Ref Expression
1 elmap.1 ⊢ 𝐴 ∈ V
2 elmap.2 ⊢ 𝐵 ∈ V
3 fpmg ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝐹 ∈ ( 𝐵 ↑pm 𝐴 ) )
4 1 2 3 mp3an12 ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 ∈ ( 𝐵 ↑pm 𝐴 ) )