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