let X be non empty finite set ; :: thesis: for F being Dependency-set of X
for K being Subset of X holds
( K in candidate-keys (Dependency-closure F) iff K is_p_i_w_ncv_of F )
let F be Dependency-set of X; :: thesis: for K being Subset of X holds
( K in candidate-keys (Dependency-closure F) iff K is_p_i_w_ncv_of F )
let K be Subset of X; :: thesis: ( K in candidate-keys (Dependency-closure F) iff K is_p_i_w_ncv_of F )
set dcF = Dependency-closure F;
set S = { P where P is Subset of X : [K,P] in Dependency-closure F } ;
{ P where P is Subset of X : [K,P] in Dependency-closure F } c= bool X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { P where P is Subset of X : [K,P] in Dependency-closure F } or x in bool X )
assume x in { P where P is Subset of X : [K,P] in Dependency-closure F } ; :: thesis: x in bool X
then ex P being Subset of X st
( x = P & [K,P] in Dependency-closure F ) ;
hence x in bool X ; :: thesis: verum

end;

then reconsider S = { P where P is Subset of X : [K,P] in Dependency-closure F } as Subset-Family of X ;
set ck = candidate-keys (Dependency-closure F);
set B = { c where c is Subset of X : for x, y being Subset of X st [x,y] in F & x c= c holds
y c= c } ;
[K,K] in Dependency-closure F by Def11;
then K in S ;
then consider m being set such that
A1: m in S and
A2: for B being set st B in S & m c= B holds
B = m by FINSET_1:6;
{ c where c is Subset of X : for x, y being Subset of X st [x,y] in F & x c= c holds
y c= c } = enclosure_of F ;
then A3: Dependency-closure F = X deps_encl_by { c where c is Subset of X : for x, y being Subset of X st [x,y] in F & x c= c holds
y c= c } by Th38;

hereby :: thesis: ( K is_p_i_w_ncv_of F implies K in candidate-keys (Dependency-closure F) )

