let a, a1, v, v1, v2 be object ; :: thesis: for V, A being set st {v,v1,v2} c= V & {a,a1} c= A holds

ND_ex_4 (v,v1,v2,a,a1) in NDSS (V,(A \/ (NDSS (V,A))))

let V, A be set ; :: thesis: ( {v,v1,v2} c= V & {a,a1} c= A implies ND_ex_4 (v,v1,v2,a,a1) in NDSS (V,(A \/ (NDSS (V,A)))) )

assume that

A1: {v,v1,v2} c= V and

A2: {a,a1} c= A ; :: thesis: ND_ex_4 (v,v1,v2,a,a1) in NDSS (V,(A \/ (NDSS (V,A))))

v in {v,v1,v2} by ENUMSET1:def 1;

then A3: v in V by A1;

v1 in {v,v1,v2} by ENUMSET1:def 1;

then A4: v1 in V by A1;

A5: v2 in {v,v1,v2} by ENUMSET1:def 1;

A6: a in A by A2, ZFMISC_1:32;

A7: a1 in A by A2, ZFMISC_1:32;

set f = v2 .--> a1;

set g = ND_ex_4 (v,v1,v2,a,a1);

dom (ND_ex_4 (v,v1,v2,a,a1)) = {v,v1} by FUNCT_4:62;

then A8: dom (ND_ex_4 (v,v1,v2,a,a1)) c= V by A3, A4, TARSKI:def 2;

A9: rng (ND_ex_4 (v,v1,v2,a,a1)) c= {a,(v2 .--> a1)} by FUNCT_4:62;

rng (ND_ex_4 (v,v1,v2,a,a1)) c= A \/ (NDSS (V,A))

hence ND_ex_4 (v,v1,v2,a,a1) in NDSS (V,(A \/ (NDSS (V,A)))) ; :: thesis: verum

ND_ex_4 (v,v1,v2,a,a1) in NDSS (V,(A \/ (NDSS (V,A))))

let V, A be set ; :: thesis: ( {v,v1,v2} c= V & {a,a1} c= A implies ND_ex_4 (v,v1,v2,a,a1) in NDSS (V,(A \/ (NDSS (V,A)))) )

assume that

A1: {v,v1,v2} c= V and

A2: {a,a1} c= A ; :: thesis: ND_ex_4 (v,v1,v2,a,a1) in NDSS (V,(A \/ (NDSS (V,A))))

v in {v,v1,v2} by ENUMSET1:def 1;

then A3: v in V by A1;

v1 in {v,v1,v2} by ENUMSET1:def 1;

then A4: v1 in V by A1;

A5: v2 in {v,v1,v2} by ENUMSET1:def 1;

A6: a in A by A2, ZFMISC_1:32;

A7: a1 in A by A2, ZFMISC_1:32;

set f = v2 .--> a1;

set g = ND_ex_4 (v,v1,v2,a,a1);

dom (ND_ex_4 (v,v1,v2,a,a1)) = {v,v1} by FUNCT_4:62;

then A8: dom (ND_ex_4 (v,v1,v2,a,a1)) c= V by A3, A4, TARSKI:def 2;

A9: rng (ND_ex_4 (v,v1,v2,a,a1)) c= {a,(v2 .--> a1)} by FUNCT_4:62;

rng (ND_ex_4 (v,v1,v2,a,a1)) c= A \/ (NDSS (V,A))

proof

then
ND_ex_4 (v,v1,v2,a,a1) is PartFunc of V,(A \/ (NDSS (V,A)))
by A8, RELSET_1:4;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (ND_ex_4 (v,v1,v2,a,a1)) or x in A \/ (NDSS (V,A)) )

assume x in rng (ND_ex_4 (v,v1,v2,a,a1)) ; :: thesis: x in A \/ (NDSS (V,A))

end;assume x in rng (ND_ex_4 (v,v1,v2,a,a1)) ; :: thesis: x in A \/ (NDSS (V,A))

per cases then
( x = a or x = v2 .--> a1 )
by A9, TARSKI:def 2;

end;

suppose A10:
x = v2 .--> a1
; :: thesis: x in A \/ (NDSS (V,A))

A11:
dom (v2 .--> a1) c= V
by A1, A5, ZFMISC_1:31;

rng (v2 .--> a1) = {a1} by FUNCOP_1:8;

then rng (v2 .--> a1) c= A by A7, ZFMISC_1:31;

then v2 .--> a1 is PartFunc of V,A by A11, RELSET_1:4;

then v2 .--> a1 in NDSS (V,A) ;

hence x in A \/ (NDSS (V,A)) by A10, XBOOLE_0:def 3; :: thesis: verum

end;rng (v2 .--> a1) = {a1} by FUNCOP_1:8;

then rng (v2 .--> a1) c= A by A7, ZFMISC_1:31;

then v2 .--> a1 is PartFunc of V,A by A11, RELSET_1:4;

then v2 .--> a1 in NDSS (V,A) ;

hence x in A \/ (NDSS (V,A)) by A10, XBOOLE_0:def 3; :: thesis: verum

hence ND_ex_4 (v,v1,v2,a,a1) in NDSS (V,(A \/ (NDSS (V,A)))) ; :: thesis: verum