Theorem ndmoprcl 3984

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 is dependent on our particular definitions of operation value, function value, and ordered pair.

Hypotheses

Ref	Expression
ndmoprcl.1	|- dom F = (S X. S)
ndmoprcl.2	|- ((A e. S /\ x e. S) -> (AFx) e. S)
ndmoprcl.3	|- (/) e. S

Assertion

Ref	Expression
ndmoprcl	|- (AFB) e. S

Distinct variable groups:   x,A   x,B   x,F   x,S

Proof of Theorem ndmoprcl

Step	Hyp	Ref	Expression
1		oprprc2 3924	. . . . 5 |- (-. B e. V -> (AFB) = (AFA))
2	1	eleq1d 1516	. . . 4 |- (-. B e. V -> ((AFB) e. S <-> (AFA) e. S))
3		ndmoprcl.1	. . . . . . . 8 |- dom F = (S X. S)
4	3	ndmoprgOLD 3983	. . . . . . 7 |- ((A e. V /\ -. (A e. S /\ A e. S)) -> (AFA) = (/))
5		ndmoprcl.3	. . . . . . 7 |- (/) e. S
6	4, 5	syl6eqel 1532	. . . . . 6 |- ((A e. V /\ -. (A e. S /\ A e. S)) -> (AFA) e. S)
7	6	ex 373	. . . . 5 |- (A e. V -> (-. (A e. S /\ A e. S) -> (AFA) e. S))
8		opreq2 3908	. . . . . . . . 9 |- (x = A -> (AFx) = (AFA))
9	8	eleq1d 1516	. . . . . . . 8 |- (x = A -> ((AFx) e. S <-> (AFA) e. S))
10	9	imbi2d 610	. . . . . . 7 |- (x = A -> ((A e. S -> (AFx) e. S) <-> (A e. S -> (AFA) e. S)))
11		ndmoprcl.2	. . . . . . . 8 |- ((A e. S /\ x e. S) -> (AFx) e. S)
12	11	expcom 374	. . . . . . 7 |- (x e. S -> (A e. S -> (AFx) e. S))
13	10, 12	vtoclga 1827	. . . . . 6 |- (A e. S -> (A e. S -> (AFA) e. S))
14	13	imp 350	. . . . 5 |- ((A e. S /\ A e. S) -> (AFA) e. S)
15	7, 14	pm2.61d2 129	. . . 4 |- (A e. V -> (AFA) e. S)
16	2, 15	syl5cbir 211	. . 3 |- (A e. V -> (-. B e. V -> (AFB) e. S))
17	3	ndmoprgOLD 3983	. . . . . 6 |- ((B e. V /\ -. (A e. S /\ B e. S)) -> (AFB) = (/))
18	17, 5	syl6eqel 1532	. . . . 5 |- ((B e. V /\ -. (A e. S /\ B e. S)) -> (AFB) e. S)
19	18	ex 373	. . . 4 |- (B e. V -> (-. (A e. S /\ B e. S) -> (AFB) e. S))
20		opreq2 3908	. . . . . . . 8 |- (x = B -> (AFx) = (AFB))
21	20	eleq1d 1516	. . . . . . 7 |- (x = B -> ((AFx) e. S <-> (AFB) e. S))
22	21	imbi2d 610	. . . . . 6 |- (x = B -> ((A e. S -> (AFx) e. S) <-> (A e. S -> (AFB) e. S)))
23	22, 12	vtoclga 1827	. . . . 5 |- (B e. S -> (A e. S -> (AFB) e. S))
24	23	impcom 351	. . . 4 |- ((A e. S /\ B e. S) -> (AFB) e. S)
25	19, 24	pm2.61d2 129	. . 3 |- (B e. V -> (AFB) e. S)
26	16, 25	pm2.61d2 129	. 2 |- (A e. V -> (AFB) e. S)
27		relxp 3217	. . . . 5 |- Rel (S X. S)
28	3	releqi 3206	. . . . 5 |- (Rel dom F <-> Rel (S X. S))
29	27, 28	mpbir 190	. . . 4 |- Rel dom F
30	29	oprprc1 3923	. . 3 |- (-. A e. V -> (AFB) = (/))
31	30, 5	syl6eqel 1532	. 2 |- (-. A e. V -> (AFB) e. S)
32	26, 31	pm2.61i 126	1 |- (AFB) e. S

Syntax hints:  -. wn 2   -> wi 3   /\ wa 223   = wceq 1099   e. wcel 1105  Vcvv 1786  (/)c0 2251   X. cxp 3131  dom cdm 3133  Rel wrel 3138  (class class class)co 3902

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-sep 2671  ax-nul 2678  ax-pow 2710  ax-pr 2747

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-ral 1625  df-rex 1626  df-v 1787  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-nul 2252  df-pw 2373  df-sn 2383  df-pr 2384  df-op 2387  df-uni 2472  df-br 2588  df-opab 2635  df-xp 3147  df-rel 3148  df-cnv 3149  df-dm 3151  df-rn 3152  df-res 3153  df-ima 3154  df-fv 3161  df-opr 3904

Copyright terms: Public domain