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 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 } ;
{ 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 A1: 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 Th40;

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
A2: K = A and
A3: [A,X] in Maximal_wrt (Dependency-closure F) ;
A4: A ^|^ X, Dependency-closure F by A3, Def18;
[A,([#] X)] in Dependency-closure F by A3;
then consider a, b being Subset of X such that
A5: [A,X] = [a,b] and
A6: 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 A1;
A7: ( A = a & X = b ) by A5, ZFMISC_1:33;
thus K is_p_i_w_ncv_of F :: thesis: verum

proof

hereby :: according to ARMSTRNG:def 33 :: 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
A8: K c= z and
A9: z <> X and
A10: 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 A10;
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 A2, A6, A7, A8;
hence contradiction by A9, 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 A11: 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 A2, XBOOLE_0:def 8;
then reconsider k = k as Subset of X by XBOOLE_1:1;
assume A12: for a being Subset of X holds
( not k c= a or not a <> X or a in charact_set F ) ; :: thesis: contradiction
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 set ; :: 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 Def12;
then k in S ;
then consider m being set such that
A13: m in S and
A14: for B being set st B in S & m c= B holds
B = m by FINSET_1:18;
consider P being Subset of X such that
A15: m = P and
A16: [k,P] in Dependency-closure F by A13;
[k,k] in Dependency-closure F by Def12;
then A17: [(k \/ k),(k \/ P)] in Dependency-closure F by A16, Def14;
A18: [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 A17; :: thesis: verum

end;

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

then k \/ P in charact_set F by A12, XBOOLE_1:7;
then k \/ P in charact_set (Dependency-closure F) by Th61;
then consider x, y being Subset of X such that
A19: [x,y] in Dependency-closure F and
A20: x c= k \/ P and
A21: not y c= k \/ P by Th57;
[(k \/ P),(k \/ P)] in Dependency-closure F by Def12;
then [(x \/ (k \/ P)),(y \/ (k \/ P))] in Dependency-closure F by A19, Def14;
then [(k \/ P),(y \/ (k \/ P))] in Dependency-closure F by A20, XBOOLE_1:12;
then [k,(y \/ (k \/ P))] in Dependency-closure F by A17, Th20;
then A22: y \/ (k \/ P) in S ;
P c= k \/ P by XBOOLE_1:7;
then P = y \/ (k \/ P) by A14, A15, A22, XBOOLE_1:10;
hence [k,([#] X)] in Dependency-closure F by A21, XBOOLE_1:7, XBOOLE_1:10; :: thesis: verum

end;

end;

end;

k c= K by A11, XBOOLE_0:def 8;
then [K,([#] X)] <= [k,([#] X)] by Th15;
hence contradiction by A2, A4, A11, A18, Th29; :: thesis: verum

end;

end;

assume A23: K is_p_i_w_ncv_of F ; :: thesis: K in candidate-keys (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 set ; :: 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 Def12;
then K in S ;
then consider m being set such that
A24: m in S and
A25: for B being set st B in S & m c= B holds
B = m by FINSET_1:18;
consider P being Subset of X such that
A26: m = P and
A27: [K,P] in Dependency-closure F by A24;
[K,K] in Dependency-closure F by Def12;
then A28: [(K \/ K),(K \/ P)] in Dependency-closure F by A27, Def14;
A29: K c= K \/ P by XBOOLE_1:7;
A30: [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 A23, A29, Def33;
then K \/ P in charact_set (Dependency-closure F) by Th61;
then consider x, y being Subset of X such that
A31: [x,y] in Dependency-closure F and
A32: x c= K \/ P and
A33: not y c= K \/ P by Th57;
[(K \/ P),(K \/ P)] in Dependency-closure F by Def12;
then [(x \/ (K \/ P)),(y \/ (K \/ P))] in Dependency-closure F by A31, Def14;
then [(K \/ P),(y \/ (K \/ P))] in Dependency-closure F by A32, XBOOLE_1:12;
then [K,(y \/ (K \/ P))] in Dependency-closure F by A28, Th20;
then A34: y \/ (K \/ P) in S ;
P c= K \/ P by XBOOLE_1:7;
then P = y \/ (K \/ P) by A25, A26, A34, XBOOLE_1:10;
hence [K,([#] X)] in Dependency-closure F by A33, XBOOLE_1:7, XBOOLE_1:10; :: thesis: verum

end;

end;

end;

now

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

end;

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