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

Metamath Proof Explorer

Theorem elpm2r

Description: Sufficient condition for being a partial function. (Contributed by NM, 31-Dec-2013)

Ref Expression
Assertion elpm2r ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐹 : 𝐶 ⟶ 𝐴 ∧ 𝐶 ⊆ 𝐵 ) ) → 𝐹 ∈ ( 𝐴 ↑pm 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fdm ⊢ ( 𝐹 : 𝐶 ⟶ 𝐴 → dom 𝐹 = 𝐶 )
2 1 feq2d ⊢ ( 𝐹 : 𝐶 ⟶ 𝐴 → ( 𝐹 : dom 𝐹 ⟶ 𝐴 ↔ 𝐹 : 𝐶 ⟶ 𝐴 ) )
3 1 sseq1d ⊢ ( 𝐹 : 𝐶 ⟶ 𝐴 → ( dom 𝐹 ⊆ 𝐵 ↔ 𝐶 ⊆ 𝐵 ) )
4 2 3 anbi12d ⊢ ( 𝐹 : 𝐶 ⟶ 𝐴 → ( ( 𝐹 : dom 𝐹 ⟶ 𝐴 ∧ dom 𝐹 ⊆ 𝐵 ) ↔ ( 𝐹 : 𝐶 ⟶ 𝐴 ∧ 𝐶 ⊆ 𝐵 ) ) )
5 4 adantr ⊢ ( ( 𝐹 : 𝐶 ⟶ 𝐴 ∧ 𝐶 ⊆ 𝐵 ) → ( ( 𝐹 : dom 𝐹 ⟶ 𝐴 ∧ dom 𝐹 ⊆ 𝐵 ) ↔ ( 𝐹 : 𝐶 ⟶ 𝐴 ∧ 𝐶 ⊆ 𝐵 ) ) )
6 5 ibir ⊢ ( ( 𝐹 : 𝐶 ⟶ 𝐴 ∧ 𝐶 ⊆ 𝐵 ) → ( 𝐹 : dom 𝐹 ⟶ 𝐴 ∧ dom 𝐹 ⊆ 𝐵 ) )
7 elpm2g ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐹 ∈ ( 𝐴 ↑pm 𝐵 ) ↔ ( 𝐹 : dom 𝐹 ⟶ 𝐴 ∧ dom 𝐹 ⊆ 𝐵 ) ) )
8 6 7 imbitrrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐹 : 𝐶 ⟶ 𝐴 ∧ 𝐶 ⊆ 𝐵 ) → 𝐹 ∈ ( 𝐴 ↑pm 𝐵 ) ) )
9 8 imp ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐹 : 𝐶 ⟶ 𝐴 ∧ 𝐶 ⊆ 𝐵 ) ) → 𝐹 ∈ ( 𝐴 ↑pm 𝐵 ) )