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

Metamath Proof Explorer

Theorem nssdmovg

Description: The value of an operation outside its domain. (Contributed by Alexander van der Vekens, 7-Sep-2017)

Ref Expression
Assertion nssdmovg ( ( dom 𝐹 ⊆ ( 𝑅 × 𝑆 ) ∧ ¬ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) → ( 𝐴 𝐹 𝐵 ) = ∅ )

Proof

Step Hyp Ref Expression
1 df-ov ⊢ ( 𝐴 𝐹 𝐵 ) = ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
2 ssel2 ⊢ ( ( dom 𝐹 ⊆ ( 𝑅 × 𝑆 ) ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑅 × 𝑆 ) )
3 opelxp ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑅 × 𝑆 ) ↔ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) )
4 2 3 sylib ⊢ ( ( dom 𝐹 ⊆ ( 𝑅 × 𝑆 ) ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 ) → ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) )
5 4 stoic1a ⊢ ( ( dom 𝐹 ⊆ ( 𝑅 × 𝑆 ) ∧ ¬ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) → ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 )
6 ndmfv ⊢ ( ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 → ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ )
7 5 6 syl ⊢ ( ( dom 𝐹 ⊆ ( 𝑅 × 𝑆 ) ∧ ¬ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) → ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ )
8 1 7 eqtrid ⊢ ( ( dom 𝐹 ⊆ ( 𝑅 × 𝑆 ) ∧ ¬ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) → ( 𝐴 𝐹 𝐵 ) = ∅ )