Theorem elpmi

Description: A partial function is a function. (Contributed by Mario Carneiro, 15-Sep-2015)

	Ref	Expression
Assertion	elpmi	⊢ ( 𝐹 ∈ ( 𝐴 ↑pm 𝐵 ) → ( 𝐹 : dom 𝐹 ⟶ 𝐴 ∧ dom 𝐹 ⊆ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		n0i	⊢ ( 𝐹 ∈ ( 𝐴 ↑pm 𝐵 ) → ¬ ( 𝐴 ↑pm 𝐵 ) = ∅ )
2		fnpm	⊢ ↑pm Fn ( V × V )
3	2	fndmi	⊢ dom ↑pm = ( V × V )
4	3	ndmov	⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 ↑pm 𝐵 ) = ∅ )
5	1 4	nsyl2	⊢ ( 𝐹 ∈ ( 𝐴 ↑pm 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
6		elpm2g	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐹 ∈ ( 𝐴 ↑pm 𝐵 ) ↔ ( 𝐹 : dom 𝐹 ⟶ 𝐴 ∧ dom 𝐹 ⊆ 𝐵 ) ) )
7	5 6	syl	⊢ ( 𝐹 ∈ ( 𝐴 ↑pm 𝐵 ) → ( 𝐹 ∈ ( 𝐴 ↑pm 𝐵 ) ↔ ( 𝐹 : dom 𝐹 ⟶ 𝐴 ∧ dom 𝐹 ⊆ 𝐵 ) ) )
8	7	ibi	⊢ ( 𝐹 ∈ ( 𝐴 ↑pm 𝐵 ) → ( 𝐹 : dom 𝐹 ⟶ 𝐴 ∧ dom 𝐹 ⊆ 𝐵 ) )