assume K in candidate-keys (Dependency-closure F) ; :: thesis: K is_p_i_w_ncv_of F
then consider A being Subset of X such that
A4: K = A and
A5: [A,X] in Maximal_wrt (Dependency-closure F) ;
A6: A ^|^ X, Dependency-closure F by A5;
[A,([#] X)] in Dependency-closure F by A5;
then consider a, b being Subset of X such that
A7: [A,X] = [a,b] and
A8: for c being set st c in { c where c is Subset of X : for x, y being Subset of X st [x,y] in F & x c= c holds
y c= c } & a c= c holds
b c= c by A3;
A9: X = b by A7, XTUPLE_0:1;
A10: A = a by A7, XTUPLE_0:1;
thus K is_p_i_w_ncv_of F :: thesis: verum

proof

hereby :: according to ARMSTRNG:def 32 :: thesis: for k being set st k c< K holds
ex a being Subset of X st
( k c= a & a <> X & not a in charact_set F )

let z be Subset of X; :: thesis: ( K c= z & z <> X implies z in charact_set F )
assume that
A11: K c= z and
A12: z <> X and
A13: not z in charact_set F ; :: thesis: contradiction
for x, y being Subset of X st [x,y] in F & x c= z holds
y c= z by A13;
then z in { c where c is Subset of X : for x, y being Subset of X st [x,y] in F & x c= c holds
y c= c } ;
then X c= z by A4, A8, A10, A9, A11;
hence contradiction by A12, XBOOLE_0:def 10; :: thesis: verum

end;

let k be set ; :: thesis: ( k c< K implies ex a being Subset of X st
( k c= a & a <> X & not a in charact_set F ) )
assume A14: k c< K ; :: thesis: ex a being Subset of X st
( k c= a & a <> X & not a in charact_set F )
then k c= A by A4, XBOOLE_0:def 8;
then reconsider k = k as Subset of X by XBOOLE_1:1;
set S = { P where P is Subset of X : [k,P] in Dependency-closure F } ;
{ P where P is Subset of X : [k,P] in Dependency-closure F } c= bool X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { P where P is Subset of X : [k,P] in Dependency-closure F } or x in bool X )
assume x in { P where P is Subset of X : [k,P] in Dependency-closure F } ; :: thesis: x in bool X
then ex P being Subset of X st
( x = P & [k,P] in Dependency-closure F ) ;
hence x in bool X ; :: thesis: verum

end;

then reconsider S = { P where P is Subset of X : [k,P] in Dependency-closure F } as Subset-Family of X ;
[k,k] in Dependency-closure F by Def11;
then k in S ;
then consider m being set such that
A15: m in S and
A16: for B being set st B in S & m c= B holds
B = m by FINSET_1:6;
consider P being Subset of X such that
A17: m = P and
A18: [k,P] in Dependency-closure F by A15;
[k,k] in Dependency-closure F by Def11;
then A19: [(k \/ k),(k \/ P)] in Dependency-closure F by A18, Def13;
assume A20: for a being Subset of X holds
( not k c= a or not a <> X or a in charact_set F ) ; :: thesis: contradiction
A21: [k,([#] X)] in Dependency-closure F

proof

per cases ( k \/ P = X or k \/ P <> X ) ;

suppose k \/ P = X ; :: thesis: [k,([#] X)] in Dependency-closure F

hence [k,([#] X)] in Dependency-closure F by A19; :: thesis: verum

end;

suppose k \/ P <> X ; :: thesis: [k,([#] X)] in Dependency-closure F

then k \/ P in charact_set F by A20, XBOOLE_1:7;
then k \/ P in charact_set (Dependency-closure F) by Th59;
then consider x, y being Subset of X such that
A22: [x,y] in Dependency-closure F and
A23: x c= k \/ P and
A24: not y c= k \/ P by Th55;
[(k \/ P),(k \/ P)] in Dependency-closure F by Def11;
then [(x \/ (k \/ P)),(y \/ (k \/ P))] in Dependency-closure F by A22, Def13;
then [(k \/ P),(y \/ (k \/ P))] in Dependency-closure F by A23, XBOOLE_1:12;
then [k,(y \/ (k \/ P))] in Dependency-closure F by A19, Th18;
then A25: y \/ (k \/ P) in S ;
P c= k \/ P by XBOOLE_1:7;
then P = y \/ (k \/ P) by A16, A17, A25, XBOOLE_1:10;
hence [k,([#] X)] in Dependency-closure F by A24, XBOOLE_1:7, XBOOLE_1:10; :: thesis: verum

end;

end;

end;

k c= K by A14, XBOOLE_0:def 8;
then [K,([#] X)] <= [k,([#] X)] ;
hence contradiction by A4, A6, A14, A21, Th27; :: thesis: verum

end;

end;

consider P being Subset of X such that
A26: m = P and
A27: [K,P] in Dependency-closure F by A1;
[K,K] in Dependency-closure F by Def11;
then A28: [(K \/ K),(K \/ P)] in Dependency-closure F by A27, Def13;
assume A29: K is_p_i_w_ncv_of F ; :: thesis: K in candidate-keys (Dependency-closure F)
A30: K c= K \/ P by XBOOLE_1:7;
A31: [K,([#] X)] in Dependency-closure F

proof

per cases ( K \/ P = X or K \/ P <> X ) ;

suppose K \/ P = X ; :: thesis: [K,([#] X)] in Dependency-closure F

hence [K,([#] X)] in Dependency-closure F by A28; :: thesis: verum

end;

suppose K \/ P <> X ; :: thesis: [K,([#] X)] in Dependency-closure F

then K \/ P in charact_set F by A29, A30;
then K \/ P in charact_set (Dependency-closure F) by Th59;
then consider x, y being Subset of X such that
A32: [x,y] in Dependency-closure F and
A33: x c= K \/ P and
A34: not y c= K \/ P by Th55;
[(K \/ P),(K \/ P)] in Dependency-closure F by Def11;
then [(x \/ (K \/ P)),(y \/ (K \/ P))] in Dependency-closure F by A32, Def13;
then [(K \/ P),(y \/ (K \/ P))] in Dependency-closure F by A33, XBOOLE_1:12;
then [K,(y \/ (K \/ P))] in Dependency-closure F by A28, Th18;
then A35: y \/ (K \/ P) in S ;
P c= K \/ P by XBOOLE_1:7;
then P = y \/ (K \/ P) by A2, A26, A35, XBOOLE_1:10;
hence [K,([#] X)] in Dependency-closure F by A34, XBOOLE_1:7, XBOOLE_1:10; :: thesis: verum

end;

end;

end;

now :: thesis: for x9, y9 being Subset of X st [x9,y9] in Dependency-closure F & ( K <> x9 or X <> y9 ) holds
not [K,([#] X)] <= [x9,y9]

let x9, y9 be Subset of X; :: thesis: ( [x9,y9] in Dependency-closure F & ( K <> x9 or X <> y9 ) implies not [K,([#] X)] <= [x9,y9] )
assume that
A36: [x9,y9] in Dependency-closure F and
A37: ( K <> x9 or X <> y9 ) and
A38: [K,([#] X)] <= [x9,y9] ; :: thesis: contradiction
A39: X c= y9 by A38;
x9 c= K by A38;
then x9 c< K by A37, A39, XBOOLE_0:def 8, XBOOLE_0:def 10;
then consider a being Subset of X such that
A40: x9 c= a and
A41: a <> X and
A42: not a in charact_set F by A29;
X = y9 by A39, XBOOLE_0:def 10;
then A43: not y9 c= a by A41, XBOOLE_0:def 10;
not a in charact_set (Dependency-closure F) by A42, Th59;
hence contradiction by A36, A40, A43; :: thesis: verum

end;

then K ^|^ X, Dependency-closure F by A31, Th27;
then [K,X] in Maximal_wrt (Dependency-closure F) ;
hence K in candidate-keys (Dependency-closure F) ; :: thesis: verum