Theorem ndmovcl 7566

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.)

Hypotheses

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

Assertion

Ref	Expression
ndmovcl	⊢ (𝐴𝐹𝐵) ∈ 𝑆

Proof of Theorem ndmovcl

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   = wceq 1550   ∈ wcel 2132  ∅c0 4276   × cxp 5634  dom cdm 5636  (class class class)co 7381

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724  ax-sep 5236  ax-nul 5246  ax-pr 5380

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-ne 2948  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-opab 5153  df-xp 5642  df-dm 5646  df-iota 6462  df-fv 6514  df-ov 7384

This theorem is referenced by: (None)