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

Metamath Proof Explorer

Theorem ndmovcl

Description: The closure of an operation outside its domain, when the domain includes the empty set. This technical lemma can make the operation more convenient to work in some cases. It is dependent on our particular definitions of operation value, function value, and ordered pair. (Contributed by NM, 24-Sep-2004)

	Ref	Expression
Hypotheses	ndmov.1	⊢ dom 𝐹 = ( 𝑆 × 𝑆 )
	ndmovcl.2	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 𝐹 𝐵 ) ∈ 𝑆 )
	ndmovcl.3	⊢ ∅ ∈ 𝑆
Assertion	ndmovcl	⊢ ( 𝐴 𝐹 𝐵 ) ∈ 𝑆

Proof

Step	Hyp	Ref	Expression
1		ndmov.1	⊢ dom 𝐹 = ( 𝑆 × 𝑆 )
2		ndmovcl.2	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 𝐹 𝐵 ) ∈ 𝑆 )
3		ndmovcl.3	⊢ ∅ ∈ 𝑆
4	1	ndmov	⊢ ( ¬ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 𝐹 𝐵 ) = ∅ )
5	4 3	eqeltrdi	⊢ ( ¬ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 𝐹 𝐵 ) ∈ 𝑆 )
6	2 5	pm2.61i	⊢ ( 𝐴 𝐹 𝐵 ) ∈ 𝑆