let X be finite set ; :: thesis: for F being Dependency-set of X
for K being Subset of X st F = { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } holds
{[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } = Maximal_wrt F
let F be Dependency-set of X; :: thesis: for K being Subset of X st F = { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } holds
{[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } = Maximal_wrt F
let K be Subset of X; :: thesis: ( F = { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } implies {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } = Maximal_wrt F )
set M = {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } ;
A1: {[K,X]} c= {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } by XBOOLE_1:7;
A2: now :: thesis: for A being Subset of X st not K c= A holds
[A,A] in {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A }
let A be Subset of X; :: thesis: ( not K c= A implies [A,A] in {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } )
assume not K c= A ; :: thesis: [A,A] in {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A }
then A3: [A,A] in { [a,a] where a is Subset of X : not K c= a } ;
{ [a,a] where a is Subset of X : not K c= a } c= {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } by XBOOLE_1:7;
hence [A,A] in {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } by A3; :: thesis: verum
end;
A4: [#] X = X ;
A5: {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } c= [:(bool X),(bool X):]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } or x in [:(bool X),(bool X):] )
assume A6: x in {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } ; :: thesis: x in [:(bool X),(bool X):]
per cases ( x in {[K,X]} or x in { [A,A] where A is Subset of X : not K c= A } ) by A6, XBOOLE_0:def 3;
suppose x in { [A,A] where A is Subset of X : not K c= A } ; :: thesis: x in [:(bool X),(bool X):]
then ex A being Subset of X st
( x = [A,A] & not K c= A ) ;
hence x in [:(bool X),(bool X):] ; :: thesis: verum
end;
end;
end;
A7: now :: thesis: for A, B being Subset of X holds
( not [A,B] in {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } or [A,B] = [K,X] or ( not K c= A & A = B ) )
let A, B be Subset of X; :: thesis: ( not [A,B] in {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } or [b1,b2] = [K,X] or ( not K c= b1 & b1 = b2 ) )
assume A8: [A,B] in {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } ; :: thesis: ( [b1,b2] = [K,X] or ( not K c= b1 & b1 = b2 ) )
per cases ( [A,B] in {[K,X]} or [A,B] in { [a,a] where a is Subset of X : not K c= a } ) by A8, XBOOLE_0:def 3;
suppose [A,B] in {[K,X]} ; :: thesis: ( [b1,b2] = [K,X] or ( not K c= b1 & b1 = b2 ) )
hence ( [A,B] = [K,X] or ( not K c= A & A = B ) ) by TARSKI:def 1; :: thesis: verum
end;
suppose [A,B] in { [a,a] where a is Subset of X : not K c= a } ; :: thesis: ( [b1,b2] = [K,X] or ( not K c= b1 & b1 = b2 ) )
then consider a being Subset of X such that
A9: [A,B] = [a,a] and
A10: not K c= a ;
A = a by A9, XTUPLE_0:1;
hence ( [A,B] = [K,X] or ( not K c= A & A = B ) ) by A9, A10, XTUPLE_0:1; :: thesis: verum
end;
end;
end;
reconsider M = {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } as Dependency-set of X by A5;
set FF = { [A,B] where A, B is Subset of X : ex A9, B9 being Subset of X st
( [A9,B9] >= [A,B] & [A9,B9] in M ) } ;
A11: { [A,B] where A, B is Subset of X : ex A9, B9 being Subset of X st
( [A9,B9] >= [A,B] & [A9,B9] in M ) } c= [:(bool X),(bool X):]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [A,B] where A, B is Subset of X : ex A9, B9 being Subset of X st
( [A9,B9] >= [A,B] & [A9,B9] in M ) } or x in [:(bool X),(bool X):] )
assume x in { [A,B] where A, B is Subset of X : ex A9, B9 being Subset of X st
( [A9,B9] >= [A,B] & [A9,B9] in M ) } ; :: thesis: x in [:(bool X),(bool X):]
then ex A, B being Subset of X st
( x = [A,B] & ex A9, B9 being Subset of X st
( [A9,B9] >= [A,B] & [A9,B9] in M ) ) ;
hence x in [:(bool X),(bool X):] ; :: thesis: verum
end;
A12: M is (M2)
proof
let A, B, A9, B9 be Subset of X; :: according to ARMSTRNG:def 19 :: thesis: ( [A,B] in M & [A9,B9] in M & [A,B] >= [A9,B9] implies ( A = A9 & B = B9 ) )
assume that
A13: [A,B] in M and
A14: [A9,B9] in M and
A15: [A,B] >= [A9,B9] ; :: thesis: ( A = A9 & B = B9 )
A16: A c= A9 by A15;
A17: B9 c= B by A15;
per cases ( [A,B] = [K,X] or ( not K c= A & A = B ) ) by A7, A13;
suppose A18: [A,B] = [K,X] ; :: thesis: ( A = A9 & B = B9 )
thus ( A = A9 & B = B9 ) :: thesis: verum
proof
per cases ( [A9,B9] = [K,X] or ( not K c= A9 & A9 = B9 ) ) by A7, A14;
suppose [A9,B9] = [K,X] ; :: thesis: ( A = A9 & B = B9 )
hence ( A = A9 & B = B9 ) by A18, XTUPLE_0:1; :: thesis: verum
end;
suppose ( not K c= A9 & A9 = B9 ) ; :: thesis: ( A = A9 & B = B9 )
hence ( A = A9 & B = B9 ) by A16, A18, XTUPLE_0:1; :: thesis: verum
end;
end;
end;
end;
suppose A19: ( not K c= A & A = B ) ; :: thesis: ( A = A9 & B = B9 )
thus ( A = A9 & B = B9 ) :: thesis: verum
proof
per cases ( [A9,B9] = [K,X] or ( not K c= A9 & A9 = B9 ) ) by A7, A14;
suppose [A9,B9] = [K,X] ; :: thesis: ( A = A9 & B = B9 )
then B9 = X by XTUPLE_0:1;
then B = X by A17, XBOOLE_0:def 10;
hence ( A = A9 & B = B9 ) by A19; :: thesis: verum
end;
suppose ( not K c= A9 & A9 = B9 ) ; :: thesis: ( A = A9 & B = B9 )
hence ( A = A9 & B = B9 ) by A16, A17, A19, XBOOLE_0:def 10; :: thesis: verum
end;
end;
end;
end;
end;
end;
reconsider FF = { [A,B] where A, B is Subset of X : ex A9, B9 being Subset of X st
( [A9,B9] >= [A,B] & [A9,B9] in M ) } as Dependency-set of X by A11;
assume A20: F = { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } ; :: thesis: {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } = Maximal_wrt F
A21: now :: thesis: for x being object holds
( ( x in F implies x in FF ) & ( x in FF implies x in F ) )
let x be object ; :: thesis: ( ( x in F implies x in FF ) & ( x in FF implies b1 in F ) )
hereby :: thesis: ( x in FF implies b1 in F )
A22: { [a,a] where a is Subset of X : not K c= a } c= M by XBOOLE_1:7;
A23: [K,X] in {[K,X]} by TARSKI:def 1;
A24: {[K,X]} c= M by XBOOLE_1:7;
assume x in F ; :: thesis: x in FF
then consider A, B being Subset of X such that
A25: x = [A,B] and
A26: ( K c= A or B c= A ) by A20;
per cases ( K c= A or not K c= A ) ;
suppose K c= A ; :: thesis: x in FF
then [K,([#] X)] >= [A,B] ;
hence x in FF by A25, A24, A23; :: thesis: verum
end;
suppose A27: not K c= A ; :: thesis: x in FF
then A28: [A,A] in { [a,a] where a is Subset of X : not K c= a } ;
[A,A] >= [A,B] by A26, A27;
hence x in FF by A25, A22, A28; :: thesis: verum
end;
end;
end;
assume x in FF ; :: thesis: b1 in F
then consider A, B being Subset of X such that
A29: x = [A,B] and
A30: ex A9, B9 being Subset of X st
( [A9,B9] >= [A,B] & [A9,B9] in M ) ;
consider A9, B9 being Subset of X such that
A31: [A9,B9] >= [A,B] and
A32: [A9,B9] in M by A30;
per cases ( [A9,B9] in {[K,X]} or [A9,B9] in { [a,a] where a is Subset of X : not K c= a } ) by A32, XBOOLE_0:def 3;
suppose [A9,B9] in {[K,X]} ; :: thesis: b1 in F
then [A9,B9] = [K,X] by TARSKI:def 1;
then A9 = K by XTUPLE_0:1;
then K c= A by A31;
hence x in F by A20, A29; :: thesis: verum
end;
suppose [A9,B9] in { [a,a] where a is Subset of X : not K c= a } ; :: thesis: b1 in F
then consider a being Subset of X such that
A33: [A9,B9] = [a,a] and
not K c= a ;
A34: A9 = a by A33, XTUPLE_0:1;
A35: B9 = a by A33, XTUPLE_0:1;
A36: B c= B9 by A31;
A9 c= A by A31;
then B c= A by A34, A35, A36;
hence x in F by A20, A29; :: thesis: verum
end;
end;
end;
A37: M is (M3)
proof
let A, B, A9, B9 be Subset of X; :: according to ARMSTRNG:def 20 :: thesis: ( [A,B] in M & [A9,B9] in M & A9 c= B implies B9 c= B )
assume that
A38: [A,B] in M and
A39: [A9,B9] in M and
A40: A9 c= B ; :: thesis: B9 c= B
per cases ( [A,B] = [K,X] or ( not K c= A & A = B ) ) by A7, A38;
suppose A41: ( not K c= A & A = B ) ; :: thesis: B9 c= B
thus B9 c= B :: thesis: verum
proof
per cases ( [A9,B9] = [K,X] or ( not K c= A9 & A9 = B9 ) ) by A7, A39;
suppose [A9,B9] = [K,X] ; :: thesis: B9 c= B
hence B9 c= B by A40, A41, XTUPLE_0:1; :: thesis: verum
end;
suppose ( not K c= A9 & A9 = B9 ) ; :: thesis: B9 c= B
hence B9 c= B by A40; :: thesis: verum
end;
end;
end;
end;
end;
end;
A42: [K,X] in {[K,X]} by TARSKI:def 1;
M is (M1)
proof
let A be Subset of X; :: according to ARMSTRNG:def 18 :: thesis: ex A9, B9 being Subset of X st
( [A9,B9] >= [A,A] & [A9,B9] in M )
per cases ( K c= A or not K c= A ) ;
suppose A43: K c= A ; :: thesis: ex A9, B9 being Subset of X st
( [A9,B9] >= [A,A] & [A9,B9] in M )
take A9 = K; :: thesis: ex B9 being Subset of X st
( [A9,B9] >= [A,A] & [A9,B9] in M )
take B9 = [#] X; :: thesis: ( [A9,B9] >= [A,A] & [A9,B9] in M )
thus [A9,B9] >= [A,A] by A43; :: thesis: [A9,B9] in M
thus [A9,B9] in M by A42, A1; :: thesis: verum
end;
suppose A44: not K c= A ; :: thesis: ex A9, B9 being Subset of X st
( [A9,B9] >= [A,A] & [A9,B9] in M )
take A9 = A; :: thesis: ex B9 being Subset of X st
( [A9,B9] >= [A,A] & [A9,B9] in M )
take B9 = A; :: thesis: ( [A9,B9] >= [A,A] & [A9,B9] in M )
thus [A9,B9] >= [A,A] ; :: thesis: [A9,B9] in M
thus [A9,B9] in M by A2, A44; :: thesis: verum
end;
end;
end;
then M = Maximal_wrt FF by A12, A37, Th29;
hence {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } = Maximal_wrt F by A21, TARSKI:2; :: thesis: verum