let V, A be set ; for D being finite Function st dom D c= V & rng D c= ND (V,A) holds
D is NonatomicND of V,A
let D be finite Function; ( dom D c= V & rng D c= ND (V,A) implies D is NonatomicND of V,A )
assume that
A1:
dom D c= V
and
A2:
rng D c= ND (V,A)
; D is NonatomicND of V,A
defpred S1[ set ] means $1 is NonatomicND of V,A;
A3:
D is finite
;
A4:
S1[ {} ]
by NOMIN_1:30;
A5:
for x, B being set st x in D & B c= D & S1[B] holds
S1[B \/ {x}]
proof
let x,
B be
set ;
( x in D & B c= D & S1[B] implies S1[B \/ {x}] )
assume that A6:
x in D
and A7:
B c= D
;
( not S1[B] or S1[B \/ {x}] )
assume
S1[
B]
;
S1[B \/ {x}]
then reconsider B =
B as
NonatomicND of
V,
A ;
consider a,
b being
object such that A8:
x = [a,b]
by A6, RELAT_1:def 1;
A9:
a in dom D
by A6, A8, XTUPLE_0:def 12;
b in rng D
by A6, A8, XTUPLE_0:def 13;
then
b is
TypeSCNominativeData of
V,
A
by A2, NOMIN_1:39;
then A10:
{[a,b]} is
NonatomicND of
V,
A
by A1, A9, Th5;
{x} c= D
by A6, ZFMISC_1:31;
then
B \/ {[a,b]} is
Function
by A7, A8, GRFUNC_1:14;
hence
S1[
B \/ {x}]
by A8, A10, NOMIN_1:36, PARTFUN1:51;
verum
end;
S1[D]
from FINSET_1:sch 2(A3, A4, A5);
hence
D is NonatomicND of V,A
; verum