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

Metamath Proof Explorer

Theorem ndmovg

Description: The value of an operation outside its domain. (Contributed by NM, 28-Mar-2008)

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

Proof

Step Hyp Ref Expression
1 df-ov ⊢ ( 𝐴 𝐹 𝐵 ) = ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
2 eleq2 ⊢ ( dom 𝐹 = ( 𝑅 × 𝑆 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑅 × 𝑆 ) ) )
3 opelxp ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑅 × 𝑆 ) ↔ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) )
4 2 3 bitrdi ⊢ ( dom 𝐹 = ( 𝑅 × 𝑆 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 ↔ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) )
5 4 notbid ⊢ ( dom 𝐹 = ( 𝑅 × 𝑆 ) → ( ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 ↔ ¬ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) )
6 ndmfv ⊢ ( ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 → ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ )
7 5 6 biimtrrdi ⊢ ( dom 𝐹 = ( 𝑅 × 𝑆 ) → ( ¬ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ ) )
8 7 imp ⊢ ( ( dom 𝐹 = ( 𝑅 × 𝑆 ) ∧ ¬ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) → ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ )
9 1 8 eqtrid ⊢ ( ( dom 𝐹 = ( 𝑅 × 𝑆 ) ∧ ¬ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) → ( 𝐴 𝐹 𝐵 ) = ∅ )