:: BVFUNC_1 semantic presentation
begin
definition
let k, l be boolean set ;
redefine pred k <= l means :Def1: :: BVFUNC_1:def 1
k => l = TRUE ;
compatibility
( k <= l iff k => l = TRUE )
proof
A1: ( l = 0 or l = 1 ) by XBOOLEAN:def_3;
( k = 0 or k = 1 ) by XBOOLEAN:def_3;
hence ( k <= l iff k => l = TRUE ) by A1; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines <= BVFUNC_1:def_1_:_
for k, l being boolean set holds
( k <= l iff k => l = TRUE );
begin
scheme :: BVFUNC_1:sch 1
BVFUniq1{ F1() -> non empty set , F2( set ) -> set } :
for f1, f2 being Function of F1(),BOOLEAN st ( for x being Element of F1() holds f1 . x = F2(x) ) & ( for x being Element of F1() holds f2 . x = F2(x) ) holds
f1 = f2
proof
let f1, f2 be Function of F1(),BOOLEAN; ::_thesis: ( ( for x being Element of F1() holds f1 . x = F2(x) ) & ( for x being Element of F1() holds f2 . x = F2(x) ) implies f1 = f2 )
assume that
A1: for x being Element of F1() holds f1 . x = F2(x) and
A2: for x being Element of F1() holds f2 . x = F2(x) ; ::_thesis: f1 = f2
let u be Element of F1(); :: according to FUNCT_2:def_8 ::_thesis: f1 . u = f2 . u
thus f2 . u = F2(u) by A2
.= f1 . u by A1 ; ::_thesis: verum
end;
definition
let Y be non empty set ;
let a be Function of Y,BOOLEAN;
:: original: 'not'
redefine func 'not' a -> Function of Y,BOOLEAN;
coherence
'not' a is Function of Y,BOOLEAN
proof
reconsider a = a as Function of Y,BOOLEAN ;
'not' a is Function of Y,BOOLEAN ;
hence 'not' a is Function of Y,BOOLEAN ; ::_thesis: verum
end;
let b be Function of Y,BOOLEAN;
:: original: '&'
redefine funca '&' b -> Function of Y,BOOLEAN;
coherence
a '&' b is Function of Y,BOOLEAN
proof
reconsider a = a, b = b as Function of Y,BOOLEAN ;
a '&' b is Function of Y,BOOLEAN ;
hence a '&' b is Function of Y,BOOLEAN ; ::_thesis: verum
end;
end;
definition
let p, q be boolean-valued Function;
funcp 'or' q -> boolean-valued Function means :Def2: :: BVFUNC_1:def 2
( dom it = (dom p) /\ (dom q) & ( for x being set st x in dom it holds
it . x = (p . x) 'or' (q . x) ) );
existence
ex b1 being boolean-valued Function st
( dom b1 = (dom p) /\ (dom q) & ( for x being set st x in dom b1 holds
b1 . x = (p . x) 'or' (q . x) ) )
proof
deffunc H1( set ) -> set = (p . $1) 'or' (q . $1);
consider s being Function such that
A1: ( dom s = (dom p) /\ (dom q) & ( for x being set st x in (dom p) /\ (dom q) holds
s . x = H1(x) ) ) from FUNCT_1:sch_3();
s is boolean-valued
proof
let x be set ; :: according to TARSKI:def_3,MARGREL1:def_16 ::_thesis: ( not x in rng s or x in BOOLEAN )
assume x in rng s ; ::_thesis: x in BOOLEAN
then consider y being set such that
A2: ( y in dom s & x = s . y ) by FUNCT_1:def_3;
x = (p . y) 'or' (q . y) by A1, A2;
then ( x = FALSE or x = TRUE ) by XBOOLEAN:def_3;
hence x in BOOLEAN ; ::_thesis: verum
end;
hence ex b1 being boolean-valued Function st
( dom b1 = (dom p) /\ (dom q) & ( for x being set st x in dom b1 holds
b1 . x = (p . x) 'or' (q . x) ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being boolean-valued Function st dom b1 = (dom p) /\ (dom q) & ( for x being set st x in dom b1 holds
b1 . x = (p . x) 'or' (q . x) ) & dom b2 = (dom p) /\ (dom q) & ( for x being set st x in dom b2 holds
b2 . x = (p . x) 'or' (q . x) ) holds
b1 = b2
proof
let s1, s2 be boolean-valued Function; ::_thesis: ( dom s1 = (dom p) /\ (dom q) & ( for x being set st x in dom s1 holds
s1 . x = (p . x) 'or' (q . x) ) & dom s2 = (dom p) /\ (dom q) & ( for x being set st x in dom s2 holds
s2 . x = (p . x) 'or' (q . x) ) implies s1 = s2 )
assume that
A3: dom s1 = (dom p) /\ (dom q) and
A4: for x being set st x in dom s1 holds
s1 . x = (p . x) 'or' (q . x) and
A5: dom s2 = (dom p) /\ (dom q) and
A6: for x being set st x in dom s2 holds
s2 . x = (p . x) 'or' (q . x) ; ::_thesis: s1 = s2
for x being set st x in dom s1 holds
s1 . x = s2 . x
proof
let x be set ; ::_thesis: ( x in dom s1 implies s1 . x = s2 . x )
assume A7: x in dom s1 ; ::_thesis: s1 . x = s2 . x
then s1 . x = (p . x) 'or' (q . x) by A4;
hence s1 . x = s2 . x by A3, A5, A6, A7; ::_thesis: verum
end;
hence s1 = s2 by A3, A5, FUNCT_1:2; ::_thesis: verum
end;
commutativity
for b1, p, q being boolean-valued Function st dom b1 = (dom p) /\ (dom q) & ( for x being set st x in dom b1 holds
b1 . x = (p . x) 'or' (q . x) ) holds
( dom b1 = (dom q) /\ (dom p) & ( for x being set st x in dom b1 holds
b1 . x = (q . x) 'or' (p . x) ) ) ;
idempotence
for p being boolean-valued Function holds
( dom p = (dom p) /\ (dom p) & ( for x being set st x in dom p holds
p . x = (p . x) 'or' (p . x) ) ) ;
funcp 'xor' q -> Function means :Def3: :: BVFUNC_1:def 3
( dom it = (dom p) /\ (dom q) & ( for x being set st x in dom it holds
it . x = (p . x) 'xor' (q . x) ) );
existence
ex b1 being Function st
( dom b1 = (dom p) /\ (dom q) & ( for x being set st x in dom b1 holds
b1 . x = (p . x) 'xor' (q . x) ) )
proof
deffunc H1( set ) -> set = (p . $1) 'xor' (q . $1);
consider s being Function such that
A8: ( dom s = (dom p) /\ (dom q) & ( for x being set st x in (dom p) /\ (dom q) holds
s . x = H1(x) ) ) from FUNCT_1:sch_3();
take s ; ::_thesis: ( dom s = (dom p) /\ (dom q) & ( for x being set st x in dom s holds
s . x = (p . x) 'xor' (q . x) ) )
thus ( dom s = (dom p) /\ (dom q) & ( for x being set st x in dom s holds
s . x = (p . x) 'xor' (q . x) ) ) by A8; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function st dom b1 = (dom p) /\ (dom q) & ( for x being set st x in dom b1 holds
b1 . x = (p . x) 'xor' (q . x) ) & dom b2 = (dom p) /\ (dom q) & ( for x being set st x in dom b2 holds
b2 . x = (p . x) 'xor' (q . x) ) holds
b1 = b2
proof
let s1, s2 be Function; ::_thesis: ( dom s1 = (dom p) /\ (dom q) & ( for x being set st x in dom s1 holds
s1 . x = (p . x) 'xor' (q . x) ) & dom s2 = (dom p) /\ (dom q) & ( for x being set st x in dom s2 holds
s2 . x = (p . x) 'xor' (q . x) ) implies s1 = s2 )
assume that
A9: dom s1 = (dom p) /\ (dom q) and
A10: for x being set st x in dom s1 holds
s1 . x = (p . x) 'xor' (q . x) and
A11: dom s2 = (dom p) /\ (dom q) and
A12: for x being set st x in dom s2 holds
s2 . x = (p . x) 'xor' (q . x) ; ::_thesis: s1 = s2
for x being set st x in dom s1 holds
s1 . x = s2 . x
proof
let x be set ; ::_thesis: ( x in dom s1 implies s1 . x = s2 . x )
assume A13: x in dom s1 ; ::_thesis: s1 . x = s2 . x
then s1 . x = (p . x) 'xor' (q . x) by A10;
hence s1 . x = s2 . x by A9, A11, A12, A13; ::_thesis: verum
end;
hence s1 = s2 by A9, A11, FUNCT_1:2; ::_thesis: verum
end;
commutativity
for b1 being Function
for p, q being boolean-valued Function st dom b1 = (dom p) /\ (dom q) & ( for x being set st x in dom b1 holds
b1 . x = (p . x) 'xor' (q . x) ) holds
( dom b1 = (dom q) /\ (dom p) & ( for x being set st x in dom b1 holds
b1 . x = (q . x) 'xor' (p . x) ) ) ;
end;
:: deftheorem Def2 defines 'or' BVFUNC_1:def_2_:_
for p, q, b3 being boolean-valued Function holds
( b3 = p 'or' q iff ( dom b3 = (dom p) /\ (dom q) & ( for x being set st x in dom b3 holds
b3 . x = (p . x) 'or' (q . x) ) ) );
:: deftheorem Def3 defines 'xor' BVFUNC_1:def_3_:_
for p, q being boolean-valued Function
for b3 being Function holds
( b3 = p 'xor' q iff ( dom b3 = (dom p) /\ (dom q) & ( for x being set st x in dom b3 holds
b3 . x = (p . x) 'xor' (q . x) ) ) );
registration
let p, q be boolean-valued Function;
clusterp 'xor' q -> boolean-valued ;
coherence
p 'xor' q is boolean-valued
proof
let x be set ; :: according to TARSKI:def_3,MARGREL1:def_16 ::_thesis: ( not x in rng (p 'xor' q) or x in BOOLEAN )
assume x in rng (p 'xor' q) ; ::_thesis: x in BOOLEAN
then consider y being set such that
A1: ( y in dom (p 'xor' q) & x = (p 'xor' q) . y ) by FUNCT_1:def_3;
x = (p . y) 'xor' (q . y) by A1, Def3;
then ( x = FALSE or x = TRUE ) by XBOOLEAN:def_3;
hence x in BOOLEAN ; ::_thesis: verum
end;
end;
definition
let A be non empty set ;
let p, q be Function of A,BOOLEAN;
:: original: 'or'
redefine funcp 'or' q -> Function of A,BOOLEAN means :Def4: :: BVFUNC_1:def 4
for x being Element of A holds it . x = (p . x) 'or' (q . x);
coherence
p 'or' q is Function of A,BOOLEAN
proof
( dom p = A & dom q = A ) by PARTFUN1:def_2;
then A1: dom (p 'or' q) = A /\ A by Def2
.= A ;
rng (p 'or' q) c= BOOLEAN by MARGREL1:def_16;
hence p 'or' q is Function of A,BOOLEAN by A1, FUNCT_2:2; ::_thesis: verum
end;
compatibility
for b1 being Function of A,BOOLEAN holds
( b1 = p 'or' q iff for x being Element of A holds b1 . x = (p . x) 'or' (q . x) )
proof
let IT be Function of A,BOOLEAN; ::_thesis: ( IT = p 'or' q iff for x being Element of A holds IT . x = (p . x) 'or' (q . x) )
A2: dom IT = A by FUNCT_2:def_1;
hereby ::_thesis: ( ( for x being Element of A holds IT . x = (p . x) 'or' (q . x) ) implies IT = p 'or' q )
assume A3: IT = p 'or' q ; ::_thesis: for x being Element of A holds IT . x = (p . x) 'or' (q . x)
let x be Element of A; ::_thesis: IT . x = (p . x) 'or' (q . x)
( dom p = A & dom q = A ) by FUNCT_2:def_1;
then dom (p 'or' q) = A /\ A by Def2
.= A ;
hence IT . x = (p . x) 'or' (q . x) by A3, Def2; ::_thesis: verum
end;
A4: dom q = A by FUNCT_2:def_1;
A5: dom IT = A /\ A by FUNCT_2:def_1
.= (dom p) /\ (dom q) by A4, FUNCT_2:def_1 ;
assume for x being Element of A holds IT . x = (p . x) 'or' (q . x) ; ::_thesis: IT = p 'or' q
then for x being set st x in dom IT holds
IT . x = (p . x) 'or' (q . x) by A2;
hence IT = p 'or' q by A5, Def2; ::_thesis: verum
end;
:: original: 'xor'
redefine funcp 'xor' q -> Function of A,BOOLEAN means :: BVFUNC_1:def 5
for x being Element of A holds it . x = (p . x) 'xor' (q . x);
coherence
p 'xor' q is Function of A,BOOLEAN
proof
( dom p = A & dom q = A ) by PARTFUN1:def_2;
then A6: dom (p 'xor' q) = A /\ A by Def3
.= A ;
rng (p 'xor' q) c= BOOLEAN by MARGREL1:def_16;
hence p 'xor' q is Function of A,BOOLEAN by A6, FUNCT_2:2; ::_thesis: verum
end;
compatibility
for b1 being Function of A,BOOLEAN holds
( b1 = p 'xor' q iff for x being Element of A holds b1 . x = (p . x) 'xor' (q . x) )
proof
let IT be Function of A,BOOLEAN; ::_thesis: ( IT = p 'xor' q iff for x being Element of A holds IT . x = (p . x) 'xor' (q . x) )
A7: dom IT = A by FUNCT_2:def_1;
hereby ::_thesis: ( ( for x being Element of A holds IT . x = (p . x) 'xor' (q . x) ) implies IT = p 'xor' q )
assume A8: IT = p 'xor' q ; ::_thesis: for x being Element of A holds IT . x = (p . x) 'xor' (q . x)
let x be Element of A; ::_thesis: IT . x = (p . x) 'xor' (q . x)
( dom p = A & dom q = A ) by FUNCT_2:def_1;
then dom (p 'xor' q) = A /\ A by Def3
.= A ;
hence IT . x = (p . x) 'xor' (q . x) by A8, Def3; ::_thesis: verum
end;
A9: dom q = A by FUNCT_2:def_1;
A10: dom IT = A /\ A by FUNCT_2:def_1
.= (dom p) /\ (dom q) by A9, FUNCT_2:def_1 ;
assume for x being Element of A holds IT . x = (p . x) 'xor' (q . x) ; ::_thesis: IT = p 'xor' q
then for x being set st x in dom IT holds
IT . x = (p . x) 'xor' (q . x) by A7;
hence IT = p 'xor' q by A10, Def3; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines 'or' BVFUNC_1:def_4_:_
for A being non empty set
for p, q, b4 being Function of A,BOOLEAN holds
( b4 = p 'or' q iff for x being Element of A holds b4 . x = (p . x) 'or' (q . x) );
:: deftheorem defines 'xor' BVFUNC_1:def_5_:_
for A being non empty set
for p, q, b4 being Function of A,BOOLEAN holds
( b4 = p 'xor' q iff for x being Element of A holds b4 . x = (p . x) 'xor' (q . x) );
definition
let p, q be boolean-valued Function;
funcp 'imp' q -> Function means :Def6: :: BVFUNC_1:def 6
( dom it = (dom p) /\ (dom q) & ( for x being set st x in dom it holds
it . x = (p . x) => (q . x) ) );
existence
ex b1 being Function st
( dom b1 = (dom p) /\ (dom q) & ( for x being set st x in dom b1 holds
b1 . x = (p . x) => (q . x) ) )
proof
deffunc H1( set ) -> set = (p . $1) => (q . $1);
consider s being Function such that
A1: ( dom s = (dom p) /\ (dom q) & ( for x being set st x in (dom p) /\ (dom q) holds
s . x = H1(x) ) ) from FUNCT_1:sch_3();
take s ; ::_thesis: ( dom s = (dom p) /\ (dom q) & ( for x being set st x in dom s holds
s . x = (p . x) => (q . x) ) )
thus ( dom s = (dom p) /\ (dom q) & ( for x being set st x in dom s holds
s . x = (p . x) => (q . x) ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function st dom b1 = (dom p) /\ (dom q) & ( for x being set st x in dom b1 holds
b1 . x = (p . x) => (q . x) ) & dom b2 = (dom p) /\ (dom q) & ( for x being set st x in dom b2 holds
b2 . x = (p . x) => (q . x) ) holds
b1 = b2
proof
let s1, s2 be Function; ::_thesis: ( dom s1 = (dom p) /\ (dom q) & ( for x being set st x in dom s1 holds
s1 . x = (p . x) => (q . x) ) & dom s2 = (dom p) /\ (dom q) & ( for x being set st x in dom s2 holds
s2 . x = (p . x) => (q . x) ) implies s1 = s2 )
assume that
A2: dom s1 = (dom p) /\ (dom q) and
A3: for x being set st x in dom s1 holds
s1 . x = (p . x) => (q . x) and
A4: dom s2 = (dom p) /\ (dom q) and
A5: for x being set st x in dom s2 holds
s2 . x = (p . x) => (q . x) ; ::_thesis: s1 = s2
for x being set st x in dom s1 holds
s1 . x = s2 . x
proof
let x be set ; ::_thesis: ( x in dom s1 implies s1 . x = s2 . x )
assume A6: x in dom s1 ; ::_thesis: s1 . x = s2 . x
then s1 . x = (p . x) => (q . x) by A3;
hence s1 . x = s2 . x by A2, A4, A5, A6; ::_thesis: verum
end;
hence s1 = s2 by A2, A4, FUNCT_1:2; ::_thesis: verum
end;
funcp 'eqv' q -> Function means :Def7: :: BVFUNC_1:def 7
( dom it = (dom p) /\ (dom q) & ( for x being set st x in dom it holds
it . x = (p . x) <=> (q . x) ) );
existence
ex b1 being Function st
( dom b1 = (dom p) /\ (dom q) & ( for x being set st x in dom b1 holds
b1 . x = (p . x) <=> (q . x) ) )
proof
deffunc H1( set ) -> set = (p . $1) <=> (q . $1);
consider s being Function such that
A7: ( dom s = (dom p) /\ (dom q) & ( for x being set st x in (dom p) /\ (dom q) holds
s . x = H1(x) ) ) from FUNCT_1:sch_3();
take s ; ::_thesis: ( dom s = (dom p) /\ (dom q) & ( for x being set st x in dom s holds
s . x = (p . x) <=> (q . x) ) )
thus ( dom s = (dom p) /\ (dom q) & ( for x being set st x in dom s holds
s . x = (p . x) <=> (q . x) ) ) by A7; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function st dom b1 = (dom p) /\ (dom q) & ( for x being set st x in dom b1 holds
b1 . x = (p . x) <=> (q . x) ) & dom b2 = (dom p) /\ (dom q) & ( for x being set st x in dom b2 holds
b2 . x = (p . x) <=> (q . x) ) holds
b1 = b2
proof
let s1, s2 be Function; ::_thesis: ( dom s1 = (dom p) /\ (dom q) & ( for x being set st x in dom s1 holds
s1 . x = (p . x) <=> (q . x) ) & dom s2 = (dom p) /\ (dom q) & ( for x being set st x in dom s2 holds
s2 . x = (p . x) <=> (q . x) ) implies s1 = s2 )
assume that
A8: dom s1 = (dom p) /\ (dom q) and
A9: for x being set st x in dom s1 holds
s1 . x = (p . x) <=> (q . x) and
A10: dom s2 = (dom p) /\ (dom q) and
A11: for x being set st x in dom s2 holds
s2 . x = (p . x) <=> (q . x) ; ::_thesis: s1 = s2
for x being set st x in dom s1 holds
s1 . x = s2 . x
proof
let x be set ; ::_thesis: ( x in dom s1 implies s1 . x = s2 . x )
assume A12: x in dom s1 ; ::_thesis: s1 . x = s2 . x
then s1 . x = (p . x) <=> (q . x) by A9;
hence s1 . x = s2 . x by A8, A10, A11, A12; ::_thesis: verum
end;
hence s1 = s2 by A8, A10, FUNCT_1:2; ::_thesis: verum
end;
commutativity
for b1 being Function
for p, q being boolean-valued Function st dom b1 = (dom p) /\ (dom q) & ( for x being set st x in dom b1 holds
b1 . x = (p . x) <=> (q . x) ) holds
( dom b1 = (dom q) /\ (dom p) & ( for x being set st x in dom b1 holds
b1 . x = (q . x) <=> (p . x) ) ) ;
end;
:: deftheorem Def6 defines 'imp' BVFUNC_1:def_6_:_
for p, q being boolean-valued Function
for b3 being Function holds
( b3 = p 'imp' q iff ( dom b3 = (dom p) /\ (dom q) & ( for x being set st x in dom b3 holds
b3 . x = (p . x) => (q . x) ) ) );
:: deftheorem Def7 defines 'eqv' BVFUNC_1:def_7_:_
for p, q being boolean-valued Function
for b3 being Function holds
( b3 = p 'eqv' q iff ( dom b3 = (dom p) /\ (dom q) & ( for x being set st x in dom b3 holds
b3 . x = (p . x) <=> (q . x) ) ) );
registration
let p, q be boolean-valued Function;
clusterp 'imp' q -> boolean-valued ;
coherence
p 'imp' q is boolean-valued
proof
let x be set ; :: according to TARSKI:def_3,MARGREL1:def_16 ::_thesis: ( not x in rng (p 'imp' q) or x in BOOLEAN )
assume x in rng (p 'imp' q) ; ::_thesis: x in BOOLEAN
then consider y being set such that
A1: ( y in dom (p 'imp' q) & x = (p 'imp' q) . y ) by FUNCT_1:def_3;
x = (p . y) => (q . y) by A1, Def6
.= ('not' (p . y)) 'or' (q . y) ;
then ( x = FALSE or x = TRUE ) by XBOOLEAN:def_3;
hence x in BOOLEAN ; ::_thesis: verum
end;
clusterp 'eqv' q -> boolean-valued ;
coherence
p 'eqv' q is boolean-valued
proof
let x be set ; :: according to TARSKI:def_3,MARGREL1:def_16 ::_thesis: ( not x in rng (p 'eqv' q) or x in BOOLEAN )
assume x in rng (p 'eqv' q) ; ::_thesis: x in BOOLEAN
then consider y being set such that
A2: ( y in dom (p 'eqv' q) & x = (p 'eqv' q) . y ) by FUNCT_1:def_3;
x = 'not' ((p . y) 'xor' (q . y)) by A2, Def7;
then ( x = FALSE or x = TRUE ) by XBOOLEAN:def_3;
hence x in BOOLEAN ; ::_thesis: verum
end;
end;
definition
let A be non empty set ;
let p, q be Function of A,BOOLEAN;
:: original: 'imp'
redefine funcp 'imp' q -> Function of A,BOOLEAN means :Def8: :: BVFUNC_1:def 8
for x being Element of A holds it . x = ('not' (p . x)) 'or' (q . x);
coherence
p 'imp' q is Function of A,BOOLEAN
proof
( dom p = A & dom q = A ) by PARTFUN1:def_2;
then A1: dom (p 'imp' q) = A /\ A by Def6
.= A ;
rng (p 'imp' q) c= BOOLEAN by MARGREL1:def_16;
hence p 'imp' q is Function of A,BOOLEAN by A1, FUNCT_2:2; ::_thesis: verum
end;
compatibility
for b1 being Function of A,BOOLEAN holds
( b1 = p 'imp' q iff for x being Element of A holds b1 . x = ('not' (p . x)) 'or' (q . x) )
proof
let IT be Function of A,BOOLEAN; ::_thesis: ( IT = p 'imp' q iff for x being Element of A holds IT . x = ('not' (p . x)) 'or' (q . x) )
A2: dom q = A by FUNCT_2:def_1;
hereby ::_thesis: ( ( for x being Element of A holds IT . x = ('not' (p . x)) 'or' (q . x) ) implies IT = p 'imp' q )
assume A3: IT = p 'imp' q ; ::_thesis: for x being Element of A holds IT . x = ('not' (p . x)) 'or' (q . x)
let x be Element of A; ::_thesis: IT . x = ('not' (p . x)) 'or' (q . x)
( dom p = A & dom q = A ) by FUNCT_2:def_1;
then dom (p 'imp' q) = A /\ A by Def6
.= A ;
hence IT . x = (p . x) => (q . x) by A3, Def6
.= ('not' (p . x)) 'or' (q . x) ;
::_thesis: verum
end;
assume A4: for x being Element of A holds IT . x = ('not' (p . x)) 'or' (q . x) ; ::_thesis: IT = p 'imp' q
A5: for x being set st x in dom IT holds
IT . x = (p . x) => (q . x)
proof
let x be set ; ::_thesis: ( x in dom IT implies IT . x = (p . x) => (q . x) )
assume x in dom IT ; ::_thesis: IT . x = (p . x) => (q . x)
then reconsider x = x as Element of A by FUNCT_2:def_1;
IT . x = ('not' (p . x)) 'or' (q . x) by A4;
hence IT . x = (p . x) => (q . x) ; ::_thesis: verum
end;
dom IT = A /\ A by FUNCT_2:def_1
.= (dom p) /\ (dom q) by A2, FUNCT_2:def_1 ;
hence IT = p 'imp' q by A5, Def6; ::_thesis: verum
end;
:: original: 'eqv'
redefine funcp 'eqv' q -> Function of A,BOOLEAN means :Def9: :: BVFUNC_1:def 9
for x being Element of A holds it . x = 'not' ((p . x) 'xor' (q . x));
coherence
p 'eqv' q is Function of A,BOOLEAN
proof
( dom p = A & dom q = A ) by PARTFUN1:def_2;
then A6: dom (p 'eqv' q) = A /\ A by Def7
.= A ;
rng (p 'eqv' q) c= BOOLEAN by MARGREL1:def_16;
hence p 'eqv' q is Function of A,BOOLEAN by A6, FUNCT_2:2; ::_thesis: verum
end;
compatibility
for b1 being Function of A,BOOLEAN holds
( b1 = p 'eqv' q iff for x being Element of A holds b1 . x = 'not' ((p . x) 'xor' (q . x)) )
proof
let IT be Function of A,BOOLEAN; ::_thesis: ( IT = p 'eqv' q iff for x being Element of A holds IT . x = 'not' ((p . x) 'xor' (q . x)) )
A7: dom q = A by FUNCT_2:def_1;
hereby ::_thesis: ( ( for x being Element of A holds IT . x = 'not' ((p . x) 'xor' (q . x)) ) implies IT = p 'eqv' q )
assume A8: IT = p 'eqv' q ; ::_thesis: for x being Element of A holds IT . x = 'not' ((p . x) 'xor' (q . x))
let x be Element of A; ::_thesis: IT . x = 'not' ((p . x) 'xor' (q . x))
( dom p = A & dom q = A ) by FUNCT_2:def_1;
then dom (p 'eqv' q) = A /\ A by Def7
.= A ;
hence IT . x = 'not' ((p . x) 'xor' (q . x)) by A8, Def7; ::_thesis: verum
end;
assume A9: for x being Element of A holds IT . x = 'not' ((p . x) 'xor' (q . x)) ; ::_thesis: IT = p 'eqv' q
A10: for x being set st x in dom IT holds
IT . x = (p . x) <=> (q . x)
proof
let x be set ; ::_thesis: ( x in dom IT implies IT . x = (p . x) <=> (q . x) )
assume x in dom IT ; ::_thesis: IT . x = (p . x) <=> (q . x)
then reconsider x = x as Element of A by FUNCT_2:def_1;
IT . x = 'not' ((p . x) 'xor' (q . x)) by A9;
hence IT . x = (p . x) <=> (q . x) ; ::_thesis: verum
end;
dom IT = A /\ A by FUNCT_2:def_1
.= (dom p) /\ (dom q) by A7, FUNCT_2:def_1 ;
hence IT = p 'eqv' q by A10, Def7; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines 'imp' BVFUNC_1:def_8_:_
for A being non empty set
for p, q, b4 being Function of A,BOOLEAN holds
( b4 = p 'imp' q iff for x being Element of A holds b4 . x = ('not' (p . x)) 'or' (q . x) );
:: deftheorem Def9 defines 'eqv' BVFUNC_1:def_9_:_
for A being non empty set
for p, q, b4 being Function of A,BOOLEAN holds
( b4 = p 'eqv' q iff for x being Element of A holds b4 . x = 'not' ((p . x) 'xor' (q . x)) );
definition
let Y be non empty set ;
func O_el Y -> Function of Y,BOOLEAN means :Def10: :: BVFUNC_1:def 10
for x being Element of Y holds it . x = FALSE ;
existence
ex b1 being Function of Y,BOOLEAN st
for x being Element of Y holds b1 . x = FALSE
proof
reconsider f = Y --> FALSE as Function of Y,BOOLEAN ;
reconsider f = f as Function of Y,BOOLEAN ;
take f ; ::_thesis: for x being Element of Y holds f . x = FALSE
let x be Element of Y; ::_thesis: f . x = FALSE
thus f . x = FALSE by FUNCOP_1:7; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of Y,BOOLEAN st ( for x being Element of Y holds b1 . x = FALSE ) & ( for x being Element of Y holds b2 . x = FALSE ) holds
b1 = b2
proof
deffunc H1( set ) -> Element of BOOLEAN = FALSE ;
thus for f1, f2 being Function of Y,BOOLEAN st ( for x being Element of Y holds f1 . x = H1(x) ) & ( for x being Element of Y holds f2 . x = H1(x) ) holds
f1 = f2 from BVFUNC_1:sch_1(); ::_thesis: verum
end;
end;
:: deftheorem Def10 defines O_el BVFUNC_1:def_10_:_
for Y being non empty set
for b2 being Function of Y,BOOLEAN holds
( b2 = O_el Y iff for x being Element of Y holds b2 . x = FALSE );
definition
let Y be non empty set ;
func I_el Y -> Function of Y,BOOLEAN means :Def11: :: BVFUNC_1:def 11
for x being Element of Y holds it . x = TRUE ;
existence
ex b1 being Function of Y,BOOLEAN st
for x being Element of Y holds b1 . x = TRUE
proof
reconsider f = Y --> TRUE as Function of Y,BOOLEAN ;
reconsider f = f as Function of Y,BOOLEAN ;
take f ; ::_thesis: for x being Element of Y holds f . x = TRUE
let x be Element of Y; ::_thesis: f . x = TRUE
thus f . x = TRUE by FUNCOP_1:7; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of Y,BOOLEAN st ( for x being Element of Y holds b1 . x = TRUE ) & ( for x being Element of Y holds b2 . x = TRUE ) holds
b1 = b2
proof
deffunc H1( set ) -> Element of BOOLEAN = TRUE ;
thus for f1, f2 being Function of Y,BOOLEAN st ( for x being Element of Y holds f1 . x = H1(x) ) & ( for x being Element of Y holds f2 . x = H1(x) ) holds
f1 = f2 from BVFUNC_1:sch_1(); ::_thesis: verum
end;
end;
:: deftheorem Def11 defines I_el BVFUNC_1:def_11_:_
for Y being non empty set
for b2 being Function of Y,BOOLEAN holds
( b2 = I_el Y iff for x being Element of Y holds b2 . x = TRUE );
theorem :: BVFUNC_1:1
canceled;
theorem Th2: :: BVFUNC_1:2
for Y being non empty set holds
( 'not' (I_el Y) = O_el Y & 'not' (O_el Y) = I_el Y )
proof
let Y be non empty set ; ::_thesis: ( 'not' (I_el Y) = O_el Y & 'not' (O_el Y) = I_el Y )
A1: for x being Element of Y holds ('not' (O_el Y)) . x = TRUE
proof
let x be Element of Y; ::_thesis: ('not' (O_el Y)) . x = TRUE
( ('not' (O_el Y)) . x = 'not' ((O_el Y) . x) & (O_el Y) . x = FALSE ) by Def10, MARGREL1:def_19;
hence ('not' (O_el Y)) . x = TRUE ; ::_thesis: verum
end;
for x being Element of Y holds ('not' (I_el Y)) . x = FALSE
proof
let x be Element of Y; ::_thesis: ('not' (I_el Y)) . x = FALSE
( ('not' (I_el Y)) . x = 'not' ((I_el Y) . x) & (I_el Y) . x = TRUE ) by Def11, MARGREL1:def_19;
hence ('not' (I_el Y)) . x = FALSE ; ::_thesis: verum
end;
hence ( 'not' (I_el Y) = O_el Y & 'not' (O_el Y) = I_el Y ) by A1, Def10, Def11; ::_thesis: verum
end;
theorem :: BVFUNC_1:3
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' a = a ;
theorem :: BVFUNC_1:4
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a '&' b) '&' c = a '&' (b '&' c)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a '&' b) '&' c = a '&' (b '&' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a '&' b) '&' c = a '&' (b '&' c)
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((a '&' b) '&' c) . x = (a '&' (b '&' c)) . x
thus ((a '&' b) '&' c) . x = ((a '&' b) . x) '&' (c . x) by MARGREL1:def_20
.= ((a . x) '&' (b . x)) '&' (c . x) by MARGREL1:def_20
.= (a . x) '&' ((b . x) '&' (c . x))
.= (a . x) '&' ((b '&' c) . x) by MARGREL1:def_20
.= (a '&' (b '&' c)) . x by MARGREL1:def_20 ; ::_thesis: verum
end;
theorem Th5: :: BVFUNC_1:5
for Y being non empty set
for a being Function of Y,BOOLEAN holds a '&' (O_el Y) = O_el Y
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a '&' (O_el Y) = O_el Y
let a be Function of Y,BOOLEAN; ::_thesis: a '&' (O_el Y) = O_el Y
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a '&' (O_el Y)) . x = (O_el Y) . x
thus (a '&' (O_el Y)) . x = (a . x) '&' ((O_el Y) . x) by MARGREL1:def_20
.= (a . x) '&' FALSE by Def10
.= (O_el Y) . x by Def10 ; ::_thesis: verum
end;
theorem Th6: :: BVFUNC_1:6
for Y being non empty set
for a being Function of Y,BOOLEAN holds a '&' (I_el Y) = a
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a '&' (I_el Y) = a
let a be Function of Y,BOOLEAN; ::_thesis: a '&' (I_el Y) = a
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a '&' (I_el Y)) . x = a . x
thus (a '&' (I_el Y)) . x = (a . x) '&' ((I_el Y) . x) by MARGREL1:def_20
.= (a . x) '&' TRUE by Def11
.= a . x ; ::_thesis: verum
end;
theorem :: BVFUNC_1:7
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'or' a = a ;
theorem :: BVFUNC_1:8
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'or' b) 'or' c = a 'or' (b 'or' c)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'or' b) 'or' c = a 'or' (b 'or' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'or' b) 'or' c = a 'or' (b 'or' c)
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((a 'or' b) 'or' c) . x = (a 'or' (b 'or' c)) . x
thus ((a 'or' b) 'or' c) . x = ((a 'or' b) . x) 'or' (c . x) by Def4
.= ((a . x) 'or' (b . x)) 'or' (c . x) by Def4
.= (a . x) 'or' ((b . x) 'or' (c . x))
.= (a . x) 'or' ((b 'or' c) . x) by Def4
.= (a 'or' (b 'or' c)) . x by Def4 ; ::_thesis: verum
end;
theorem Th9: :: BVFUNC_1:9
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'or' (O_el Y) = a
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a 'or' (O_el Y) = a
let a be Function of Y,BOOLEAN; ::_thesis: a 'or' (O_el Y) = a
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'or' (O_el Y)) . x = a . x
thus (a 'or' (O_el Y)) . x = (a . x) 'or' ((O_el Y) . x) by Def4
.= (a . x) 'or' FALSE by Def10
.= a . x ; ::_thesis: verum
end;
theorem Th10: :: BVFUNC_1:10
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'or' (I_el Y) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a 'or' (I_el Y) = I_el Y
let a be Function of Y,BOOLEAN; ::_thesis: a 'or' (I_el Y) = I_el Y
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'or' (I_el Y)) . x = (I_el Y) . x
thus (a 'or' (I_el Y)) . x = (a . x) 'or' ((I_el Y) . x) by Def4
.= (a . x) 'or' TRUE by Def11
.= (I_el Y) . x by Def11 ; ::_thesis: verum
end;
theorem :: BVFUNC_1:11
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a '&' b) 'or' c = (a 'or' c) '&' (b 'or' c)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a '&' b) 'or' c = (a 'or' c) '&' (b 'or' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a '&' b) 'or' c = (a 'or' c) '&' (b 'or' c)
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((a '&' b) 'or' c) . x = ((a 'or' c) '&' (b 'or' c)) . x
thus ((a '&' b) 'or' c) . x = ((a '&' b) . x) 'or' (c . x) by Def4
.= ((a . x) '&' (b . x)) 'or' (c . x) by MARGREL1:def_20
.= ((a . x) 'or' (c . x)) '&' ((b . x) 'or' (c . x)) by XBOOLEAN:9
.= ((a . x) 'or' (c . x)) '&' ((b 'or' c) . x) by Def4
.= ((a 'or' c) . x) '&' ((b 'or' c) . x) by Def4
.= ((a 'or' c) '&' (b 'or' c)) . x by MARGREL1:def_20 ; ::_thesis: verum
end;
theorem :: BVFUNC_1:12
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'or' b) '&' c = (a '&' c) 'or' (b '&' c)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'or' b) '&' c = (a '&' c) 'or' (b '&' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'or' b) '&' c = (a '&' c) 'or' (b '&' c)
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((a 'or' b) '&' c) . x = ((a '&' c) 'or' (b '&' c)) . x
thus ((a 'or' b) '&' c) . x = ((a 'or' b) . x) '&' (c . x) by MARGREL1:def_20
.= ((a . x) 'or' (b . x)) '&' (c . x) by Def4
.= ((a . x) '&' (c . x)) 'or' ((b . x) '&' (c . x)) by XBOOLEAN:8
.= ((a . x) '&' (c . x)) 'or' ((b '&' c) . x) by MARGREL1:def_20
.= ((a '&' c) . x) 'or' ((b '&' c) . x) by MARGREL1:def_20
.= ((a '&' c) 'or' (b '&' c)) . x by Def4 ; ::_thesis: verum
end;
theorem :: BVFUNC_1:13
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds 'not' (a 'or' b) = ('not' a) '&' ('not' b)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds 'not' (a 'or' b) = ('not' a) '&' ('not' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: 'not' (a 'or' b) = ('not' a) '&' ('not' b)
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ('not' (a 'or' b)) . x = (('not' a) '&' ('not' b)) . x
thus ('not' (a 'or' b)) . x = 'not' ((a 'or' b) . x) by MARGREL1:def_19
.= 'not' ((a . x) 'or' (b . x)) by Def4
.= (('not' a) . x) '&' ('not' (b . x)) by MARGREL1:def_19
.= (('not' a) . x) '&' (('not' b) . x) by MARGREL1:def_19
.= (('not' a) '&' ('not' b)) . x by MARGREL1:def_20 ; ::_thesis: verum
end;
theorem :: BVFUNC_1:14
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds 'not' (a '&' b) = ('not' a) 'or' ('not' b)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds 'not' (a '&' b) = ('not' a) 'or' ('not' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: 'not' (a '&' b) = ('not' a) 'or' ('not' b)
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ('not' (a '&' b)) . x = (('not' a) 'or' ('not' b)) . x
thus ('not' (a '&' b)) . x = 'not' ((a '&' b) . x) by MARGREL1:def_19
.= ('not' (a . x)) 'or' ('not' (b . x)) by MARGREL1:def_20
.= ('not' (a . x)) 'or' (('not' b) . x) by MARGREL1:def_19
.= (('not' a) . x) 'or' (('not' b) . x) by MARGREL1:def_19
.= (('not' a) 'or' ('not' b)) . x by Def4 ; ::_thesis: verum
end;
definition
let Y be non empty set ;
let a, b be Function of Y,BOOLEAN;
preda '<' b means :Def12: :: BVFUNC_1:def 12
for x being Element of Y st a . x = TRUE holds
b . x = TRUE ;
reflexivity
for a being Function of Y,BOOLEAN
for x being Element of Y st a . x = TRUE holds
a . x = TRUE ;
end;
:: deftheorem Def12 defines '<' BVFUNC_1:def_12_:_
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds
( a '<' b iff for x being Element of Y st a . x = TRUE holds
b . x = TRUE );
theorem :: BVFUNC_1:15
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds
( ( a '<' b & b '<' a implies a = b ) & ( a '<' b & b '<' c implies a '<' c ) )
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds
( ( a '<' b & b '<' a implies a = b ) & ( a '<' b & b '<' c implies a '<' c ) )
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ( ( a '<' b & b '<' a implies a = b ) & ( a '<' b & b '<' c implies a '<' c ) )
A1: for a, b, c being Function of Y,BOOLEAN st a '<' b & b '<' a holds
a = b
proof
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ( a '<' b & b '<' a implies a = b )
assume A6: ( a '<' b & b '<' a ) ; ::_thesis: a = b
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: a . x = b . x
( ( a . x = FALSE & b . x = FALSE ) or ( a . x = FALSE & b . x = TRUE ) or ( a . x = TRUE & b . x = FALSE ) or ( a . x = TRUE & b . x = TRUE ) ) by XBOOLEAN:def_3;
hence a . x = b . x by A6, Def12; ::_thesis: verum
end;
for a, b, c being Function of Y,BOOLEAN st a '<' b & b '<' c holds
a '<' c
proof
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ( a '<' b & b '<' c implies a '<' c )
assume that
A7: a '<' b and
A8: b '<' c ; ::_thesis: a '<' c
for x being Element of Y st a . x = TRUE holds
c . x = TRUE
proof
let x be Element of Y; ::_thesis: ( a . x = TRUE implies c . x = TRUE )
( b . x = TRUE implies c . x = TRUE ) by A8, Def12;
hence ( a . x = TRUE implies c . x = TRUE ) by A7, Def12; ::_thesis: verum
end;
hence a '<' c by Def12; ::_thesis: verum
end;
hence ( ( a '<' b & b '<' a implies a = b ) & ( a '<' b & b '<' c implies a '<' c ) ) by A1; ::_thesis: verum
end;
theorem Th16: :: BVFUNC_1:16
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds
( a 'imp' b = I_el Y iff a '<' b )
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds
( a 'imp' b = I_el Y iff a '<' b )
let a, b be Function of Y,BOOLEAN; ::_thesis: ( a 'imp' b = I_el Y iff a '<' b )
A1: for a, b being Function of Y,BOOLEAN st a '<' b holds
a 'imp' b = I_el Y
proof
let a, b be Function of Y,BOOLEAN; ::_thesis: ( a '<' b implies a 'imp' b = I_el Y )
assume A6: a '<' b ; ::_thesis: a 'imp' b = I_el Y
A8: for x being Element of Y holds ('not' (a . x)) 'or' (b . x) = TRUE
proof
let x be Element of Y; ::_thesis: ('not' (a . x)) 'or' (b . x) = TRUE
( ( a . x = FALSE & b . x = FALSE ) or ( a . x = FALSE & b . x = TRUE ) or ( a . x = TRUE & b . x = TRUE ) ) by A6, Def12, XBOOLEAN:def_3;
hence ('not' (a . x)) 'or' (b . x) = TRUE ; ::_thesis: verum
end;
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'imp' b) . x = (I_el Y) . x
( (a 'imp' b) . x = ('not' (a . x)) 'or' (b . x) & (I_el Y) . x = TRUE ) by Def8, Def11;
hence (a 'imp' b) . x = (I_el Y) . x by A8; ::_thesis: verum
end;
for a, b being Function of Y,BOOLEAN st a 'imp' b = I_el Y holds
a '<' b
proof
let a, b be Function of Y,BOOLEAN; ::_thesis: ( a 'imp' b = I_el Y implies a '<' b )
assume A9: a 'imp' b = I_el Y ; ::_thesis: a '<' b
A10: for x being Element of Y holds ('not' (a . x)) 'or' (b . x) = TRUE
proof
let x be Element of Y; ::_thesis: ('not' (a . x)) 'or' (b . x) = TRUE
(a 'imp' b) . x = ('not' (a . x)) 'or' (b . x) by Def8;
hence ('not' (a . x)) 'or' (b . x) = TRUE by A9, Def11; ::_thesis: verum
end;
for x being Element of Y holds
( ( a . x = FALSE & b . x = FALSE ) or ( a . x = FALSE & b . x = TRUE ) or ( a . x = TRUE & b . x = TRUE ) )
proof
let x be Element of Y; ::_thesis: ( ( a . x = FALSE & b . x = FALSE ) or ( a . x = FALSE & b . x = TRUE ) or ( a . x = TRUE & b . x = TRUE ) )
A11: ( ( 'not' (a . x) = TRUE & b . x = FALSE ) or ( 'not' (a . x) = TRUE & b . x = TRUE ) or ( 'not' (a . x) = FALSE & b . x = FALSE ) or ( 'not' (a . x) = FALSE & b . x = TRUE ) ) by XBOOLEAN:def_3;
('not' (a . x)) 'or' (b . x) = TRUE by A10;
hence ( ( a . x = FALSE & b . x = FALSE ) or ( a . x = FALSE & b . x = TRUE ) or ( a . x = TRUE & b . x = TRUE ) ) by A11; ::_thesis: verum
end;
then for x being Element of Y st a . x = TRUE holds
b . x = TRUE ;
hence a '<' b by Def12; ::_thesis: verum
end;
hence ( a 'imp' b = I_el Y iff a '<' b ) by A1; ::_thesis: verum
end;
theorem :: BVFUNC_1:17
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds
( a 'eqv' b = I_el Y iff a = b )
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds
( a 'eqv' b = I_el Y iff a = b )
let a, b be Function of Y,BOOLEAN; ::_thesis: ( a 'eqv' b = I_el Y iff a = b )
A1: for a, b being Function of Y,BOOLEAN st a 'eqv' b = I_el Y holds
a = b
proof
let a, b be Function of Y,BOOLEAN; ::_thesis: ( a 'eqv' b = I_el Y implies a = b )
assume A6: a 'eqv' b = I_el Y ; ::_thesis: a = b
A7: for x being Element of Y holds (('not' (a . x)) '&' (b . x)) 'or' ((a . x) '&' ('not' (b . x))) = FALSE
proof
let x be Element of Y; ::_thesis: (('not' (a . x)) '&' (b . x)) 'or' ((a . x) '&' ('not' (b . x))) = FALSE
(a 'eqv' b) . x = 'not' ((a . x) 'xor' (b . x)) by Def9;
then 'not' ((a . x) 'xor' (b . x)) = TRUE by A6, Def11;
hence (('not' (a . x)) '&' (b . x)) 'or' ((a . x) '&' ('not' (b . x))) = FALSE ; ::_thesis: verum
end;
A8: for x being Element of Y holds
( ('not' (a . x)) '&' (b . x) = FALSE & (a . x) '&' ('not' (b . x)) = FALSE )
proof
let x be Element of Y; ::_thesis: ( ('not' (a . x)) '&' (b . x) = FALSE & (a . x) '&' ('not' (b . x)) = FALSE )
A9: ( (a . x) '&' ('not' (b . x)) = TRUE or (a . x) '&' ('not' (b . x)) = FALSE ) by XBOOLEAN:def_3;
(('not' (a . x)) '&' (b . x)) 'or' ((a . x) '&' ('not' (b . x))) = FALSE by A7;
hence ( ('not' (a . x)) '&' (b . x) = FALSE & (a . x) '&' ('not' (b . x)) = FALSE ) by A9; ::_thesis: verum
end;
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: a . x = b . x
('not' (a . x)) '&' (b . x) = FALSE by A8;
then A10: ( ( 'not' (a . x) = TRUE & b . x = FALSE ) or ( 'not' (a . x) = FALSE & b . x = FALSE ) or ( 'not' (a . x) = FALSE & b . x = TRUE ) ) by MARGREL1:12, XBOOLEAN:def_3;
(a . x) '&' ('not' (b . x)) = FALSE by A8;
hence a . x = b . x by A10; ::_thesis: verum
end;
for a, b being Function of Y,BOOLEAN st a = b holds
a 'eqv' b = I_el Y
proof
let a, b be Function of Y,BOOLEAN; ::_thesis: ( a = b implies a 'eqv' b = I_el Y )
assume A15: a = b ; ::_thesis: a 'eqv' b = I_el Y
A16: for x being Element of Y holds
( ('not' (a . x)) '&' (b . x) = FALSE & (a . x) '&' ('not' (b . x)) = FALSE )
proof
let x be Element of Y; ::_thesis: ( ('not' (a . x)) '&' (b . x) = FALSE & (a . x) '&' ('not' (b . x)) = FALSE )
( b . x = TRUE iff 'not' (b . x) = FALSE ) ;
then ( ( a . x = FALSE & 'not' (b . x) = TRUE ) or ( a . x = TRUE & 'not' (b . x) = FALSE ) ) by A15, XBOOLEAN:def_3;
hence ( ('not' (a . x)) '&' (b . x) = FALSE & (a . x) '&' ('not' (b . x)) = FALSE ) ; ::_thesis: verum
end;
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'eqv' b) . x = (I_el Y) . x
(a . x) '&' ('not' (b . x)) = FALSE by A16;
then 'not' ((a . x) 'xor' (b . x)) = TRUE by A16;
then (a 'eqv' b) . x = TRUE by Def9;
hence (a 'eqv' b) . x = (I_el Y) . x by Def11; ::_thesis: verum
end;
hence ( a 'eqv' b = I_el Y iff a = b ) by A1; ::_thesis: verum
end;
theorem :: BVFUNC_1:18
for Y being non empty set
for a being Function of Y,BOOLEAN holds
( O_el Y '<' a & a '<' I_el Y )
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds
( O_el Y '<' a & a '<' I_el Y )
let a be Function of Y,BOOLEAN; ::_thesis: ( O_el Y '<' a & a '<' I_el Y )
A5: (O_el Y) 'imp' a = I_el Y
proof
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((O_el Y) 'imp' a) . x = (I_el Y) . x
((O_el Y) 'imp' a) . x = ('not' ((O_el Y) . x)) 'or' (a . x) by Def8;
then ((O_el Y) 'imp' a) . x = TRUE 'or' (a . x) by Def10;
hence ((O_el Y) 'imp' a) . x = (I_el Y) . x by Def11; ::_thesis: verum
end;
a 'imp' (I_el Y) = I_el Y
proof
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'imp' (I_el Y)) . x = (I_el Y) . x
(a 'imp' (I_el Y)) . x = ('not' (a . x)) 'or' ((I_el Y) . x) by Def8;
then (a 'imp' (I_el Y)) . x = ('not' (a . x)) 'or' TRUE by Def11;
hence (a 'imp' (I_el Y)) . x = (I_el Y) . x by Def11; ::_thesis: verum
end;
hence ( O_el Y '<' a & a '<' I_el Y ) by A5, Th16; ::_thesis: verum
end;
begin
definition
let Y be non empty set ;
let a be Function of Y,BOOLEAN;
func B_INF a -> Function of Y,BOOLEAN equals :Def13: :: BVFUNC_1:def 13
I_el Y if for x being Element of Y holds a . x = TRUE
otherwise O_el Y;
correctness
coherence
( ( ( for x being Element of Y holds a . x = TRUE ) implies I_el Y is Function of Y,BOOLEAN ) & ( not for x being Element of Y holds a . x = TRUE implies O_el Y is Function of Y,BOOLEAN ) );
consistency
for b1 being Function of Y,BOOLEAN holds verum;
;
func B_SUP a -> Function of Y,BOOLEAN equals :Def14: :: BVFUNC_1:def 14
O_el Y if for x being Element of Y holds a . x = FALSE
otherwise I_el Y;
correctness
coherence
( ( ( for x being Element of Y holds a . x = FALSE ) implies O_el Y is Function of Y,BOOLEAN ) & ( not for x being Element of Y holds a . x = FALSE implies I_el Y is Function of Y,BOOLEAN ) );
consistency
for b1 being Function of Y,BOOLEAN holds verum;
;
end;
:: deftheorem Def13 defines B_INF BVFUNC_1:def_13_:_
for Y being non empty set
for a being Function of Y,BOOLEAN holds
( ( ( for x being Element of Y holds a . x = TRUE ) implies B_INF a = I_el Y ) & ( not for x being Element of Y holds a . x = TRUE implies B_INF a = O_el Y ) );
:: deftheorem Def14 defines B_SUP BVFUNC_1:def_14_:_
for Y being non empty set
for a being Function of Y,BOOLEAN holds
( ( ( for x being Element of Y holds a . x = FALSE ) implies B_SUP a = O_el Y ) & ( not for x being Element of Y holds a . x = FALSE implies B_SUP a = I_el Y ) );
theorem Th19: :: BVFUNC_1:19
for Y being non empty set
for a being Function of Y,BOOLEAN holds
( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) )
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds
( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) )
let a be Function of Y,BOOLEAN; ::_thesis: ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) )
A1: ( ( for x being Element of Y holds ('not' a) . x = TRUE ) implies for x being Element of Y holds a . x = FALSE )
proof
assume A2: for x being Element of Y holds ('not' a) . x = TRUE ; ::_thesis: for x being Element of Y holds a . x = FALSE
let x be Element of Y; ::_thesis: a . x = FALSE
('not' a) . x = TRUE by A2;
then 'not' (a . x) = TRUE by MARGREL1:def_19;
hence a . x = FALSE ; ::_thesis: verum
end;
A3: ( ( for x being Element of Y holds ('not' a) . x = FALSE ) implies for x being Element of Y holds a . x = TRUE )
proof
assume A4: for x being Element of Y holds ('not' a) . x = FALSE ; ::_thesis: for x being Element of Y holds a . x = TRUE
let x be Element of Y; ::_thesis: a . x = TRUE
('not' a) . x = FALSE by A4;
then 'not' (a . x) = FALSE by MARGREL1:def_19;
hence a . x = TRUE ; ::_thesis: verum
end;
A5: now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_or_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_)_implies_(_'not'_(B_INF_a)_=_B_SUP_('not'_a)_&_'not'_(B_SUP_a)_=_B_INF_('not'_a)_)_)
assume A6: ( for x being Element of Y holds a . x = TRUE or for x being Element of Y holds a . x = FALSE ) ; ::_thesis: ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) )
now__::_thesis:_(_(_(_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_)_&_not_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_&_'not'_(B_INF_a)_=_B_SUP_('not'_a)_&_'not'_(B_SUP_a)_=_B_INF_('not'_a)_)_or_(_(_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_)_&_not_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_&_'not'_(B_INF_a)_=_B_SUP_('not'_a)_&_'not'_(B_SUP_a)_=_B_INF_('not'_a)_)_or_(_(_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_)_&_(_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_)_&_(_for_x_being_Element_of_Y_holds_
(_'not'_(B_INF_a)_=_B_SUP_('not'_a)_&_'not'_(B_SUP_a)_=_B_INF_('not'_a)_)_)_)_)
percases ( ( ( for x being Element of Y holds a . x = TRUE ) & not for x being Element of Y holds a . x = FALSE ) or ( ( for x being Element of Y holds a . x = FALSE ) & not for x being Element of Y holds a . x = TRUE ) or ( ( for x being Element of Y holds a . x = TRUE ) & ( for x being Element of Y holds a . x = FALSE ) ) ) by A6;
caseA7: ( ( for x being Element of Y holds a . x = TRUE ) & not for x being Element of Y holds a . x = FALSE ) ; ::_thesis: ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) )
A8: for x being Element of Y holds ('not' a) . x = FALSE
proof
let x be Element of Y; ::_thesis: ('not' a) . x = FALSE
'not' TRUE = FALSE ;
then 'not' (a . x) = FALSE by A7;
hence ('not' a) . x = FALSE by MARGREL1:def_19; ::_thesis: verum
end;
B_INF a = I_el Y by A7, Def13;
then A9: 'not' (B_INF a) = O_el Y by Th2;
( B_INF ('not' a) = O_el Y & 'not' (B_SUP a) = 'not' (I_el Y) ) by A1, A7, Def13, Def14;
hence ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) ) by A9, A8, Def14, Th2; ::_thesis: verum
end;
caseA10: ( ( for x being Element of Y holds a . x = FALSE ) & not for x being Element of Y holds a . x = TRUE ) ; ::_thesis: ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) )
A11: for x being Element of Y holds ('not' a) . x = TRUE
proof
let x be Element of Y; ::_thesis: ('not' a) . x = TRUE
'not' FALSE = TRUE ;
then 'not' (a . x) = TRUE by A10;
hence ('not' a) . x = TRUE by MARGREL1:def_19; ::_thesis: verum
end;
'not' (B_SUP a) = 'not' (O_el Y) by A10, Def14;
then A12: 'not' (B_SUP a) = I_el Y by Th2;
( B_SUP ('not' a) = I_el Y & 'not' (B_INF a) = 'not' (O_el Y) ) by A3, A10, Def13, Def14;
hence ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) ) by A12, A11, Def13, Th2; ::_thesis: verum
end;
caseA13: ( ( for x being Element of Y holds a . x = TRUE ) & ( for x being Element of Y holds a . x = FALSE ) ) ; ::_thesis: for x being Element of Y holds
( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) )
let x be Element of Y; ::_thesis: ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) )
a . x = TRUE by A13;
hence ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) ) by A13; ::_thesis: verum
end;
end;
end;
hence ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) ) ; ::_thesis: verum
end;
now__::_thesis:_(_not_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_&_not_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_implies_(_'not'_(B_INF_a)_=_B_SUP_('not'_a)_&_'not'_(B_SUP_a)_=_B_INF_('not'_a)_)_)
assume that
A14: not for x being Element of Y holds a . x = TRUE and
A15: not for x being Element of Y holds a . x = FALSE ; ::_thesis: ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) )
'not' (B_INF a) = 'not' (O_el Y) by A14, Def13;
then A16: 'not' (B_INF a) = I_el Y by Th2;
( 'not' (B_SUP a) = 'not' (I_el Y) & B_INF ('not' a) = O_el Y ) by A1, A15, Def13, Def14;
hence ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) ) by A3, A14, A16, Def14, Th2; ::_thesis: verum
end;
hence ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) ) by A5; ::_thesis: verum
end;
theorem :: BVFUNC_1:20
for Y being non empty set holds
( B_INF (O_el Y) = O_el Y & B_INF (I_el Y) = I_el Y & B_SUP (O_el Y) = O_el Y & B_SUP (I_el Y) = I_el Y )
proof
let Y be non empty set ; ::_thesis: ( B_INF (O_el Y) = O_el Y & B_INF (I_el Y) = I_el Y & B_SUP (O_el Y) = O_el Y & B_SUP (I_el Y) = I_el Y )
A1: not for x being Element of Y holds (O_el Y) . x = TRUE
proof
now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_(O_el_Y)_._x_=_TRUE_)_implies_for_x_being_Element_of_Y_holds_
not_for_x_being_Element_of_Y_holds_(O_el_Y)_._x_=_TRUE_)
assume for x being Element of Y holds (O_el Y) . x = TRUE ; ::_thesis: for x being Element of Y holds
not for x being Element of Y holds (O_el Y) . x = TRUE
let x be Element of Y; ::_thesis: not for x being Element of Y holds (O_el Y) . x = TRUE
(O_el Y) . x = FALSE by Def10;
hence not for x being Element of Y holds (O_el Y) . x = TRUE ; ::_thesis: verum
end;
hence not for x being Element of Y holds (O_el Y) . x = TRUE ; ::_thesis: verum
end;
A2: not for x being Element of Y holds (I_el Y) . x = FALSE
proof
now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_(I_el_Y)_._x_=_FALSE_)_implies_for_x_being_Element_of_Y_holds_
not_for_x_being_Element_of_Y_holds_(I_el_Y)_._x_=_FALSE_)
assume A3: for x being Element of Y holds (I_el Y) . x = FALSE ; ::_thesis: for x being Element of Y holds
not for x being Element of Y holds (I_el Y) . x = FALSE
let x be Element of Y; ::_thesis: not for x being Element of Y holds (I_el Y) . x = FALSE
(I_el Y) . x = FALSE by A3;
hence not for x being Element of Y holds (I_el Y) . x = FALSE by Def11; ::_thesis: verum
end;
hence not for x being Element of Y holds (I_el Y) . x = FALSE ; ::_thesis: verum
end;
( ( for x being Element of Y holds (O_el Y) . x = FALSE ) & ( for x being Element of Y holds (I_el Y) . x = TRUE ) ) by Def10, Def11;
hence ( B_INF (O_el Y) = O_el Y & B_INF (I_el Y) = I_el Y & B_SUP (O_el Y) = O_el Y & B_SUP (I_el Y) = I_el Y ) by A1, A2, Def13, Def14; ::_thesis: verum
end;
registration
let Y be non empty set ;
cluster O_el Y -> constant ;
coherence
O_el Y is constant
proof
for n1, n2 being set st n1 in dom (O_el Y) & n2 in dom (O_el Y) holds
(O_el Y) . n1 = (O_el Y) . n2
proof
let n1, n2 be set ; ::_thesis: ( n1 in dom (O_el Y) & n2 in dom (O_el Y) implies (O_el Y) . n1 = (O_el Y) . n2 )
assume ( n1 in dom (O_el Y) & n2 in dom (O_el Y) ) ; ::_thesis: (O_el Y) . n1 = (O_el Y) . n2
then reconsider n1 = n1, n2 = n2 as Element of Y by PARTFUN1:def_2;
( (O_el Y) . n2 = FALSE & (O_el Y) . n1 = (O_el Y) . n1 ) by Def10;
hence (O_el Y) . n1 = (O_el Y) . n2 by Def10; ::_thesis: verum
end;
hence O_el Y is constant by FUNCT_1:def_10; ::_thesis: verum
end;
end;
registration
let Y be non empty set ;
cluster I_el Y -> constant ;
coherence
I_el Y is constant
proof
thus I_el Y is constant ::_thesis: verum
proof
for n1, n2 being set st n1 in dom (I_el Y) & n2 in dom (I_el Y) holds
(I_el Y) . n1 = (I_el Y) . n2
proof
let n1, n2 be set ; ::_thesis: ( n1 in dom (I_el Y) & n2 in dom (I_el Y) implies (I_el Y) . n1 = (I_el Y) . n2 )
assume ( n1 in dom (I_el Y) & n2 in dom (I_el Y) ) ; ::_thesis: (I_el Y) . n1 = (I_el Y) . n2
then reconsider n1 = n1, n2 = n2 as Element of Y by PARTFUN1:def_2;
( (I_el Y) . n2 = TRUE & (I_el Y) . n1 = (I_el Y) . n1 ) by Def11;
hence (I_el Y) . n1 = (I_el Y) . n2 by Def11; ::_thesis: verum
end;
hence I_el Y is constant by FUNCT_1:def_10; ::_thesis: verum
end;
end;
end;
registration
let Y be non empty set ;
cluster non empty Relation-like Y -defined BOOLEAN -valued Function-like constant V21(Y) quasi_total boolean-valued for Element of bool [:Y,BOOLEAN:];
existence
ex b1 being Function of Y,BOOLEAN st b1 is constant
proof
take O_el Y ; ::_thesis: O_el Y is constant
thus O_el Y is constant ; ::_thesis: verum
end;
end;
theorem Th21: :: BVFUNC_1:21
for Y being non empty set
for a being constant Function of Y,BOOLEAN holds
( a = O_el Y or a = I_el Y )
proof
let Y be non empty set ; ::_thesis: for a being constant Function of Y,BOOLEAN holds
( a = O_el Y or a = I_el Y )
let a be constant Function of Y,BOOLEAN; ::_thesis: ( a = O_el Y or a = I_el Y )
A1: ( ex n1, n2 being set st
( n1 in Y & n2 in Y & not a . n1 = a . n2 ) or for x being Element of Y holds a . x = TRUE or for x being Element of Y holds a . x = FALSE )
proof
assume A2: for n1, n2 being set st n1 in Y & n2 in Y holds
a . n1 = a . n2 ; ::_thesis: ( for x being Element of Y holds a . x = TRUE or for x being Element of Y holds a . x = FALSE )
now__::_thesis:_(_not_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_implies_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_)
assume that
A3: not for x being Element of Y holds a . x = TRUE and
A4: not for x being Element of Y holds a . x = FALSE ; ::_thesis: contradiction
consider x1 being Element of Y such that
A5: a . x1 <> TRUE by A3;
a . x1 = FALSE by A5, XBOOLEAN:def_3;
hence contradiction by A2, A4; ::_thesis: verum
end;
hence ( for x being Element of Y holds a . x = TRUE or for x being Element of Y holds a . x = FALSE ) ; ::_thesis: verum
end;
dom a = Y by PARTFUN1:def_2;
hence ( a = O_el Y or a = I_el Y ) by A1, Def10, Def11, FUNCT_1:def_10; ::_thesis: verum
end;
theorem Th22: :: BVFUNC_1:22
for Y being non empty set
for d being constant Function of Y,BOOLEAN holds
( B_INF d = d & B_SUP d = d )
proof
let Y be non empty set ; ::_thesis: for d being constant Function of Y,BOOLEAN holds
( B_INF d = d & B_SUP d = d )
let d be constant Function of Y,BOOLEAN; ::_thesis: ( B_INF d = d & B_SUP d = d )
A1: now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_d_._x_=_TRUE_or_for_x_being_Element_of_Y_holds_d_._x_=_FALSE_)_implies_(_B_INF_d_=_d_&_B_SUP_d_=_d_)_)
assume A2: ( for x being Element of Y holds d . x = TRUE or for x being Element of Y holds d . x = FALSE ) ; ::_thesis: ( B_INF d = d & B_SUP d = d )
now__::_thesis:_(_(_(_for_x_being_Element_of_Y_holds_d_._x_=_TRUE_)_&_not_for_x_being_Element_of_Y_holds_d_._x_=_FALSE_&_B_INF_d_=_d_&_B_SUP_d_=_d_)_or_(_(_for_x_being_Element_of_Y_holds_d_._x_=_FALSE_)_&_not_for_x_being_Element_of_Y_holds_d_._x_=_TRUE_&_B_INF_d_=_d_&_B_SUP_d_=_d_)_or_(_(_for_x_being_Element_of_Y_holds_d_._x_=_TRUE_)_&_(_for_x_being_Element_of_Y_holds_d_._x_=_FALSE_)_&_(_for_x_being_Element_of_Y_holds_
(_B_INF_d_=_d_&_B_SUP_d_=_d_)_)_)_)
percases ( ( ( for x being Element of Y holds d . x = TRUE ) & not for x being Element of Y holds d . x = FALSE ) or ( ( for x being Element of Y holds d . x = FALSE ) & not for x being Element of Y holds d . x = TRUE ) or ( ( for x being Element of Y holds d . x = TRUE ) & ( for x being Element of Y holds d . x = FALSE ) ) ) by A2;
caseA3: ( ( for x being Element of Y holds d . x = TRUE ) & not for x being Element of Y holds d . x = FALSE ) ; ::_thesis: ( B_INF d = d & B_SUP d = d )
then d = I_el Y by Def11;
hence ( B_INF d = d & B_SUP d = d ) by A3, Def13, Def14; ::_thesis: verum
end;
caseA4: ( ( for x being Element of Y holds d . x = FALSE ) & not for x being Element of Y holds d . x = TRUE ) ; ::_thesis: ( B_INF d = d & B_SUP d = d )
then d = O_el Y by Def10;
hence ( B_INF d = d & B_SUP d = d ) by A4, Def13, Def14; ::_thesis: verum
end;
caseA5: ( ( for x being Element of Y holds d . x = TRUE ) & ( for x being Element of Y holds d . x = FALSE ) ) ; ::_thesis: for x being Element of Y holds
( B_INF d = d & B_SUP d = d )
let x be Element of Y; ::_thesis: ( B_INF d = d & B_SUP d = d )
d . x = TRUE by A5;
hence ( B_INF d = d & B_SUP d = d ) by A5; ::_thesis: verum
end;
end;
end;
hence ( B_INF d = d & B_SUP d = d ) ; ::_thesis: verum
end;
now__::_thesis:_(_not_for_x_being_Element_of_Y_holds_d_._x_=_TRUE_&_not_for_x_being_Element_of_Y_holds_d_._x_=_FALSE_implies_(_B_INF_d_=_d_&_B_SUP_d_=_d_)_)
assume that
A6: not for x being Element of Y holds d . x = TRUE and
A7: not for x being Element of Y holds d . x = FALSE ; ::_thesis: ( B_INF d = d & B_SUP d = d )
now__::_thesis:_(_(_d_=_O_el_Y_&_B_INF_d_=_d_&_B_SUP_d_=_d_)_or_(_d_=_I_el_Y_&_B_INF_d_=_d_&_B_SUP_d_=_d_)_)
percases ( d = O_el Y or d = I_el Y ) by Th21;
case d = O_el Y ; ::_thesis: ( B_INF d = d & B_SUP d = d )
hence ( B_INF d = d & B_SUP d = d ) by A7, Def10; ::_thesis: verum
end;
case d = I_el Y ; ::_thesis: ( B_INF d = d & B_SUP d = d )
hence ( B_INF d = d & B_SUP d = d ) by A6, Def11; ::_thesis: verum
end;
end;
end;
hence ( B_INF d = d & B_SUP d = d ) ; ::_thesis: verum
end;
hence ( B_INF d = d & B_SUP d = d ) by A1; ::_thesis: verum
end;
theorem :: BVFUNC_1:23
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds
( B_INF (a '&' b) = (B_INF a) '&' (B_INF b) & B_SUP (a 'or' b) = (B_SUP a) 'or' (B_SUP b) )
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds
( B_INF (a '&' b) = (B_INF a) '&' (B_INF b) & B_SUP (a 'or' b) = (B_SUP a) 'or' (B_SUP b) )
let a, b be Function of Y,BOOLEAN; ::_thesis: ( B_INF (a '&' b) = (B_INF a) '&' (B_INF b) & B_SUP (a 'or' b) = (B_SUP a) 'or' (B_SUP b) )
A1: now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_(a_'&'_b)_._x_=_TRUE_)_implies_(_B_INF_(a_'&'_b)_=_(B_INF_a)_'&'_(B_INF_b)_&_B_SUP_(a_'or'_b)_=_(B_SUP_a)_'or'_(B_SUP_b)_)_)
assume A2: for x being Element of Y holds (a '&' b) . x = TRUE ; ::_thesis: ( B_INF (a '&' b) = (B_INF a) '&' (B_INF b) & B_SUP (a 'or' b) = (B_SUP a) 'or' (B_SUP b) )
A3: for x being Element of Y holds a . x = TRUE
proof
let x be Element of Y; ::_thesis: a . x = TRUE
(a '&' b) . x = (a . x) '&' (b . x) by MARGREL1:def_20;
then (a . x) '&' (b . x) = TRUE by A2;
hence a . x = TRUE by XBOOLEAN:101; ::_thesis: verum
end;
not for x being Element of Y holds a . x = FALSE
proof
now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_)_implies_for_x_being_Element_of_Y_holds_
not_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_)
assume for x being Element of Y holds a . x = FALSE ; ::_thesis: for x being Element of Y holds
not for x being Element of Y holds a . x = FALSE
let x be Element of Y; ::_thesis: not for x being Element of Y holds a . x = FALSE
a . x = TRUE by A3;
hence not for x being Element of Y holds a . x = FALSE ; ::_thesis: verum
end;
hence not for x being Element of Y holds a . x = FALSE ; ::_thesis: verum
end;
then A4: B_SUP a = I_el Y by Def14;
A5: for x being Element of Y holds b . x = TRUE
proof
let x be Element of Y; ::_thesis: b . x = TRUE
(a '&' b) . x = TRUE by A2;
then (a . x) '&' (b . x) = TRUE by MARGREL1:def_20;
hence b . x = TRUE by XBOOLEAN:101; ::_thesis: verum
end;
not for x being Element of Y holds b . x = FALSE
proof
now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_b_._x_=_FALSE_)_implies_for_x_being_Element_of_Y_holds_
not_for_x_being_Element_of_Y_holds_b_._x_=_FALSE_)
assume for x being Element of Y holds b . x = FALSE ; ::_thesis: for x being Element of Y holds
not for x being Element of Y holds b . x = FALSE
let x be Element of Y; ::_thesis: not for x being Element of Y holds b . x = FALSE
b . x = TRUE by A5;
hence not for x being Element of Y holds b . x = FALSE ; ::_thesis: verum
end;
hence not for x being Element of Y holds b . x = FALSE ; ::_thesis: verum
end;
then A6: (B_SUP a) 'or' (B_SUP b) = (I_el Y) 'or' (I_el Y) by A4, Def14;
A7: not for x being Element of Y holds (a 'or' b) . x = FALSE
proof
now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_(a_'or'_b)_._x_=_FALSE_)_implies_for_x_being_Element_of_Y_holds_
not_for_x_being_Element_of_Y_holds_(a_'or'_b)_._x_=_FALSE_)
assume for x being Element of Y holds (a 'or' b) . x = FALSE ; ::_thesis: for x being Element of Y holds
not for x being Element of Y holds (a 'or' b) . x = FALSE
let x be Element of Y; ::_thesis: not for x being Element of Y holds (a 'or' b) . x = FALSE
( (a 'or' b) . x = (a . x) 'or' (b . x) & a . x = TRUE ) by A3, Def4;
hence not for x being Element of Y holds (a 'or' b) . x = FALSE ; ::_thesis: verum
end;
hence not for x being Element of Y holds (a 'or' b) . x = FALSE ; ::_thesis: verum
end;
(B_INF a) '&' (B_INF b) = (B_INF a) '&' (I_el Y) by A5, Def13
.= (I_el Y) '&' (I_el Y) by A3, Def13 ;
hence ( B_INF (a '&' b) = (B_INF a) '&' (B_INF b) & B_SUP (a 'or' b) = (B_SUP a) 'or' (B_SUP b) ) by A2, A7, A6, Def13, Def14; ::_thesis: verum
end;
A8: now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_(a_'or'_b)_._x_=_FALSE_)_implies_(_B_INF_(a_'&'_b)_=_(B_INF_a)_'&'_(B_INF_b)_&_B_SUP_(a_'or'_b)_=_(B_SUP_a)_'or'_(B_SUP_b)_)_)
assume A9: for x being Element of Y holds (a 'or' b) . x = FALSE ; ::_thesis: ( B_INF (a '&' b) = (B_INF a) '&' (B_INF b) & B_SUP (a 'or' b) = (B_SUP a) 'or' (B_SUP b) )
A10: for x being Element of Y holds a . x = FALSE
proof
let x be Element of Y; ::_thesis: a . x = FALSE
(a 'or' b) . x = FALSE by A9;
then A11: (a . x) 'or' (b . x) = FALSE by Def4;
( a . x = TRUE or a . x = FALSE ) by XBOOLEAN:def_3;
hence a . x = FALSE by A11; ::_thesis: verum
end;
A12: not for x being Element of Y holds (a '&' b) . x = TRUE
proof
now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_(a_'&'_b)_._x_=_TRUE_)_implies_for_x_being_Element_of_Y_holds_
not_for_x_being_Element_of_Y_holds_(a_'&'_b)_._x_=_TRUE_)
assume for x being Element of Y holds (a '&' b) . x = TRUE ; ::_thesis: for x being Element of Y holds
not for x being Element of Y holds (a '&' b) . x = TRUE
let x be Element of Y; ::_thesis: not for x being Element of Y holds (a '&' b) . x = TRUE
( (a '&' b) . x = (a . x) '&' (b . x) & a . x = FALSE ) by A10, MARGREL1:def_20;
hence not for x being Element of Y holds (a '&' b) . x = TRUE ; ::_thesis: verum
end;
hence not for x being Element of Y holds (a '&' b) . x = TRUE ; ::_thesis: verum
end;
A13: for x being Element of Y holds b . x = FALSE
proof
let x be Element of Y; ::_thesis: b . x = FALSE
(a 'or' b) . x = FALSE by A9;
then A14: (a . x) 'or' (b . x) = FALSE by Def4;
( b . x = TRUE or b . x = FALSE ) by XBOOLEAN:def_3;
hence b . x = FALSE by A14; ::_thesis: verum
end;
then B_SUP b = O_el Y by Def14;
then A15: (B_SUP a) 'or' (B_SUP b) = (O_el Y) 'or' (O_el Y) by A10, Def14;
not for x being Element of Y holds a . x = TRUE
proof
now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_)_implies_for_x_being_Element_of_Y_holds_
not_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_)
assume for x being Element of Y holds a . x = TRUE ; ::_thesis: for x being Element of Y holds
not for x being Element of Y holds a . x = TRUE
let x be Element of Y; ::_thesis: not for x being Element of Y holds a . x = TRUE
a . x = FALSE by A10;
hence not for x being Element of Y holds a . x = TRUE ; ::_thesis: verum
end;
hence not for x being Element of Y holds a . x = TRUE ; ::_thesis: verum
end;
then A16: B_INF a = O_el Y by Def13;
not for x being Element of Y holds b . x = TRUE
proof
now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_b_._x_=_TRUE_)_implies_for_x_being_Element_of_Y_holds_
not_for_x_being_Element_of_Y_holds_b_._x_=_TRUE_)
assume for x being Element of Y holds b . x = TRUE ; ::_thesis: for x being Element of Y holds
not for x being Element of Y holds b . x = TRUE
let x be Element of Y; ::_thesis: not for x being Element of Y holds b . x = TRUE
b . x = FALSE by A13;
hence not for x being Element of Y holds b . x = TRUE ; ::_thesis: verum
end;
hence not for x being Element of Y holds b . x = TRUE ; ::_thesis: verum
end;
then (B_INF a) '&' (B_INF b) = (O_el Y) '&' (O_el Y) by A16, Def13;
hence ( B_INF (a '&' b) = (B_INF a) '&' (B_INF b) & B_SUP (a 'or' b) = (B_SUP a) 'or' (B_SUP b) ) by A9, A15, A12, Def13, Def14; ::_thesis: verum
end;
now__::_thesis:_(_not_for_x_being_Element_of_Y_holds_(a_'&'_b)_._x_=_TRUE_&_not_for_x_being_Element_of_Y_holds_(a_'or'_b)_._x_=_FALSE_implies_(_B_INF_(a_'&'_b)_=_(B_INF_a)_'&'_(B_INF_b)_&_B_SUP_(a_'or'_b)_=_(B_SUP_a)_'or'_(B_SUP_b)_)_)
assume that
A17: not for x being Element of Y holds (a '&' b) . x = TRUE and
A18: not for x being Element of Y holds (a 'or' b) . x = FALSE ; ::_thesis: ( B_INF (a '&' b) = (B_INF a) '&' (B_INF b) & B_SUP (a 'or' b) = (B_SUP a) 'or' (B_SUP b) )
( ( for x being Element of Y holds a . x = FALSE ) & ( for x being Element of Y holds b . x = FALSE ) implies for x being Element of Y holds (a 'or' b) . x = FALSE )
proof
assume that
A19: for x being Element of Y holds a . x = FALSE and
A20: for x being Element of Y holds b . x = FALSE ; ::_thesis: for x being Element of Y holds (a 'or' b) . x = FALSE
let x be Element of Y; ::_thesis: (a 'or' b) . x = FALSE
a . x = FALSE by A19;
then (a . x) 'or' (b . x) = FALSE by A20;
hence (a 'or' b) . x = FALSE by Def4; ::_thesis: verum
end;
then ( B_SUP a = I_el Y or B_SUP b = I_el Y ) by A18, Def14;
then A21: (B_SUP a) 'or' (B_SUP b) = I_el Y by Th10;
( ( for x being Element of Y holds a . x = TRUE ) & ( for x being Element of Y holds b . x = TRUE ) implies for x being Element of Y holds (a '&' b) . x = TRUE )
proof
assume that
A22: for x being Element of Y holds a . x = TRUE and
A23: for x being Element of Y holds b . x = TRUE ; ::_thesis: for x being Element of Y holds (a '&' b) . x = TRUE
let x be Element of Y; ::_thesis: (a '&' b) . x = TRUE
a . x = TRUE by A22;
then (a . x) '&' (b . x) = TRUE by A23;
hence (a '&' b) . x = TRUE by MARGREL1:def_20; ::_thesis: verum
end;
then ( B_INF a = O_el Y or B_INF b = O_el Y ) by A17, Def13;
then (B_INF a) '&' (B_INF b) = O_el Y by Th5;
hence ( B_INF (a '&' b) = (B_INF a) '&' (B_INF b) & B_SUP (a 'or' b) = (B_SUP a) 'or' (B_SUP b) ) by A17, A18, A21, Def13, Def14; ::_thesis: verum
end;
hence ( B_INF (a '&' b) = (B_INF a) '&' (B_INF b) & B_SUP (a 'or' b) = (B_SUP a) 'or' (B_SUP b) ) by A1, A8; ::_thesis: verum
end;
theorem :: BVFUNC_1:24
for Y being non empty set
for a being Function of Y,BOOLEAN
for d being constant Function of Y,BOOLEAN holds
( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN
for d being constant Function of Y,BOOLEAN holds
( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
let a be Function of Y,BOOLEAN; ::_thesis: for d being constant Function of Y,BOOLEAN holds
( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
let d be constant Function of Y,BOOLEAN; ::_thesis: ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
A5: (I_el Y) 'imp' (I_el Y) = I_el Y
proof
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((I_el Y) 'imp' (I_el Y)) . x = (I_el Y) . x
(I_el Y) . x = TRUE by Def11;
then ((I_el Y) 'imp' (I_el Y)) . x = ('not' TRUE) 'or' TRUE by Def8;
hence ((I_el Y) 'imp' (I_el Y)) . x = (I_el Y) . x by Def11; ::_thesis: verum
end;
A6: (B_SUP a) 'imp' d = (B_SUP a) 'imp' (B_INF d) by Th22;
A7: B_INF d = d by Th22;
A12: (O_el Y) 'imp' (I_el Y) = I_el Y
proof
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((O_el Y) 'imp' (I_el Y)) . x = (I_el Y) . x
( ((O_el Y) 'imp' (I_el Y)) . x = ('not' ((O_el Y) . x)) 'or' ((I_el Y) . x) & (I_el Y) . x = TRUE ) by Def8, Def11;
hence ((O_el Y) 'imp' (I_el Y)) . x = (I_el Y) . x ; ::_thesis: verum
end;
A18: (I_el Y) 'imp' (O_el Y) = O_el Y
proof
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((I_el Y) 'imp' (O_el Y)) . x = (O_el Y) . x
(O_el Y) . x = FALSE by Def10;
then A17: ('not' ((I_el Y) . x)) 'or' ((O_el Y) . x) = ('not' TRUE) 'or' FALSE by Def11;
((I_el Y) 'imp' (O_el Y)) . x = ('not' ((I_el Y) . x)) 'or' ((O_el Y) . x) by Def8;
hence ((I_el Y) 'imp' (O_el Y)) . x = (O_el Y) . x by A17, Def10; ::_thesis: verum
end;
A23: (O_el Y) 'imp' (O_el Y) = I_el Y
proof
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((O_el Y) 'imp' (O_el Y)) . x = (I_el Y) . x
(O_el Y) . x = FALSE by Def10;
then ((O_el Y) 'imp' (O_el Y)) . x = TRUE 'or' FALSE by Def8;
hence ((O_el Y) 'imp' (O_el Y)) . x = (I_el Y) . x by Def11; ::_thesis: verum
end;
A24: d 'imp' (B_INF a) = (B_INF d) 'imp' (B_INF a) by Th22;
A25: (B_SUP a) 'imp' d = (B_SUP a) 'imp' (B_SUP d) by Th22;
A26: now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_d_._x_=_TRUE_or_for_x_being_Element_of_Y_holds_d_._x_=_FALSE_)_implies_(_B_INF_(d_'imp'_a)_=_d_'imp'_(B_INF_a)_&_B_INF_(a_'imp'_d)_=_(B_SUP_a)_'imp'_d_)_)
assume A27: ( for x being Element of Y holds d . x = TRUE or for x being Element of Y holds d . x = FALSE ) ; ::_thesis: ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
now__::_thesis:_(_(_(_for_x_being_Element_of_Y_holds_d_._x_=_TRUE_)_&_not_for_x_being_Element_of_Y_holds_d_._x_=_FALSE_&_B_INF_(d_'imp'_a)_=_d_'imp'_(B_INF_a)_&_B_INF_(a_'imp'_d)_=_(B_SUP_a)_'imp'_d_)_or_(_(_for_x_being_Element_of_Y_holds_d_._x_=_FALSE_)_&_not_for_x_being_Element_of_Y_holds_d_._x_=_TRUE_&_B_INF_(d_'imp'_a)_=_d_'imp'_(B_INF_a)_&_B_INF_(a_'imp'_d)_=_(B_SUP_a)_'imp'_d_)_or_(_(_for_x_being_Element_of_Y_holds_d_._x_=_TRUE_)_&_(_for_x_being_Element_of_Y_holds_d_._x_=_FALSE_)_&_(_for_x_being_Element_of_Y_holds_
(_B_INF_(d_'imp'_a)_=_d_'imp'_(B_INF_a)_&_B_INF_(a_'imp'_d)_=_(B_SUP_a)_'imp'_d_)_)_)_)
percases ( ( ( for x being Element of Y holds d . x = TRUE ) & not for x being Element of Y holds d . x = FALSE ) or ( ( for x being Element of Y holds d . x = FALSE ) & not for x being Element of Y holds d . x = TRUE ) or ( ( for x being Element of Y holds d . x = TRUE ) & ( for x being Element of Y holds d . x = FALSE ) ) ) by A27;
caseA28: ( ( for x being Element of Y holds d . x = TRUE ) & not for x being Element of Y holds d . x = FALSE ) ; ::_thesis: ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
A29: now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_or_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_)_implies_(_B_INF_(d_'imp'_a)_=_d_'imp'_(B_INF_a)_&_B_INF_(a_'imp'_d)_=_(B_SUP_a)_'imp'_d_)_)
assume A30: ( for x being Element of Y holds a . x = TRUE or for x being Element of Y holds a . x = FALSE ) ; ::_thesis: ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
now__::_thesis:_(_(_(_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_)_&_not_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_&_B_INF_(d_'imp'_a)_=_d_'imp'_(B_INF_a)_&_B_INF_(a_'imp'_d)_=_(B_SUP_a)_'imp'_d_)_or_(_(_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_)_&_not_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_&_B_INF_(d_'imp'_a)_=_d_'imp'_(B_INF_a)_&_B_INF_(a_'imp'_d)_=_(B_SUP_a)_'imp'_d_)_or_(_(_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_)_&_(_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_)_&_B_INF_(d_'imp'_a)_=_d_'imp'_(B_INF_a)_&_B_INF_(a_'imp'_d)_=_(B_SUP_a)_'imp'_d_)_)
percases ( ( ( for x being Element of Y holds a . x = TRUE ) & not for x being Element of Y holds a . x = FALSE ) or ( ( for x being Element of Y holds a . x = FALSE ) & not for x being Element of Y holds a . x = TRUE ) or ( ( for x being Element of Y holds a . x = FALSE ) & ( for x being Element of Y holds a . x = TRUE ) ) ) by A30;
caseA31: ( ( for x being Element of Y holds a . x = TRUE ) & not for x being Element of Y holds a . x = FALSE ) ; ::_thesis: ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
A32: for x being Element of Y holds (a 'imp' d) . x = TRUE
proof
let x be Element of Y; ::_thesis: (a 'imp' d) . x = TRUE
( d . x = TRUE & a . x = TRUE ) by A28, A31;
then (a 'imp' d) . x = ('not' TRUE) 'or' TRUE by Def8;
hence (a 'imp' d) . x = TRUE ; ::_thesis: verum
end;
A33: for x being Element of Y holds (d 'imp' a) . x = TRUE
proof
let x be Element of Y; ::_thesis: (d 'imp' a) . x = TRUE
( d . x = TRUE & a . x = TRUE ) by A28, A31;
then (d 'imp' a) . x = ('not' TRUE) 'or' TRUE by Def8;
hence (d 'imp' a) . x = TRUE ; ::_thesis: verum
end;
B_INF a = I_el Y by A31, Def13;
then A34: d 'imp' (B_INF a) = I_el Y by A24, A5, A28, Def13;
A35: B_SUP a = I_el Y by A31, Def14;
B_SUP d = I_el Y by A28, Def14;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A25, A5, A33, A32, A35, A34, Def13; ::_thesis: verum
end;
caseA36: ( ( for x being Element of Y holds a . x = FALSE ) & not for x being Element of Y holds a . x = TRUE ) ; ::_thesis: ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
A37: for x being Element of Y holds (d 'imp' a) . x = FALSE
proof
let x be Element of Y; ::_thesis: (d 'imp' a) . x = FALSE
( (d 'imp' a) . x = ('not' (d . x)) 'or' (a . x) & d . x = TRUE ) by A28, Def8;
hence (d 'imp' a) . x = FALSE by A36; ::_thesis: verum
end;
A38: now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_(d_'imp'_a)_._x_=_TRUE_)_implies_for_x_being_Element_of_Y_holds_contradiction_)
assume A39: for x being Element of Y holds (d 'imp' a) . x = TRUE ; ::_thesis: for x being Element of Y holds contradiction
let x be Element of Y; ::_thesis: contradiction
(d 'imp' a) . x = TRUE by A39;
hence contradiction by A37; ::_thesis: verum
end;
A40: for x being Element of Y holds (a 'imp' d) . x = TRUE
proof
let x be Element of Y; ::_thesis: (a 'imp' d) . x = TRUE
( d . x = TRUE & a . x = FALSE ) by A28, A36;
then (a 'imp' d) . x = ('not' FALSE) 'or' TRUE by Def8;
hence (a 'imp' d) . x = TRUE ; ::_thesis: verum
end;
A41: B_SUP a = O_el Y by A36, Def14;
B_SUP d = I_el Y by A28, Def14;
then A42: (B_SUP a) 'imp' d = I_el Y by A12, A41, Th22;
A43: B_INF a = O_el Y by A36, Def13;
B_INF d = I_el Y by A28, Def13;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A24, A18, A38, A40, A43, A42, Def13; ::_thesis: verum
end;
caseA44: ( ( for x being Element of Y holds a . x = FALSE ) & ( for x being Element of Y holds a . x = TRUE ) ) ; ::_thesis: ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
A45: for x being Element of Y holds (d 'imp' a) . x = TRUE
proof
let x be Element of Y; ::_thesis: (d 'imp' a) . x = TRUE
( (d 'imp' a) . x = ('not' (d . x)) 'or' (a . x) & a . x = TRUE ) by A44, Def8;
hence (d 'imp' a) . x = TRUE ; ::_thesis: verum
end;
A46: B_INF d = I_el Y by A28, Def13;
A47: for x being Element of Y holds (a 'imp' d) . x = TRUE
proof
let x be Element of Y; ::_thesis: (a 'imp' d) . x = TRUE
( (a 'imp' d) . x = ('not' (a . x)) 'or' (d . x) & d . x = TRUE ) by A28, Def8;
hence (a 'imp' d) . x = TRUE ; ::_thesis: verum
end;
( B_INF a = I_el Y & B_SUP a = O_el Y ) by A44, Def13, Def14;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A24, A6, A5, A12, A45, A47, A46, Def13; ::_thesis: verum
end;
end;
end;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) ; ::_thesis: verum
end;
now__::_thesis:_(_not_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_&_not_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_implies_(_B_INF_(d_'imp'_a)_=_d_'imp'_(B_INF_a)_&_B_INF_(a_'imp'_d)_=_(B_SUP_a)_'imp'_d_)_)
A48: for x being Element of Y holds (a 'imp' d) . x = TRUE
proof
let x be Element of Y; ::_thesis: (a 'imp' d) . x = TRUE
('not' (a . x)) 'or' (d . x) = (('not' a) . x) 'or' (d . x) by MARGREL1:def_19;
then ('not' (a . x)) 'or' (d . x) = (('not' a) 'or' d) . x by Def4;
then B49: ('not' (a . x)) 'or' (d . x) = (('not' a) 'or' (I_el Y)) . x by A7, A28, Def13;
(a 'imp' d) . x = ('not' (a . x)) 'or' (d . x) by Def8;
hence (a 'imp' d) . x = TRUE by Th10, Def11, B49; ::_thesis: verum
end;
A50: B_INF d = I_el Y by A28, Def13;
assume that
A51: not for x being Element of Y holds a . x = TRUE and
A52: not for x being Element of Y holds a . x = FALSE ; ::_thesis: ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
A53: B_INF a = O_el Y by A51, Def13;
B_SUP a = I_el Y by A52, Def14;
then A54: (B_SUP a) 'imp' d = I_el Y by A5, A50, Th22;
d 'imp' a = a
proof
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (d 'imp' a) . x = a . x
('not' (d . x)) 'or' (a . x) = (('not' d) . x) 'or' (a . x) by MARGREL1:def_19;
then ('not' (d . x)) 'or' (a . x) = (('not' d) 'or' a) . x by Def4;
then ('not' (d . x)) 'or' (a . x) = (('not' (I_el Y)) 'or' a) . x by A7, A28, Def13;
then A59: ('not' (d . x)) 'or' (a . x) = ((O_el Y) 'or' a) . x by Th2;
(d 'imp' a) . x = ('not' (d . x)) 'or' (a . x) by Def8;
hence (d 'imp' a) . x = a . x by A59, Th9; ::_thesis: verum
end;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A24, A18, A28, Def13, A53, A48, A54; ::_thesis: verum
end;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A29; ::_thesis: verum
end;
caseA60: ( ( for x being Element of Y holds d . x = FALSE ) & not for x being Element of Y holds d . x = TRUE ) ; ::_thesis: ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
A61: now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_or_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_)_implies_(_B_INF_(d_'imp'_a)_=_d_'imp'_(B_INF_a)_&_B_INF_(a_'imp'_d)_=_(B_SUP_a)_'imp'_d_)_)
assume A62: ( for x being Element of Y holds a . x = TRUE or for x being Element of Y holds a . x = FALSE ) ; ::_thesis: ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
now__::_thesis:_(_(_(_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_)_&_not_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_&_B_INF_(d_'imp'_a)_=_d_'imp'_(B_INF_a)_&_B_INF_(a_'imp'_d)_=_(B_SUP_a)_'imp'_d_)_or_(_(_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_)_&_not_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_&_B_INF_(d_'imp'_a)_=_d_'imp'_(B_INF_a)_&_B_INF_(a_'imp'_d)_=_(B_SUP_a)_'imp'_d_)_or_(_(_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_)_&_(_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_)_&_B_INF_(d_'imp'_a)_=_d_'imp'_(B_INF_a)_&_B_INF_(a_'imp'_d)_=_(B_SUP_a)_'imp'_d_)_)
percases ( ( ( for x being Element of Y holds a . x = TRUE ) & not for x being Element of Y holds a . x = FALSE ) or ( ( for x being Element of Y holds a . x = FALSE ) & not for x being Element of Y holds a . x = TRUE ) or ( ( for x being Element of Y holds a . x = FALSE ) & ( for x being Element of Y holds a . x = TRUE ) ) ) by A62;
caseA63: ( ( for x being Element of Y holds a . x = TRUE ) & not for x being Element of Y holds a . x = FALSE ) ; ::_thesis: ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
A64: for x being Element of Y holds (a 'imp' d) . x = FALSE
proof
let x be Element of Y; ::_thesis: (a 'imp' d) . x = FALSE
( d . x = FALSE & a . x = TRUE ) by A60, A63;
then (a 'imp' d) . x = ('not' TRUE) 'or' FALSE by Def8;
hence (a 'imp' d) . x = FALSE ; ::_thesis: verum
end;
A65: now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_(a_'imp'_d)_._x_=_TRUE_)_implies_for_x_being_Element_of_Y_holds_contradiction_)
assume A66: for x being Element of Y holds (a 'imp' d) . x = TRUE ; ::_thesis: for x being Element of Y holds contradiction
let x be Element of Y; ::_thesis: contradiction
(a 'imp' d) . x = TRUE by A66;
hence contradiction by A64; ::_thesis: verum
end;
A67: for x being Element of Y holds (d 'imp' a) . x = TRUE
proof
let x be Element of Y; ::_thesis: (d 'imp' a) . x = TRUE
( d . x = FALSE & a . x = TRUE ) by A60, A63;
then (d 'imp' a) . x = ('not' FALSE) 'or' TRUE by Def8;
hence (d 'imp' a) . x = TRUE ; ::_thesis: verum
end;
A68: B_SUP a = I_el Y by A63, Def14;
B_SUP d = O_el Y by A60, Def14;
then A69: (B_SUP a) 'imp' d = O_el Y by A18, A68, Th22;
A70: B_INF a = I_el Y by A63, Def13;
B_INF d = O_el Y by A60, Def13;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A24, A12, A67, A65, A70, A69, Def13; ::_thesis: verum
end;
caseA71: ( ( for x being Element of Y holds a . x = FALSE ) & not for x being Element of Y holds a . x = TRUE ) ; ::_thesis: ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
A72: for x being Element of Y holds (d 'imp' a) . x = TRUE
proof
let x be Element of Y; ::_thesis: (d 'imp' a) . x = TRUE
( d . x = FALSE & a . x = FALSE ) by A60, A71;
then (d 'imp' a) . x = ('not' FALSE) 'or' FALSE by Def8;
hence (d 'imp' a) . x = TRUE ; ::_thesis: verum
end;
A73: B_INF d = O_el Y by A60, Def13;
A74: for x being Element of Y holds (a 'imp' d) . x = TRUE
proof
let x be Element of Y; ::_thesis: (a 'imp' d) . x = TRUE
( (a 'imp' d) . x = ('not' (a . x)) 'or' (d . x) & a . x = FALSE ) by A71, Def8;
hence (a 'imp' d) . x = TRUE ; ::_thesis: verum
end;
( B_INF a = O_el Y & B_SUP a = O_el Y ) by A71, Def13, Def14;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A24, A6, A23, A72, A74, A73, Def13; ::_thesis: verum
end;
caseA75: ( ( for x being Element of Y holds a . x = FALSE ) & ( for x being Element of Y holds a . x = TRUE ) ) ; ::_thesis: ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
A76: for x being Element of Y holds (a 'imp' d) . x = TRUE
proof
let x be Element of Y; ::_thesis: (a 'imp' d) . x = TRUE
( (a 'imp' d) . x = ('not' (a . x)) 'or' (d . x) & a . x = FALSE ) by A75, Def8;
hence (a 'imp' d) . x = TRUE ; ::_thesis: verum
end;
A77: for x being Element of Y holds (d 'imp' a) . x = TRUE
proof
let x be Element of Y; ::_thesis: (d 'imp' a) . x = TRUE
( (d 'imp' a) . x = ('not' (d . x)) 'or' (a . x) & a . x = TRUE ) by A75, Def8;
hence (d 'imp' a) . x = TRUE ; ::_thesis: verum
end;
A78: B_INF d = O_el Y by A60, Def13;
B_SUP a = O_el Y by A75, Def14;
then A79: (B_SUP a) 'imp' d = I_el Y by A23, A78, Th22;
B_INF a = I_el Y by A75, Def13;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A24, A12, A77, A76, A78, A79, Def13; ::_thesis: verum
end;
end;
end;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) ; ::_thesis: verum
end;
now__::_thesis:_(_not_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_&_not_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_implies_(_B_INF_(d_'imp'_a)_=_d_'imp'_(B_INF_a)_&_B_INF_(a_'imp'_d)_=_(B_SUP_a)_'imp'_d_)_)
A80: B_INF d = O_el Y by A60, Def13;
A81: for x being Element of Y holds (d 'imp' a) . x = TRUE
proof
let x be Element of Y; ::_thesis: (d 'imp' a) . x = TRUE
('not' (d . x)) 'or' (a . x) = (('not' d) . x) 'or' (a . x) by MARGREL1:def_19;
then ('not' (d . x)) 'or' (a . x) = (('not' (O_el Y)) 'or' a) . x by A7, A80, Def4;
then ('not' (d . x)) 'or' (a . x) = ((I_el Y) 'or' a) . x by Th2;
then ('not' (d . x)) 'or' (a . x) = TRUE by Def11, Th10;
hence (d 'imp' a) . x = TRUE by Def8; ::_thesis: verum
end;
a 'imp' d = 'not' a
proof
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'imp' d) . x = ('not' a) . x
('not' (a . x)) 'or' (d . x) = (('not' a) . x) 'or' (d . x) by MARGREL1:def_19;
then ('not' (a . x)) 'or' (d . x) = (('not' a) 'or' d) . x by Def4;
then ('not' (a . x)) 'or' (d . x) = ('not' a) . x by A7, A80, Th9;
hence (a 'imp' d) . x = ('not' a) . x by Def8; ::_thesis: verum
end;
then A86: B_INF (a 'imp' d) = 'not' (B_SUP a) by Th19;
assume ( not for x being Element of Y holds a . x = TRUE & not for x being Element of Y holds a . x = FALSE ) ; ::_thesis: ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
then A87: ( B_INF a = O_el Y & B_SUP a = I_el Y ) by Def13, Def14;
B_INF d = O_el Y by A60, Def13;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A24, A6, A18, A23, A81, A86, A87, Def13, Th2; ::_thesis: verum
end;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A61; ::_thesis: verum
end;
caseA88: ( ( for x being Element of Y holds d . x = TRUE ) & ( for x being Element of Y holds d . x = FALSE ) ) ; ::_thesis: for x being Element of Y holds
( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
let x be Element of Y; ::_thesis: ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
d . x = FALSE by A88;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A88; ::_thesis: verum
end;
end;
end;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) ; ::_thesis: verum
end;
now__::_thesis:_(_not_for_x_being_Element_of_Y_holds_d_._x_=_TRUE_&_not_for_x_being_Element_of_Y_holds_d_._x_=_FALSE_implies_(_B_INF_(d_'imp'_a)_=_d_'imp'_(B_INF_a)_&_B_INF_(a_'imp'_d)_=_(B_SUP_a)_'imp'_d_)_)
assume that
A89: not for x being Element of Y holds d . x = TRUE and
A90: not for x being Element of Y holds d . x = FALSE ; ::_thesis: ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
now__::_thesis:_(_(_d_=_O_el_Y_&_B_INF_(d_'imp'_a)_=_d_'imp'_(B_INF_a)_&_B_INF_(a_'imp'_d)_=_(B_SUP_a)_'imp'_d_)_or_(_d_=_I_el_Y_&_B_INF_(d_'imp'_a)_=_d_'imp'_(B_INF_a)_&_B_INF_(a_'imp'_d)_=_(B_SUP_a)_'imp'_d_)_)
percases ( d = O_el Y or d = I_el Y ) by Th21;
case d = O_el Y ; ::_thesis: ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A90, Def10; ::_thesis: verum
end;
case d = I_el Y ; ::_thesis: ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A89, Def11; ::_thesis: verum
end;
end;
end;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) ; ::_thesis: verum
end;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A26; ::_thesis: verum
end;
theorem :: BVFUNC_1:25
for Y being non empty set
for a being Function of Y,BOOLEAN
for d being constant Function of Y,BOOLEAN holds
( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d )
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN
for d being constant Function of Y,BOOLEAN holds
( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d )
let a be Function of Y,BOOLEAN; ::_thesis: for d being constant Function of Y,BOOLEAN holds
( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d )
let d be constant Function of Y,BOOLEAN; ::_thesis: ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d )
A1: d 'or' (B_INF a) = (B_INF d) 'or' (B_INF a) by Th22;
A2: d '&' (B_SUP a) = (B_SUP d) '&' (B_SUP a) by Th22;
A3: B_INF d = d by Th22;
A4: now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_d_._x_=_TRUE_or_for_x_being_Element_of_Y_holds_d_._x_=_FALSE_)_implies_(_B_INF_(d_'or'_a)_=_d_'or'_(B_INF_a)_&_B_SUP_(d_'&'_a)_=_d_'&'_(B_SUP_a)_&_B_SUP_(a_'&'_d)_=_(B_SUP_a)_'&'_d_)_)
assume A5: ( for x being Element of Y holds d . x = TRUE or for x being Element of Y holds d . x = FALSE ) ; ::_thesis: ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d )
now__::_thesis:_(_(_(_for_x_being_Element_of_Y_holds_d_._x_=_TRUE_)_&_not_for_x_being_Element_of_Y_holds_d_._x_=_FALSE_&_B_INF_(d_'or'_a)_=_d_'or'_(B_INF_a)_&_B_SUP_(d_'&'_a)_=_d_'&'_(B_SUP_a)_&_B_SUP_(a_'&'_d)_=_(B_SUP_a)_'&'_d_)_or_(_(_for_x_being_Element_of_Y_holds_d_._x_=_FALSE_)_&_not_for_x_being_Element_of_Y_holds_d_._x_=_TRUE_&_B_INF_(d_'or'_a)_=_d_'or'_(B_INF_a)_&_B_SUP_(d_'&'_a)_=_d_'&'_(B_SUP_a)_&_B_SUP_(a_'&'_d)_=_(B_SUP_a)_'&'_d_)_or_(_(_for_x_being_Element_of_Y_holds_d_._x_=_TRUE_)_&_(_for_x_being_Element_of_Y_holds_d_._x_=_FALSE_)_&_(_for_x_being_Element_of_Y_holds_
(_B_INF_(d_'or'_a)_=_d_'or'_(B_INF_a)_&_B_SUP_(d_'&'_a)_=_d_'&'_(B_SUP_a)_&_B_SUP_(a_'&'_d)_=_(B_SUP_a)_'&'_d_)_)_)_)
percases ( ( ( for x being Element of Y holds d . x = TRUE ) & not for x being Element of Y holds d . x = FALSE ) or ( ( for x being Element of Y holds d . x = FALSE ) & not for x being Element of Y holds d . x = TRUE ) or ( ( for x being Element of Y holds d . x = TRUE ) & ( for x being Element of Y holds d . x = FALSE ) ) ) by A5;
caseA6: ( ( for x being Element of Y holds d . x = TRUE ) & not for x being Element of Y holds d . x = FALSE ) ; ::_thesis: ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d )
A7: now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_or_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_)_implies_(_B_INF_(d_'or'_a)_=_d_'or'_(B_INF_a)_&_B_SUP_(d_'&'_a)_=_d_'&'_(B_SUP_a)_&_B_SUP_(a_'&'_d)_=_(B_SUP_a)_'&'_d_)_)
assume A8: ( for x being Element of Y holds a . x = TRUE or for x being Element of Y holds a . x = FALSE ) ; ::_thesis: ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d )
now__::_thesis:_(_(_(_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_)_&_not_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_&_B_INF_(d_'or'_a)_=_d_'or'_(B_INF_a)_&_B_SUP_(d_'&'_a)_=_d_'&'_(B_SUP_a)_&_B_SUP_(a_'&'_d)_=_(B_SUP_a)_'&'_d_)_or_(_(_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_)_&_not_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_&_B_INF_(d_'or'_a)_=_d_'or'_(B_INF_a)_&_B_SUP_(d_'&'_a)_=_d_'&'_(B_SUP_a)_&_B_SUP_(a_'&'_d)_=_(B_SUP_a)_'&'_d_)_or_(_(_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_)_&_(_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_)_&_B_INF_(d_'or'_a)_=_d_'or'_(B_INF_a)_&_B_SUP_(d_'&'_a)_=_d_'&'_(B_SUP_a)_&_B_SUP_(a_'&'_d)_=_(B_SUP_a)_'&'_d_)_)
percases ( ( ( for x being Element of Y holds a . x = TRUE ) & not for x being Element of Y holds a . x = FALSE ) or ( ( for x being Element of Y holds a . x = FALSE ) & not for x being Element of Y holds a . x = TRUE ) or ( ( for x being Element of Y holds a . x = FALSE ) & ( for x being Element of Y holds a . x = TRUE ) ) ) by A8;
caseA9: ( ( for x being Element of Y holds a . x = TRUE ) & not for x being Element of Y holds a . x = FALSE ) ; ::_thesis: ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d )
A10: for x being Element of Y holds (d '&' a) . x = TRUE
proof
let x be Element of Y; ::_thesis: (d '&' a) . x = TRUE
( d . x = TRUE & a . x = TRUE ) by A6, A9;
then (d '&' a) . x = TRUE '&' TRUE by MARGREL1:def_20;
hence (d '&' a) . x = TRUE ; ::_thesis: verum
end;
A11: now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_(d_'&'_a)_._x_=_FALSE_)_implies_for_x_being_Element_of_Y_holds_contradiction_)
assume A12: for x being Element of Y holds (d '&' a) . x = FALSE ; ::_thesis: for x being Element of Y holds contradiction
let x be Element of Y; ::_thesis: contradiction
(d '&' a) . x = TRUE by A10;
hence contradiction by A12; ::_thesis: verum
end;
A13: for x being Element of Y holds (d 'or' a) . x = TRUE
proof
let x be Element of Y; ::_thesis: (d 'or' a) . x = TRUE
( (d 'or' a) . x = (d . x) 'or' (a . x) & a . x = TRUE ) by A9, Def4;
hence (d 'or' a) . x = TRUE ; ::_thesis: verum
end;
A14: ( B_INF a = I_el Y & B_SUP a = I_el Y ) by A9, Def13, Def14;
( B_INF d = I_el Y & B_SUP d = I_el Y ) by A6, Def13, Def14;
hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) by A1, A2, A13, A11, A14, Def13, Def14; ::_thesis: verum
end;
caseA15: ( ( for x being Element of Y holds a . x = FALSE ) & not for x being Element of Y holds a . x = TRUE ) ; ::_thesis: ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d )
A16: for x being Element of Y holds (d '&' a) . x = FALSE
proof
let x be Element of Y; ::_thesis: (d '&' a) . x = FALSE
( (d '&' a) . x = (d . x) '&' (a . x) & a . x = FALSE ) by A15, MARGREL1:def_20;
hence (d '&' a) . x = FALSE ; ::_thesis: verum
end;
A17: for x being Element of Y holds (d 'or' a) . x = TRUE
proof
let x be Element of Y; ::_thesis: (d 'or' a) . x = TRUE
( (d 'or' a) . x = (d . x) 'or' (a . x) & d . x = TRUE ) by A6, Def4;
hence (d 'or' a) . x = TRUE ; ::_thesis: verum
end;
B_SUP a = O_el Y by A15, Def14;
then A18: d '&' (B_SUP a) = O_el Y by Th5;
A19: B_INF a = O_el Y by A15, Def13;
B_INF d = I_el Y by A6, Def13;
then d 'or' (B_INF a) = I_el Y by A1, A19, Th9;
hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) by A17, A16, A18, Def13, Def14; ::_thesis: verum
end;
caseA20: ( ( for x being Element of Y holds a . x = FALSE ) & ( for x being Element of Y holds a . x = TRUE ) ) ; ::_thesis: ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d )
A21: for x being Element of Y holds (d '&' a) . x = FALSE
proof
let x be Element of Y; ::_thesis: (d '&' a) . x = FALSE
( d . x = TRUE & a . x = FALSE ) by A6, A20;
then (d '&' a) . x = TRUE '&' FALSE by MARGREL1:def_20;
hence (d '&' a) . x = FALSE ; ::_thesis: verum
end;
A22: for x being Element of Y holds (d 'or' a) . x = TRUE
proof
let x be Element of Y; ::_thesis: (d 'or' a) . x = TRUE
( d . x = TRUE & a . x = FALSE ) by A6, A20;
then (d 'or' a) . x = TRUE 'or' FALSE by Def4;
hence (d 'or' a) . x = TRUE ; ::_thesis: verum
end;
B_SUP a = O_el Y by A20, Def14;
then A23: d '&' (B_SUP a) = O_el Y by Th5;
B_INF d = I_el Y by A6, Def13;
then d 'or' (B_INF a) = I_el Y by A1, Th10;
hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) by A22, A21, A23, Def13, Def14; ::_thesis: verum
end;
end;
end;
hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) ; ::_thesis: verum
end;
now__::_thesis:_(_not_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_&_not_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_implies_(_B_INF_(d_'or'_a)_=_d_'or'_(B_INF_a)_&_B_SUP_(d_'&'_a)_=_d_'&'_(B_SUP_a)_&_B_SUP_(a_'&'_d)_=_(B_SUP_a)_'&'_d_)_)
assume that
A24: not for x being Element of Y holds a . x = TRUE and
not for x being Element of Y holds a . x = FALSE ; ::_thesis: ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d )
A25: B_INF a = O_el Y by A24, Def13;
B_INF d = I_el Y by A6, Def13;
then A26: d 'or' (B_INF a) = I_el Y by A1, A25, Th9;
A27: d = I_el Y by A3, A6, Def13;
A28: for x being Element of Y holds (d 'or' a) . x = TRUE by A27, Th10, Def11;
A33: d '&' a = a
proof
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (d '&' a) . x = a . x
(d '&' a) . x = ((I_el Y) . x) '&' (a . x) by A27, MARGREL1:def_20;
then (d '&' a) . x = TRUE '&' (a . x) by Def11;
hence (d '&' a) . x = a . x ; ::_thesis: verum
end;
B_SUP d = I_el Y by A6, Def14;
hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) by A2, A28, A33, A26, Def13, Th6; ::_thesis: verum
end;
hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) by A7; ::_thesis: verum
end;
caseA34: ( ( for x being Element of Y holds d . x = FALSE ) & not for x being Element of Y holds d . x = TRUE ) ; ::_thesis: ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d )
A35: now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_or_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_)_implies_(_B_INF_(d_'or'_a)_=_d_'or'_(B_INF_a)_&_B_SUP_(d_'&'_a)_=_d_'&'_(B_SUP_a)_&_B_SUP_(a_'&'_d)_=_(B_SUP_a)_'&'_d_)_)
assume A36: ( for x being Element of Y holds a . x = TRUE or for x being Element of Y holds a . x = FALSE ) ; ::_thesis: ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d )
now__::_thesis:_(_(_(_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_)_&_not_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_&_B_INF_(d_'or'_a)_=_d_'or'_(B_INF_a)_&_B_SUP_(d_'&'_a)_=_d_'&'_(B_SUP_a)_&_B_SUP_(a_'&'_d)_=_(B_SUP_a)_'&'_d_)_or_(_(_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_)_&_not_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_&_B_INF_(d_'or'_a)_=_d_'or'_(B_INF_a)_&_B_SUP_(d_'&'_a)_=_d_'&'_(B_SUP_a)_&_B_SUP_(a_'&'_d)_=_(B_SUP_a)_'&'_d_)_or_(_(_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_)_&_(_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_)_&_B_INF_(d_'or'_a)_=_d_'or'_(B_INF_a)_&_B_SUP_(d_'&'_a)_=_d_'&'_(B_SUP_a)_&_B_SUP_(a_'&'_d)_=_(B_SUP_a)_'&'_d_)_)
percases ( ( ( for x being Element of Y holds a . x = TRUE ) & not for x being Element of Y holds a . x = FALSE ) or ( ( for x being Element of Y holds a . x = FALSE ) & not for x being Element of Y holds a . x = TRUE ) or ( ( for x being Element of Y holds a . x = FALSE ) & ( for x being Element of Y holds a . x = TRUE ) ) ) by A36;
caseA37: ( ( for x being Element of Y holds a . x = TRUE ) & not for x being Element of Y holds a . x = FALSE ) ; ::_thesis: ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d )
A38: for x being Element of Y holds (d 'or' a) . x = TRUE
proof
let x be Element of Y; ::_thesis: (d 'or' a) . x = TRUE
( (d 'or' a) . x = (d . x) 'or' (a . x) & d . x = FALSE ) by A34, Def4;
hence (d 'or' a) . x = TRUE by A37; ::_thesis: verum
end;
B_SUP d = O_el Y by A34, Def14;
then A39: d '&' (B_SUP a) = O_el Y by A2, Th5;
A40: for x being Element of Y holds (d '&' a) . x = FALSE
proof
let x be Element of Y; ::_thesis: (d '&' a) . x = FALSE
( (d '&' a) . x = (d . x) '&' (a . x) & d . x = FALSE ) by A34, MARGREL1:def_20;
hence (d '&' a) . x = FALSE ; ::_thesis: verum
end;
A41: B_INF a = I_el Y by A37, Def13;
B_INF d = O_el Y by A34, Def13;
then d 'or' (B_INF a) = I_el Y by A1, A41, Th9;
hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) by A38, A40, A39, Def13, Def14; ::_thesis: verum
end;
caseA42: ( ( for x being Element of Y holds a . x = FALSE ) & not for x being Element of Y holds a . x = TRUE ) ; ::_thesis: ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d )
A43: for x being Element of Y holds (d 'or' a) . x = FALSE
proof
let x be Element of Y; ::_thesis: (d 'or' a) . x = FALSE
( d . x = FALSE & a . x = FALSE ) by A34, A42;
then (d 'or' a) . x = FALSE 'or' FALSE by Def4;
hence (d 'or' a) . x = FALSE ; ::_thesis: verum
end;
A44: now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_(d_'or'_a)_._x_=_TRUE_)_implies_for_x_being_Element_of_Y_holds_contradiction_)
assume A45: for x being Element of Y holds (d 'or' a) . x = TRUE ; ::_thesis: for x being Element of Y holds contradiction
let x be Element of Y; ::_thesis: contradiction
(d 'or' a) . x = FALSE by A43;
hence contradiction by A45; ::_thesis: verum
end;
B_SUP d = O_el Y by A34, Def14;
then A46: d '&' (B_SUP a) = O_el Y by A2, Th5;
A47: for x being Element of Y holds (d '&' a) . x = FALSE
proof
let x be Element of Y; ::_thesis: (d '&' a) . x = FALSE
( d . x = FALSE & a . x = FALSE ) by A34, A42;
then (d '&' a) . x = FALSE '&' FALSE by MARGREL1:def_20;
hence (d '&' a) . x = FALSE ; ::_thesis: verum
end;
A48: B_INF a = O_el Y by A42, Def13;
B_INF d = O_el Y by A34, Def13;
hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) by A1, A44, A47, A48, A46, Def13, Def14; ::_thesis: verum
end;
caseA49: ( ( for x being Element of Y holds a . x = FALSE ) & ( for x being Element of Y holds a . x = TRUE ) ) ; ::_thesis: ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d )
A50: for x being Element of Y holds (d 'or' a) . x = TRUE
proof
let x be Element of Y; ::_thesis: (d 'or' a) . x = TRUE
( d . x = FALSE & a . x = TRUE ) by A34, A49;
then (d 'or' a) . x = FALSE 'or' TRUE by Def4;
hence (d 'or' a) . x = TRUE ; ::_thesis: verum
end;
B_SUP d = O_el Y by A34, Def14;
then A51: d '&' (B_SUP a) = O_el Y by A2, Th5;
A52: for x being Element of Y holds (d '&' a) . x = FALSE
proof
let x be Element of Y; ::_thesis: (d '&' a) . x = FALSE
( d . x = FALSE & a . x = TRUE ) by A34, A49;
then (d '&' a) . x = FALSE '&' TRUE by MARGREL1:def_20;
hence (d '&' a) . x = FALSE ; ::_thesis: verum
end;
A53: B_INF a = I_el Y by A49, Def13;
B_INF d = O_el Y by A34, Def13;
then d 'or' (B_INF a) = I_el Y by A1, A53, Th9;
hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) by A50, A52, A51, Def13, Def14; ::_thesis: verum
end;
end;
end;
hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) ; ::_thesis: verum
end;
now__::_thesis:_(_not_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_&_not_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_implies_(_B_INF_(d_'or'_a)_=_d_'or'_(B_INF_a)_&_B_SUP_(d_'&'_a)_=_d_'&'_(B_SUP_a)_&_B_SUP_(a_'&'_d)_=_(B_SUP_a)_'&'_d_)_)
for x being Element of Y holds (d '&' a) . x = FALSE
proof
let x be Element of Y; ::_thesis: (d '&' a) . x = FALSE
(d '&' a) . x = ((O_el Y) '&' a) . x by A3, A34, Def13;
hence (d '&' a) . x = FALSE by Def10, Th5; ::_thesis: verum
end;
then A54: B_SUP (d '&' a) = O_el Y by Def14;
assume that
A55: not for x being Element of Y holds a . x = TRUE and
not for x being Element of Y holds a . x = FALSE ; ::_thesis: ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d )
B_INF d = O_el Y by A34, Def13;
then A56: d 'or' (B_INF a) = (O_el Y) 'or' (O_el Y) by A1, A55, Def13;
A61: d 'or' a = a
proof
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (d 'or' a) . x = a . x
(d 'or' a) . x = (d . x) 'or' (a . x) by Def4;
then (d 'or' a) . x = FALSE 'or' (a . x) by A34;
hence (d 'or' a) . x = a . x ; ::_thesis: verum
end;
B_SUP d = O_el Y by A34, Def14;
hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) by A2, A55, A61, A54, A56, Def13, Th5; ::_thesis: verum
end;
hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) by A35; ::_thesis: verum
end;
caseA62: ( ( for x being Element of Y holds d . x = TRUE ) & ( for x being Element of Y holds d . x = FALSE ) ) ; ::_thesis: for x being Element of Y holds
( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d )
let x be Element of Y; ::_thesis: ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d )
d . x = FALSE by A62;
hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) by A62; ::_thesis: verum
end;
end;
end;
hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) ; ::_thesis: verum
end;
now__::_thesis:_(_not_for_x_being_Element_of_Y_holds_d_._x_=_TRUE_&_not_for_x_being_Element_of_Y_holds_d_._x_=_FALSE_implies_(_B_INF_(d_'or'_a)_=_d_'or'_(B_INF_a)_&_B_SUP_(d_'&'_a)_=_d_'&'_(B_SUP_a)_&_B_SUP_(a_'&'_d)_=_(B_SUP_a)_'&'_d_)_)
assume that
A63: not for x being Element of Y holds d . x = TRUE and
A64: not for x being Element of Y holds d . x = FALSE ; ::_thesis: ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d )
now__::_thesis:_(_(_d_=_O_el_Y_&_B_INF_(d_'or'_a)_=_d_'or'_(B_INF_a)_&_B_SUP_(d_'&'_a)_=_d_'&'_(B_SUP_a)_&_B_SUP_(a_'&'_d)_=_(B_SUP_a)_'&'_d_)_or_(_d_=_I_el_Y_&_B_INF_(d_'or'_a)_=_d_'or'_(B_INF_a)_&_B_SUP_(d_'&'_a)_=_d_'&'_(B_SUP_a)_&_B_SUP_(a_'&'_d)_=_(B_SUP_a)_'&'_d_)_)
percases ( d = O_el Y or d = I_el Y ) by Th21;
case d = O_el Y ; ::_thesis: ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d )
hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) by A64, Def10; ::_thesis: verum
end;
case d = I_el Y ; ::_thesis: ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d )
hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) by A63, Def11; ::_thesis: verum
end;
end;
end;
hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) ; ::_thesis: verum
end;
hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) by A4; ::_thesis: verum
end;
theorem :: BVFUNC_1:26
for Y being non empty set
for a being Function of Y,BOOLEAN
for x being Element of Y holds (B_INF a) . x <= a . x
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN
for x being Element of Y holds (B_INF a) . x <= a . x
let a be Function of Y,BOOLEAN; ::_thesis: for x being Element of Y holds (B_INF a) . x <= a . x
let x be Element of Y; ::_thesis: (B_INF a) . x <= a . x
A1: now__::_thesis:_(_not_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_implies_(B_INF_a)_._x_<=_a_._x_)
assume not for x being Element of Y holds a . x = TRUE ; ::_thesis: (B_INF a) . x <= a . x
then B_INF a = O_el Y by Def13;
then (B_INF a) . x = FALSE by Def10;
then ((B_INF a) . x) => (a . x) = TRUE ;
hence (B_INF a) . x <= a . x by Def1; ::_thesis: verum
end;
now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_)_implies_(B_INF_a)_._x_<=_a_._x_)
assume for x being Element of Y holds a . x = TRUE ; ::_thesis: (B_INF a) . x <= a . x
then a . x = TRUE ;
then ((B_INF a) . x) => (a . x) = TRUE ;
hence (B_INF a) . x <= a . x by Def1; ::_thesis: verum
end;
hence (B_INF a) . x <= a . x by A1; ::_thesis: verum
end;
theorem :: BVFUNC_1:27
for Y being non empty set
for a being Function of Y,BOOLEAN
for x being Element of Y holds a . x <= (B_SUP a) . x
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN
for x being Element of Y holds a . x <= (B_SUP a) . x
let a be Function of Y,BOOLEAN; ::_thesis: for x being Element of Y holds a . x <= (B_SUP a) . x
let x be Element of Y; ::_thesis: a . x <= (B_SUP a) . x
A1: now__::_thesis:_(_not_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_implies_a_._x_<=_(B_SUP_a)_._x_)
assume not for x being Element of Y holds a . x = FALSE ; ::_thesis: a . x <= (B_SUP a) . x
then B_SUP a = I_el Y by Def14;
then (B_SUP a) . x = TRUE by Def11;
then (a . x) => ((B_SUP a) . x) = TRUE ;
hence a . x <= (B_SUP a) . x by Def1; ::_thesis: verum
end;
now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_)_implies_a_._x_<=_(B_SUP_a)_._x_)
assume for x being Element of Y holds a . x = FALSE ; ::_thesis: a . x <= (B_SUP a) . x
then a . x = FALSE ;
then (a . x) => ((B_SUP a) . x) = TRUE ;
hence a . x <= (B_SUP a) . x by Def1; ::_thesis: verum
end;
hence a . x <= (B_SUP a) . x by A1; ::_thesis: verum
end;
begin
definition
let Y be non empty set ;
let a be Function of Y,BOOLEAN;
let PA be a_partition of Y;
preda is_dependent_of PA means :Def15: :: BVFUNC_1:def 15
for F being set st F in PA holds
for x1, x2 being set st x1 in F & x2 in F holds
a . x1 = a . x2;
end;
:: deftheorem Def15 defines is_dependent_of BVFUNC_1:def_15_:_
for Y being non empty set
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds
( a is_dependent_of PA iff for F being set st F in PA holds
for x1, x2 being set st x1 in F & x2 in F holds
a . x1 = a . x2 );
theorem :: BVFUNC_1:28
for Y being non empty set
for a being Function of Y,BOOLEAN holds a is_dependent_of %I Y
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a is_dependent_of %I Y
let a be Function of Y,BOOLEAN; ::_thesis: a is_dependent_of %I Y
for F being set st F in %I Y holds
for x1, x2 being set st x1 in F & x2 in F holds
a . x1 = a . x2
proof
let F be set ; ::_thesis: ( F in %I Y implies for x1, x2 being set st x1 in F & x2 in F holds
a . x1 = a . x2 )
assume F in %I Y ; ::_thesis: for x1, x2 being set st x1 in F & x2 in F holds
a . x1 = a . x2
then F in { B where B is Subset of Y : ex z being set st
( B = {z} & z in Y ) } by PARTIT1:31;
then ex B being Subset of Y st
( F = B & ex z being set st
( B = {z} & z in Y ) ) ;
then consider z being set such that
A1: F = {z} and
z in Y ;
let x1, x2 be set ; ::_thesis: ( x1 in F & x2 in F implies a . x1 = a . x2 )
assume that
A2: x1 in F and
A3: x2 in F ; ::_thesis: a . x1 = a . x2
x1 = z by A1, A2, TARSKI:def_1;
hence a . x1 = a . x2 by A1, A3, TARSKI:def_1; ::_thesis: verum
end;
hence a is_dependent_of %I Y by Def15; ::_thesis: verum
end;
theorem :: BVFUNC_1:29
for Y being non empty set
for a being constant Function of Y,BOOLEAN holds a is_dependent_of %O Y
proof
let Y be non empty set ; ::_thesis: for a being constant Function of Y,BOOLEAN holds a is_dependent_of %O Y
let a be constant Function of Y,BOOLEAN; ::_thesis: a is_dependent_of %O Y
for F being set st F in %O Y holds
for x1, x2 being set st x1 in F & x2 in F holds
a . x1 = a . x2
proof
let F be set ; ::_thesis: ( F in %O Y implies for x1, x2 being set st x1 in F & x2 in F holds
a . x1 = a . x2 )
for x1, x2 being Element of Y holds a . x1 = a . x2
proof
let x1, x2 be Element of Y; ::_thesis: a . x1 = a . x2
percases ( a = O_el Y or a = I_el Y ) by Th21;
supposeA2: a = O_el Y ; ::_thesis: a . x1 = a . x2
then a . x1 = FALSE by Def10;
hence a . x1 = a . x2 by A2, Def10; ::_thesis: verum
end;
supposeA3: a = I_el Y ; ::_thesis: a . x1 = a . x2
then a . x1 = TRUE by Def11;
hence a . x1 = a . x2 by A3, Def11; ::_thesis: verum
end;
end;
end;
hence ( F in %O Y implies for x1, x2 being set st x1 in F & x2 in F holds
a . x1 = a . x2 ) ; ::_thesis: verum
end;
hence a is_dependent_of %O Y by Def15; ::_thesis: verum
end;
definition
let Y be non empty set ;
let PA be a_partition of Y;
:: original: Element
redefine mode Element of PA -> Subset of Y;
coherence
for b1 being Element of PA holds b1 is Subset of Y
proof
let x be Element of PA; ::_thesis: x is Subset of Y
thus x is Subset of Y ; ::_thesis: verum
end;
end;
definition
let Y be non empty set ;
let x be Element of Y;
let PA be a_partition of Y;
:: original: EqClass
redefine func EqClass (x,PA) -> Element of PA;
coherence
EqClass (x,PA) is Element of PA by EQREL_1:def_6;
end;
definition
let Y be non empty set ;
let a be Function of Y,BOOLEAN;
let PA be a_partition of Y;
func B_INF (a,PA) -> Function of Y,BOOLEAN means :Def16: :: BVFUNC_1:def 16
for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ) implies it . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) implies it . y = FALSE ) );
existence
ex b1 being Function of Y,BOOLEAN st
for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ) implies b1 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) implies b1 . y = FALSE ) )
proof
defpred S1[ Element of Y, set ] means ( ( ( for x being Element of Y st x in EqClass ($1,PA) holds
a . x = TRUE ) implies $2 = TRUE ) & ( ex x being Element of Y st
( x in EqClass ($1,PA) & not a . x = TRUE ) implies $2 = FALSE ) );
A1: for e being Element of Y ex u being Element of BOOLEAN st S1[e,u]
proof
let e be Element of Y; ::_thesis: ex u being Element of BOOLEAN st S1[e,u]
percases ( for x being Element of Y st x in EqClass (e,PA) holds
a . x = TRUE or ex x being Element of Y st
( x in EqClass (e,PA) & not a . x = TRUE ) ) ;
suppose for x being Element of Y st x in EqClass (e,PA) holds
a . x = TRUE ; ::_thesis: ex u being Element of BOOLEAN st S1[e,u]
hence ex u being Element of BOOLEAN st S1[e,u] ; ::_thesis: verum
end;
suppose ex x being Element of Y st
( x in EqClass (e,PA) & not a . x = TRUE ) ; ::_thesis: ex u being Element of BOOLEAN st S1[e,u]
hence ex u being Element of BOOLEAN st S1[e,u] ; ::_thesis: verum
end;
end;
end;
consider f being Function of Y,BOOLEAN such that
A2: for e being Element of Y holds S1[e,f . e] from FUNCT_2:sch_3(A1);
reconsider f = f as Function of Y,BOOLEAN ;
reconsider f = f as Function of Y,BOOLEAN ;
take f ; ::_thesis: for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ) implies f . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) implies f . y = FALSE ) )
thus for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ) implies f . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) implies f . y = FALSE ) ) by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of Y,BOOLEAN st ( for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ) implies b1 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) implies b1 . y = FALSE ) ) ) & ( for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ) implies b2 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) implies b2 . y = FALSE ) ) ) holds
b1 = b2
proof
let A1, A2 be Function of Y,BOOLEAN; ::_thesis: ( ( for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ) implies A1 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) implies A1 . y = FALSE ) ) ) & ( for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ) implies A2 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) implies A2 . y = FALSE ) ) ) implies A1 = A2 )
assume that
A3: for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ) implies A1 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) implies A1 . y = FALSE ) ) and
A4: for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ) implies A2 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) implies A2 . y = FALSE ) ) ; ::_thesis: A1 = A2
let y be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: A1 . y = A2 . y
A9: now__::_thesis:_(_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(y,PA)_&_not_a_._x_=_TRUE_)_implies_A1_._y_=_A2_._y_)
assume A10: ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) ; ::_thesis: A1 . y = A2 . y
then A2 . y = FALSE by A4;
hence A1 . y = A2 . y by A3, A10; ::_thesis: verum
end;
now__::_thesis:_(_(_for_x_being_Element_of_Y_st_x_in_EqClass_(y,PA)_holds_
a_._x_=_TRUE_)_implies_A1_._y_=_A2_._y_)
assume A11: for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ; ::_thesis: A1 . y = A2 . y
then A2 . y = TRUE by A4;
hence A1 . y = A2 . y by A3, A11; ::_thesis: verum
end;
hence A1 . y = A2 . y by A9; ::_thesis: verum
end;
end;
:: deftheorem Def16 defines B_INF BVFUNC_1:def_16_:_
for Y being non empty set
for a being Function of Y,BOOLEAN
for PA being a_partition of Y
for b4 being Function of Y,BOOLEAN holds
( b4 = B_INF (a,PA) iff for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ) implies b4 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) implies b4 . y = FALSE ) ) );
definition
let Y be non empty set ;
let a be Function of Y,BOOLEAN;
let PA be a_partition of Y;
func B_SUP (a,PA) -> Function of Y,BOOLEAN means :Def17: :: BVFUNC_1:def 17
for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) implies it . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies it . y = FALSE ) );
existence
ex b1 being Function of Y,BOOLEAN st
for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) implies b1 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies b1 . y = FALSE ) )
proof
defpred S1[ Element of Y, set ] means ( ( ex x being Element of Y st
( x in EqClass ($1,PA) & a . x = TRUE ) implies $2 = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass ($1,PA) or not a . x = TRUE ) ) implies $2 = FALSE ) );
A1: for e being Element of Y ex u being Element of BOOLEAN st S1[e,u]
proof
let e be Element of Y; ::_thesis: ex u being Element of BOOLEAN st S1[e,u]
percases ( ex x being Element of Y st
( x in EqClass (e,PA) & a . x = TRUE ) or for x being Element of Y holds
( not x in EqClass (e,PA) or not a . x = TRUE ) ) ;
suppose ex x being Element of Y st
( x in EqClass (e,PA) & a . x = TRUE ) ; ::_thesis: ex u being Element of BOOLEAN st S1[e,u]
hence ex u being Element of BOOLEAN st S1[e,u] ; ::_thesis: verum
end;
suppose for x being Element of Y holds
( not x in EqClass (e,PA) or not a . x = TRUE ) ; ::_thesis: ex u being Element of BOOLEAN st S1[e,u]
hence ex u being Element of BOOLEAN st S1[e,u] ; ::_thesis: verum
end;
end;
end;
consider f being Function of Y,BOOLEAN such that
A2: for e being Element of Y holds S1[e,f . e] from FUNCT_2:sch_3(A1);
reconsider f = f as Function of Y,BOOLEAN ;
reconsider f = f as Function of Y,BOOLEAN ;
take f ; ::_thesis: for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) implies f . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies f . y = FALSE ) )
thus for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) implies f . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies f . y = FALSE ) ) by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of Y,BOOLEAN st ( for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) implies b1 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies b1 . y = FALSE ) ) ) & ( for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) implies b2 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies b2 . y = FALSE ) ) ) holds
b1 = b2
proof
let A1, A2 be Function of Y,BOOLEAN; ::_thesis: ( ( for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) implies A1 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies A1 . y = FALSE ) ) ) & ( for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) implies A2 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies A2 . y = FALSE ) ) ) implies A1 = A2 )
assume that
A3: for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) implies A1 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies A1 . y = FALSE ) ) and
A4: for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) implies A2 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies A2 . y = FALSE ) ) ; ::_thesis: A1 = A2
let y be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: A1 . y = A2 . y
A9: now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_
(_not_x_in_EqClass_(y,PA)_or_not_a_._x_=_TRUE_)_)_implies_A1_._y_=_A2_._y_)
assume A10: for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ; ::_thesis: A1 . y = A2 . y
then A2 . y = FALSE by A4;
hence A1 . y = A2 . y by A3, A10; ::_thesis: verum
end;
now__::_thesis:_(_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(y,PA)_&_a_._x_=_TRUE_)_implies_A1_._y_=_A2_._y_)
assume A11: ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) ; ::_thesis: A1 . y = A2 . y
then A2 . y = TRUE by A4;
hence A1 . y = A2 . y by A3, A11; ::_thesis: verum
end;
hence A1 . y = A2 . y by A9; ::_thesis: verum
end;
end;
:: deftheorem Def17 defines B_SUP BVFUNC_1:def_17_:_
for Y being non empty set
for a being Function of Y,BOOLEAN
for PA being a_partition of Y
for b4 being Function of Y,BOOLEAN holds
( b4 = B_SUP (a,PA) iff for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) implies b4 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies b4 . y = FALSE ) ) );
theorem :: BVFUNC_1:30
for Y being non empty set
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds B_INF (a,PA) is_dependent_of PA
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds B_INF (a,PA) is_dependent_of PA
let a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds B_INF (a,PA) is_dependent_of PA
let PA be a_partition of Y; ::_thesis: B_INF (a,PA) is_dependent_of PA
for F being set st F in PA holds
for x1, x2 being set st x1 in F & x2 in F holds
(B_INF (a,PA)) . x1 = (B_INF (a,PA)) . x2
proof
let F be set ; ::_thesis: ( F in PA implies for x1, x2 being set st x1 in F & x2 in F holds
(B_INF (a,PA)) . x1 = (B_INF (a,PA)) . x2 )
assume A1: F in PA ; ::_thesis: for x1, x2 being set st x1 in F & x2 in F holds
(B_INF (a,PA)) . x1 = (B_INF (a,PA)) . x2
let x1, x2 be set ; ::_thesis: ( x1 in F & x2 in F implies (B_INF (a,PA)) . x1 = (B_INF (a,PA)) . x2 )
assume that
A2: x1 in F and
A3: x2 in F ; ::_thesis: (B_INF (a,PA)) . x1 = (B_INF (a,PA)) . x2
reconsider x1 = x1 as Element of Y by A1, A2;
A4: ( EqClass (x1,PA) = F or EqClass (x1,PA) misses F ) by A1, EQREL_1:def_4;
reconsider x2 = x2 as Element of Y by A1, A3;
A5: ( x1 in EqClass (x1,PA) & EqClass (x2,PA) = F ) by A1, EQREL_1:def_6, A3;
percases ( for x being Element of Y st x in EqClass (x1,PA) holds
a . x = TRUE or ex x being Element of Y st
( x in EqClass (x1,PA) & not a . x = TRUE ) ) ;
supposeA6: for x being Element of Y st x in EqClass (x1,PA) holds
a . x = TRUE ; ::_thesis: (B_INF (a,PA)) . x1 = (B_INF (a,PA)) . x2
then (B_INF (a,PA)) . x1 = TRUE by Def16;
hence (B_INF (a,PA)) . x1 = (B_INF (a,PA)) . x2 by A2, A4, A5, A6, Def16, XBOOLE_0:3; ::_thesis: verum
end;
supposeA7: ex x being Element of Y st
( x in EqClass (x1,PA) & not a . x = TRUE ) ; ::_thesis: (B_INF (a,PA)) . x1 = (B_INF (a,PA)) . x2
then (B_INF (a,PA)) . x1 = FALSE by Def16;
hence (B_INF (a,PA)) . x1 = (B_INF (a,PA)) . x2 by A2, A4, A5, A7, Def16, XBOOLE_0:3; ::_thesis: verum
end;
end;
end;
hence B_INF (a,PA) is_dependent_of PA by Def15; ::_thesis: verum
end;
theorem :: BVFUNC_1:31
for Y being non empty set
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds B_SUP (a,PA) is_dependent_of PA
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds B_SUP (a,PA) is_dependent_of PA
let a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds B_SUP (a,PA) is_dependent_of PA
let PA be a_partition of Y; ::_thesis: B_SUP (a,PA) is_dependent_of PA
for F being set st F in PA holds
for x1, x2 being set st x1 in F & x2 in F holds
(B_SUP (a,PA)) . x1 = (B_SUP (a,PA)) . x2
proof
let F be set ; ::_thesis: ( F in PA implies for x1, x2 being set st x1 in F & x2 in F holds
(B_SUP (a,PA)) . x1 = (B_SUP (a,PA)) . x2 )
assume A1: F in PA ; ::_thesis: for x1, x2 being set st x1 in F & x2 in F holds
(B_SUP (a,PA)) . x1 = (B_SUP (a,PA)) . x2
let x1, x2 be set ; ::_thesis: ( x1 in F & x2 in F implies (B_SUP (a,PA)) . x1 = (B_SUP (a,PA)) . x2 )
assume A2: ( x1 in F & x2 in F ) ; ::_thesis: (B_SUP (a,PA)) . x1 = (B_SUP (a,PA)) . x2
then reconsider x1 = x1, x2 = x2 as Element of Y by A1;
A3: x1 in EqClass (x1,PA) by EQREL_1:def_6;
( EqClass (x1,PA) = F or EqClass (x1,PA) misses F ) by A1, EQREL_1:def_4;
then A4: EqClass (x2,PA) = EqClass (x1,PA) by A2, A3, EQREL_1:def_6, XBOOLE_0:3;
percases ( ex x being Element of Y st
( x in EqClass (x1,PA) & a . x = TRUE ) or for x being Element of Y holds
( not x in EqClass (x1,PA) or not a . x = TRUE ) ) ;
supposeA5: ex x being Element of Y st
( x in EqClass (x1,PA) & a . x = TRUE ) ; ::_thesis: (B_SUP (a,PA)) . x1 = (B_SUP (a,PA)) . x2
then (B_SUP (a,PA)) . x1 = TRUE by Def17;
hence (B_SUP (a,PA)) . x1 = (B_SUP (a,PA)) . x2 by A4, A5, Def17; ::_thesis: verum
end;
supposeA6: for x being Element of Y holds
( not x in EqClass (x1,PA) or not a . x = TRUE ) ; ::_thesis: (B_SUP (a,PA)) . x1 = (B_SUP (a,PA)) . x2
then (B_SUP (a,PA)) . x1 = FALSE by Def17;
hence (B_SUP (a,PA)) . x1 = (B_SUP (a,PA)) . x2 by A4, A6, Def17; ::_thesis: verum
end;
end;
end;
hence B_SUP (a,PA) is_dependent_of PA by Def15; ::_thesis: verum
end;
theorem :: BVFUNC_1:32
for Y being non empty set
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds B_INF (a,PA) '<' a
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds B_INF (a,PA) '<' a
let a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds B_INF (a,PA) '<' a
let PA be a_partition of Y; ::_thesis: B_INF (a,PA) '<' a
(B_INF (a,PA)) 'imp' a = I_el Y
proof
let y be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((B_INF (a,PA)) 'imp' a) . y = (I_el Y) . y
percases ( for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE or ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) ) ;
supposeA5: for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ; ::_thesis: ((B_INF (a,PA)) 'imp' a) . y = (I_el Y) . y
A6: a . y = TRUE by A5, EQREL_1:def_6;
'not' ((B_INF (a,PA)) . y) = ('not' (B_INF (a,PA))) . y by MARGREL1:def_19;
then ('not' ((B_INF (a,PA)) . y)) 'or' (a . y) = (('not' (B_INF (a,PA))) . y) 'or' ((I_el Y) . y) by A6, Def11
.= (('not' (B_INF (a,PA))) 'or' (I_el Y)) . y by Def4
.= (I_el Y) . y by Th10 ;
hence ((B_INF (a,PA)) 'imp' a) . y = (I_el Y) . y by Def8; ::_thesis: verum
end;
suppose ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) ; ::_thesis: ((B_INF (a,PA)) 'imp' a) . y = (I_el Y) . y
then (B_INF (a,PA)) . y = FALSE by Def16;
then ('not' ((B_INF (a,PA)) . y)) 'or' (a . y) = ((I_el Y) . y) 'or' (a . y) by Def11
.= ((I_el Y) 'or' a) . y by Def4
.= (I_el Y) . y by Th10 ;
hence ((B_INF (a,PA)) 'imp' a) . y = (I_el Y) . y by Def8; ::_thesis: verum
end;
end;
end;
hence B_INF (a,PA) '<' a by Th16; ::_thesis: verum
end;
theorem :: BVFUNC_1:33
for Y being non empty set
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds a '<' B_SUP (a,PA)
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds a '<' B_SUP (a,PA)
let a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds a '<' B_SUP (a,PA)
let PA be a_partition of Y; ::_thesis: a '<' B_SUP (a,PA)
a 'imp' (B_SUP (a,PA)) = I_el Y
proof
let y be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'imp' (B_SUP (a,PA))) . y = (I_el Y) . y
percases ( ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) or for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ) ;
suppose ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) ; ::_thesis: (a 'imp' (B_SUP (a,PA))) . y = (I_el Y) . y
then (B_SUP (a,PA)) . y = TRUE by Def17;
then (B_SUP (a,PA)) . y = (I_el Y) . y by Def11;
then ('not' (a . y)) 'or' ((B_SUP (a,PA)) . y) = (('not' a) . y) 'or' ((I_el Y) . y) by MARGREL1:def_19
.= (('not' a) 'or' (I_el Y)) . y by Def4
.= (I_el Y) . y by Th10 ;
hence (a 'imp' (B_SUP (a,PA))) . y = (I_el Y) . y by Def8; ::_thesis: verum
end;
supposeA5: for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ; ::_thesis: (a 'imp' (B_SUP (a,PA))) . y = (I_el Y) . y
a . y <> TRUE by A5, EQREL_1:def_6;
then a . y = FALSE by XBOOLEAN:def_3;
then ('not' (a . y)) 'or' ((B_SUP (a,PA)) . y) = ((I_el Y) . y) 'or' ((B_SUP (a,PA)) . y) by Def11
.= ((I_el Y) 'or' (B_SUP (a,PA))) . y by Def4
.= (I_el Y) . y by Th10 ;
hence (a 'imp' (B_SUP (a,PA))) . y = (I_el Y) . y by Def8; ::_thesis: verum
end;
end;
end;
hence a '<' B_SUP (a,PA) by Th16; ::_thesis: verum
end;
theorem :: BVFUNC_1:34
for Y being non empty set
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds 'not' (B_INF (a,PA)) = B_SUP (('not' a),PA)
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds 'not' (B_INF (a,PA)) = B_SUP (('not' a),PA)
let a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds 'not' (B_INF (a,PA)) = B_SUP (('not' a),PA)
let PA be a_partition of Y; ::_thesis: 'not' (B_INF (a,PA)) = B_SUP (('not' a),PA)
let y be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ('not' (B_INF (a,PA))) . y = (B_SUP (('not' a),PA)) . y
A5: now__::_thesis:_(_(_for_x_being_Element_of_Y_st_x_in_EqClass_(y,PA)_holds_
a_._x_=_TRUE_)_implies_for_x_being_Element_of_Y_holds_
(_not_x_in_EqClass_(y,PA)_or_not_('not'_a)_._x_=_TRUE_)_)
assume that
A6: for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE and
A7: ex x being Element of Y st
( x in EqClass (y,PA) & ('not' a) . x = TRUE ) ; ::_thesis: contradiction
consider x1 being Element of Y such that
A8: x1 in EqClass (y,PA) and
A9: ('not' a) . x1 = TRUE by A7;
('not' ('not' a)) . x1 = 'not' TRUE by A9, MARGREL1:def_19;
hence contradiction by A6, A8; ::_thesis: verum
end;
A10: now__::_thesis:_(_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(y,PA)_&_not_a_._x_=_TRUE_)_implies_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(y,PA)_&_('not'_a)_._x_=_TRUE_)_)
assume that
A11: ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) and
A12: for x being Element of Y holds
( not x in EqClass (y,PA) or not ('not' a) . x = TRUE ) ; ::_thesis: contradiction
consider x1 being Element of Y such that
A13: x1 in EqClass (y,PA) and
A14: a . x1 <> TRUE by A11;
a . x1 = FALSE by A14, XBOOLEAN:def_3;
then ('not' a) . x1 = 'not' FALSE by MARGREL1:def_19;
hence contradiction by A12, A13; ::_thesis: verum
end;
A15: now__::_thesis:_(_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(y,PA)_&_not_a_._x_=_TRUE_)_&_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(y,PA)_&_('not'_a)_._x_=_TRUE_)_implies_('not'_(B_INF_(a,PA)))_._y_=_(B_SUP_(('not'_a),PA))_._y_)
assume that
A16: ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) and
A17: ex x being Element of Y st
( x in EqClass (y,PA) & ('not' a) . x = TRUE ) ; ::_thesis: ('not' (B_INF (a,PA))) . y = (B_SUP (('not' a),PA)) . y
(B_INF (a,PA)) . y = FALSE by A16, Def16;
then ('not' (B_INF (a,PA))) . y = 'not' FALSE by MARGREL1:def_19;
hence ('not' (B_INF (a,PA))) . y = (B_SUP (('not' a),PA)) . y by A17, Def17; ::_thesis: verum
end;
now__::_thesis:_(_(_for_x_being_Element_of_Y_st_x_in_EqClass_(y,PA)_holds_
a_._x_=_TRUE_)_&_(_for_x_being_Element_of_Y_holds_
(_not_x_in_EqClass_(y,PA)_or_not_('not'_a)_._x_=_TRUE_)_)_implies_('not'_(B_INF_(a,PA)))_._y_=_(B_SUP_(('not'_a),PA))_._y_)
assume that
A18: for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE and
A19: for x being Element of Y holds
( not x in EqClass (y,PA) or not ('not' a) . x = TRUE ) ; ::_thesis: ('not' (B_INF (a,PA))) . y = (B_SUP (('not' a),PA)) . y
(B_INF (a,PA)) . y = TRUE by A18, Def16;
then ('not' (B_INF (a,PA))) . y = 'not' TRUE by MARGREL1:def_19;
hence ('not' (B_INF (a,PA))) . y = (B_SUP (('not' a),PA)) . y by A19, Def17; ::_thesis: verum
end;
hence ('not' (B_INF (a,PA))) . y = (B_SUP (('not' a),PA)) . y by A5, A15, A10; ::_thesis: verum
end;
theorem :: BVFUNC_1:35
for Y being non empty set
for a being Function of Y,BOOLEAN holds B_INF (a,(%O Y)) = B_INF a
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds B_INF (a,(%O Y)) = B_INF a
let a be Function of Y,BOOLEAN; ::_thesis: B_INF (a,(%O Y)) = B_INF a
let y be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (B_INF (a,(%O Y))) . y = (B_INF a) . y
A5: now__::_thesis:_(_not_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_implies_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(y,(%O_Y))_&_not_a_._x_=_TRUE_)_)
EqClass (y,(%O Y)) in %O Y ;
then EqClass (y,(%O Y)) in {Y} by PARTIT1:def_8;
then A6: EqClass (y,(%O Y)) = Y by TARSKI:def_1;
assume ( not for x being Element of Y holds a . x = TRUE & ( for x being Element of Y st x in EqClass (y,(%O Y)) holds
a . x = TRUE ) ) ; ::_thesis: contradiction
hence contradiction by A6; ::_thesis: verum
end;
A7: now__::_thesis:_(_not_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_&_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(y,(%O_Y))_&_not_a_._x_=_TRUE_)_implies_(B_INF_(a,(%O_Y)))_._y_=_(B_INF_a)_._y_)
assume that
A8: not for x being Element of Y holds a . x = TRUE and
A9: ex x being Element of Y st
( x in EqClass (y,(%O Y)) & not a . x = TRUE ) ; ::_thesis: (B_INF (a,(%O Y))) . y = (B_INF a) . y
B_INF a = O_el Y by A8, Def13;
then (B_INF a) . y = FALSE by Def10;
hence (B_INF (a,(%O Y))) . y = (B_INF a) . y by A9, Def16; ::_thesis: verum
end;
now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_a_._x_=_TRUE_)_&_(_for_x_being_Element_of_Y_st_x_in_EqClass_(y,(%O_Y))_holds_
a_._x_=_TRUE_)_implies_(B_INF_(a,(%O_Y)))_._y_=_(B_INF_a)_._y_)
assume that
A10: for x being Element of Y holds a . x = TRUE and
A11: for x being Element of Y st x in EqClass (y,(%O Y)) holds
a . x = TRUE ; ::_thesis: (B_INF (a,(%O Y))) . y = (B_INF a) . y
B_INF a = I_el Y by A10, Def13;
then (B_INF a) . y = TRUE by Def11;
hence (B_INF (a,(%O Y))) . y = (B_INF a) . y by A11, Def16; ::_thesis: verum
end;
hence (B_INF (a,(%O Y))) . y = (B_INF a) . y by A5, A7; ::_thesis: verum
end;
theorem :: BVFUNC_1:36
for Y being non empty set
for a being Function of Y,BOOLEAN holds B_SUP (a,(%O Y)) = B_SUP a
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds B_SUP (a,(%O Y)) = B_SUP a
let a be Function of Y,BOOLEAN; ::_thesis: B_SUP (a,(%O Y)) = B_SUP a
let y be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (B_SUP (a,(%O Y))) . y = (B_SUP a) . y
EqClass (y,(%O Y)) in %O Y ;
then EqClass (y,(%O Y)) in {Y} by PARTIT1:def_8;
then A5: EqClass (y,(%O Y)) = Y by TARSKI:def_1;
A10: now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_
(_not_x_in_EqClass_(y,(%O_Y))_or_not_a_._x_=_TRUE_)_)_&_(_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_)_implies_(B_SUP_(a,(%O_Y)))_._y_=_(B_SUP_a)_._y_)
assume that
A11: for x being Element of Y holds
( not x in EqClass (y,(%O Y)) or not a . x = TRUE ) and
A12: for x being Element of Y holds a . x = FALSE ; ::_thesis: (B_SUP (a,(%O Y))) . y = (B_SUP a) . y
B_SUP a = O_el Y by A12, Def14;
then (B_SUP a) . y = FALSE by Def10;
hence (B_SUP (a,(%O Y))) . y = (B_SUP a) . y by A11, Def17; ::_thesis: verum
end;
now__::_thesis:_(_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(y,(%O_Y))_&_a_._x_=_TRUE_)_&_not_for_x_being_Element_of_Y_holds_a_._x_=_FALSE_implies_(B_SUP_(a,(%O_Y)))_._y_=_(B_SUP_a)_._y_)
assume that
A13: ex x being Element of Y st
( x in EqClass (y,(%O Y)) & a . x = TRUE ) and
not for x being Element of Y holds a . x = FALSE ; ::_thesis: (B_SUP (a,(%O Y))) . y = (B_SUP a) . y
B_SUP a = I_el Y by A13, Def14;
then (B_SUP a) . y = TRUE by Def11;
hence (B_SUP (a,(%O Y))) . y = (B_SUP a) . y by A13, Def17; ::_thesis: verum
end;
hence (B_SUP (a,(%O Y))) . y = (B_SUP a) . y by A10, A5, XBOOLEAN:def_3; ::_thesis: verum
end;
theorem :: BVFUNC_1:37
for Y being non empty set
for a being Function of Y,BOOLEAN holds B_INF (a,(%I Y)) = a
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds B_INF (a,(%I Y)) = a
let a be Function of Y,BOOLEAN; ::_thesis: B_INF (a,(%I Y)) = a
let y be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (B_INF (a,(%I Y))) . y = a . y
A5: now__::_thesis:_(_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(y,(%I_Y))_&_not_a_._x_=_TRUE_)_implies_not_a_._y_=_TRUE_)
EqClass (y,(%I Y)) in %I Y ;
then EqClass (y,(%I Y)) in { B where B is Subset of Y : ex z being set st
( B = {z} & z in Y ) } by PARTIT1:31;
then ex B being Subset of Y st
( EqClass (y,(%I Y)) = B & ex z being set st
( B = {z} & z in Y ) ) ;
then consider z being set such that
A6: EqClass (y,(%I Y)) = {z} and
z in Y ;
A7: y in {z} by A6, EQREL_1:def_6;
assume that
A8: ex x being Element of Y st
( x in EqClass (y,(%I Y)) & not a . x = TRUE ) and
A9: a . y = TRUE ; ::_thesis: contradiction
consider x1 being Element of Y such that
A10: x1 in EqClass (y,(%I Y)) and
A11: a . x1 <> TRUE by A8;
x1 = z by A10, A6, TARSKI:def_1;
hence contradiction by A9, A11, A7, TARSKI:def_1; ::_thesis: verum
end;
A13: now__::_thesis:_(_(_for_x_being_Element_of_Y_st_x_in_EqClass_(y,(%I_Y))_holds_
a_._x_=_TRUE_)_implies_(B_INF_(a,(%I_Y)))_._y_=_a_._y_)
assume A14: for x being Element of Y st x in EqClass (y,(%I Y)) holds
a . x = TRUE ; ::_thesis: (B_INF (a,(%I Y))) . y = a . y
then a . y = TRUE by EQREL_1:def_6;
hence (B_INF (a,(%I Y))) . y = a . y by A14, Def16; ::_thesis: verum
end;
now__::_thesis:_(_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(y,(%I_Y))_&_not_a_._x_=_TRUE_)_&_a_._y_<>_TRUE_implies_(B_INF_(a,(%I_Y)))_._y_=_a_._y_)
assume that
A15: ex x being Element of Y st
( x in EqClass (y,(%I Y)) & not a . x = TRUE ) and
A16: a . y <> TRUE ; ::_thesis: (B_INF (a,(%I Y))) . y = a . y
a . y = FALSE by A16, XBOOLEAN:def_3;
hence (B_INF (a,(%I Y))) . y = a . y by A15, Def16; ::_thesis: verum
end;
hence (B_INF (a,(%I Y))) . y = a . y by A13, A5; ::_thesis: verum
end;
theorem :: BVFUNC_1:38
for Y being non empty set
for a being Function of Y,BOOLEAN holds B_SUP (a,(%I Y)) = a
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds B_SUP (a,(%I Y)) = a
let a be Function of Y,BOOLEAN; ::_thesis: B_SUP (a,(%I Y)) = a
let y be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (B_SUP (a,(%I Y))) . y = a . y
A5: now__::_thesis:_(_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(y,(%I_Y))_&_a_._x_=_TRUE_)_implies_not_a_._y_<>_TRUE_)
EqClass (y,(%I Y)) in %I Y ;
then EqClass (y,(%I Y)) in { B where B is Subset of Y : ex z being set st
( B = {z} & z in Y ) } by PARTIT1:31;
then ex B being Subset of Y st
( EqClass (y,(%I Y)) = B & ex z being set st
( B = {z} & z in Y ) ) ;
then consider z being set such that
A6: EqClass (y,(%I Y)) = {z} and
z in Y ;
A7: y in {z} by A6, EQREL_1:def_6;
assume that
A8: ex x being Element of Y st
( x in EqClass (y,(%I Y)) & a . x = TRUE ) and
A9: a . y <> TRUE ; ::_thesis: contradiction
consider x1 being Element of Y such that
A10: x1 in EqClass (y,(%I Y)) and
A11: a . x1 = TRUE by A8;
x1 = z by A10, A6, TARSKI:def_1;
hence contradiction by A9, A11, A7, TARSKI:def_1; ::_thesis: verum
end;
A12: now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_
(_not_x_in_EqClass_(y,(%I_Y))_or_not_a_._x_=_TRUE_)_)_&_a_._y_<>_TRUE_implies_(B_SUP_(a,(%I_Y)))_._y_=_a_._y_)
assume that
A13: for x being Element of Y holds
( not x in EqClass (y,(%I Y)) or not a . x = TRUE ) and
A14: a . y <> TRUE ; ::_thesis: (B_SUP (a,(%I Y))) . y = a . y
a . y = FALSE by A14, XBOOLEAN:def_3;
hence (B_SUP (a,(%I Y))) . y = a . y by A13, Def17; ::_thesis: verum
end;
y in EqClass (y,(%I Y)) by EQREL_1:def_6;
hence (B_SUP (a,(%I Y))) . y = a . y by A5, A12, Def17; ::_thesis: verum
end;
theorem :: BVFUNC_1:39
for Y being non empty set
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds B_INF ((a '&' b),PA) = (B_INF (a,PA)) '&' (B_INF (b,PA))
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds B_INF ((a '&' b),PA) = (B_INF (a,PA)) '&' (B_INF (b,PA))
let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds B_INF ((a '&' b),PA) = (B_INF (a,PA)) '&' (B_INF (b,PA))
let PA be a_partition of Y; ::_thesis: B_INF ((a '&' b),PA) = (B_INF (a,PA)) '&' (B_INF (b,PA))
let y be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (B_INF ((a '&' b),PA)) . y = ((B_INF (a,PA)) '&' (B_INF (b,PA))) . y
A5: now__::_thesis:_(_(_for_x_being_Element_of_Y_st_x_in_EqClass_(y,PA)_holds_
a_._x_=_TRUE_)_&_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(y,PA)_&_not_b_._x_=_TRUE_)_implies_(B_INF_((a_'&'_b),PA))_._y_=_((B_INF_(a,PA))_'&'_(B_INF_(b,PA)))_._y_)
assume that
for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE and
A6: ex x being Element of Y st
( x in EqClass (y,PA) & not b . x = TRUE ) ; ::_thesis: (B_INF ((a '&' b),PA)) . y = ((B_INF (a,PA)) '&' (B_INF (b,PA))) . y
(B_INF (b,PA)) . y = FALSE by A6, Def16;
then ((B_INF (a,PA)) . y) '&' ((B_INF (b,PA)) . y) = FALSE ;
then A7: ((B_INF (a,PA)) '&' (B_INF (b,PA))) . y = FALSE by MARGREL1:def_20;
consider x1 being Element of Y such that
A8: x1 in EqClass (y,PA) and
A9: b . x1 <> TRUE by A6;
b . x1 = FALSE by A9, XBOOLEAN:def_3;
then (a . x1) '&' (b . x1) = FALSE ;
then (a '&' b) . x1 <> TRUE by MARGREL1:def_20;
hence (B_INF ((a '&' b),PA)) . y = ((B_INF (a,PA)) '&' (B_INF (b,PA))) . y by A8, A7, Def16; ::_thesis: verum
end;
A10: now__::_thesis:_(_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(y,PA)_&_not_a_._x_=_TRUE_)_&_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(y,PA)_&_not_b_._x_=_TRUE_)_implies_(B_INF_((a_'&'_b),PA))_._y_=_((B_INF_(a,PA))_'&'_(B_INF_(b,PA)))_._y_)
assume that
A11: ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) and
A12: ex x being Element of Y st
( x in EqClass (y,PA) & not b . x = TRUE ) ; ::_thesis: (B_INF ((a '&' b),PA)) . y = ((B_INF (a,PA)) '&' (B_INF (b,PA))) . y
(B_INF (b,PA)) . y = FALSE by A12, Def16;
then ((B_INF (a,PA)) . y) '&' ((B_INF (b,PA)) . y) = FALSE ;
then A13: ((B_INF (a,PA)) '&' (B_INF (b,PA))) . y = FALSE by MARGREL1:def_20;
consider xa being Element of Y such that
A14: xa in EqClass (y,PA) and
A15: a . xa <> TRUE by A11;
a . xa = FALSE by A15, XBOOLEAN:def_3;
then (a . xa) '&' (b . xa) = FALSE ;
then (a '&' b) . xa <> TRUE by MARGREL1:def_20;
hence (B_INF ((a '&' b),PA)) . y = ((B_INF (a,PA)) '&' (B_INF (b,PA))) . y by A14, A13, Def16; ::_thesis: verum
end;
A16: now__::_thesis:_(_(_for_x_being_Element_of_Y_st_x_in_EqClass_(y,PA)_holds_
a_._x_=_TRUE_)_&_(_for_x_being_Element_of_Y_st_x_in_EqClass_(y,PA)_holds_
b_._x_=_TRUE_)_implies_(B_INF_((a_'&'_b),PA))_._y_=_((B_INF_(a,PA))_'&'_(B_INF_(b,PA)))_._y_)
assume that
A17: for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE and
A18: for x being Element of Y st x in EqClass (y,PA) holds
b . x = TRUE ; ::_thesis: (B_INF ((a '&' b),PA)) . y = ((B_INF (a,PA)) '&' (B_INF (b,PA))) . y
A19: for x being Element of Y st x in EqClass (y,PA) holds
(a '&' b) . x = TRUE
proof
let x be Element of Y; ::_thesis: ( x in EqClass (y,PA) implies (a '&' b) . x = TRUE )
assume A20: x in EqClass (y,PA) ; ::_thesis: (a '&' b) . x = TRUE
then b . x = TRUE by A18;
then (a . x) '&' (b . x) = TRUE '&' TRUE by A17, A20;
hence (a '&' b) . x = TRUE by MARGREL1:def_20; ::_thesis: verum
end;
(B_INF (b,PA)) . y = TRUE by A18, Def16;
then ((B_INF (a,PA)) . y) '&' ((B_INF (b,PA)) . y) = TRUE '&' TRUE by A17, Def16;
then ((B_INF (a,PA)) '&' (B_INF (b,PA))) . y = TRUE by MARGREL1:def_20;
hence (B_INF ((a '&' b),PA)) . y = ((B_INF (a,PA)) '&' (B_INF (b,PA))) . y by A19, Def16; ::_thesis: verum
end;
now__::_thesis:_(_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(y,PA)_&_not_a_._x_=_TRUE_)_&_(_for_x_being_Element_of_Y_st_x_in_EqClass_(y,PA)_holds_
b_._x_=_TRUE_)_implies_(B_INF_((a_'&'_b),PA))_._y_=_((B_INF_(a,PA))_'&'_(B_INF_(b,PA)))_._y_)
assume that
A21: ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) and
A22: for x being Element of Y st x in EqClass (y,PA) holds
b . x = TRUE ; ::_thesis: (B_INF ((a '&' b),PA)) . y = ((B_INF (a,PA)) '&' (B_INF (b,PA))) . y
(B_INF (b,PA)) . y = TRUE by A22, Def16;
then ((B_INF (a,PA)) . y) '&' ((B_INF (b,PA)) . y) = FALSE '&' TRUE by A21, Def16;
then A23: ((B_INF (a,PA)) '&' (B_INF (b,PA))) . y = FALSE by MARGREL1:def_20;
consider x1 being Element of Y such that
A24: x1 in EqClass (y,PA) and
A25: a . x1 <> TRUE by A21;
a . x1 = FALSE by A25, XBOOLEAN:def_3;
then (a . x1) '&' (b . x1) = FALSE ;
then (a '&' b) . x1 <> TRUE by MARGREL1:def_20;
hence (B_INF ((a '&' b),PA)) . y = ((B_INF (a,PA)) '&' (B_INF (b,PA))) . y by A24, A23, Def16; ::_thesis: verum
end;
hence (B_INF ((a '&' b),PA)) . y = ((B_INF (a,PA)) '&' (B_INF (b,PA))) . y by A16, A5, A10; ::_thesis: verum
end;
theorem :: BVFUNC_1:40
for Y being non empty set
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds B_SUP ((a 'or' b),PA) = (B_SUP (a,PA)) 'or' (B_SUP (b,PA))
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds B_SUP ((a 'or' b),PA) = (B_SUP (a,PA)) 'or' (B_SUP (b,PA))
let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds B_SUP ((a 'or' b),PA) = (B_SUP (a,PA)) 'or' (B_SUP (b,PA))
let PA be a_partition of Y; ::_thesis: B_SUP ((a 'or' b),PA) = (B_SUP (a,PA)) 'or' (B_SUP (b,PA))
let y be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y
A5: now__::_thesis:_(_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(y,PA)_&_(a_'or'_b)_._x_=_TRUE_)_implies_(B_SUP_((a_'or'_b),PA))_._y_=_((B_SUP_(a,PA))_'or'_(B_SUP_(b,PA)))_._y_)
assume A6: ex x being Element of Y st
( x in EqClass (y,PA) & (a 'or' b) . x = TRUE ) ; ::_thesis: (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y
then consider x1 being Element of Y such that
A7: x1 in EqClass (y,PA) and
A8: (a 'or' b) . x1 = TRUE ;
A9: ( ( a . x1 = FALSE & b . x1 = FALSE ) or ( a . x1 = FALSE & b . x1 = TRUE ) or ( a . x1 = TRUE & b . x1 = FALSE ) or ( a . x1 = TRUE & b . x1 = TRUE ) ) by XBOOLEAN:def_3;
A10: (a . x1) 'or' (b . x1) = TRUE by A8, Def4;
now__::_thesis:_(_(_a_._x1_=_FALSE_&_b_._x1_=_TRUE_&_(B_SUP_((a_'or'_b),PA))_._y_=_((B_SUP_(a,PA))_'or'_(B_SUP_(b,PA)))_._y_)_or_(_a_._x1_=_TRUE_&_b_._x1_=_FALSE_&_(B_SUP_((a_'or'_b),PA))_._y_=_((B_SUP_(a,PA))_'or'_(B_SUP_(b,PA)))_._y_)_or_(_a_._x1_=_TRUE_&_b_._x1_=_TRUE_&_(B_SUP_((a_'or'_b),PA))_._y_=_((B_SUP_(a,PA))_'or'_(B_SUP_(b,PA)))_._y_)_)
percases ( ( a . x1 = FALSE & b . x1 = TRUE ) or ( a . x1 = TRUE & b . x1 = FALSE ) or ( a . x1 = TRUE & b . x1 = TRUE ) ) by A10, A9;
case ( a . x1 = FALSE & b . x1 = TRUE ) ; ::_thesis: (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y
then (B_SUP (b,PA)) . y = TRUE by A7, Def17;
then ((B_SUP (a,PA)) . y) 'or' ((B_SUP (b,PA)) . y) = TRUE ;
then ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y = TRUE by Def4;
hence (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y by A6, Def17; ::_thesis: verum
end;
case ( a . x1 = TRUE & b . x1 = FALSE ) ; ::_thesis: (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y
then (B_SUP (a,PA)) . y = TRUE by A7, Def17;
then ((B_SUP (a,PA)) . y) 'or' ((B_SUP (b,PA)) . y) = TRUE ;
then ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y = TRUE by Def4;
hence (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y by A6, Def17; ::_thesis: verum
end;
case ( a . x1 = TRUE & b . x1 = TRUE ) ; ::_thesis: (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y
then (B_SUP (b,PA)) . y = TRUE by A7, Def17;
then ((B_SUP (a,PA)) . y) 'or' ((B_SUP (b,PA)) . y) = TRUE ;
then ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y = TRUE by Def4;
hence (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y by A6, Def17; ::_thesis: verum
end;
end;
end;
hence (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y ; ::_thesis: verum
end;
now__::_thesis:_(_(_for_x_being_Element_of_Y_holds_
(_not_x_in_EqClass_(y,PA)_or_not_(a_'or'_b)_._x_=_TRUE_)_)_implies_(B_SUP_((a_'or'_b),PA))_._y_=_((B_SUP_(a,PA))_'or'_(B_SUP_(b,PA)))_._y_)
assume A11: for x being Element of Y holds
( not x in EqClass (y,PA) or not (a 'or' b) . x = TRUE ) ; ::_thesis: (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y
now__::_thesis:_for_x_being_Element_of_Y_holds_
(_not_x_in_EqClass_(y,PA)_or_not_b_._x_=_TRUE_)
assume ex x being Element of Y st
( x in EqClass (y,PA) & b . x = TRUE ) ; ::_thesis: contradiction
then consider x1 being Element of Y such that
A12: x1 in EqClass (y,PA) and
A13: b . x1 = TRUE ;
(a . x1) 'or' (b . x1) = TRUE by A13;
then (a 'or' b) . x1 = TRUE by Def4;
hence contradiction by A11, A12; ::_thesis: verum
end;
then A14: (B_SUP (b,PA)) . y = FALSE by Def17;
now__::_thesis:_for_x_being_Element_of_Y_holds_
(_not_x_in_EqClass_(y,PA)_or_not_a_._x_=_TRUE_)
assume ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) ; ::_thesis: contradiction
then consider x1 being Element of Y such that
A15: x1 in EqClass (y,PA) and
A16: a . x1 = TRUE ;
(a . x1) 'or' (b . x1) = TRUE by A16;
then (a 'or' b) . x1 = TRUE by Def4;
hence contradiction by A11, A15; ::_thesis: verum
end;
then ((B_SUP (a,PA)) . y) 'or' ((B_SUP (b,PA)) . y) = FALSE 'or' FALSE by A14, Def17;
then ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y = FALSE by Def4;
hence (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y by A11, Def17; ::_thesis: verum
end;
hence (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y by A5; ::_thesis: verum
end;
definition
let Y be non empty set ;
let f be Function of Y,BOOLEAN;
func GPart f -> a_partition of Y equals :: BVFUNC_1:def 18
{ { x where x is Element of Y : f . x = TRUE } , { x9 where x9 is Element of Y : f . x9 = FALSE } } \ {{}};
correctness
coherence
{ { x where x is Element of Y : f . x = TRUE } , { x9 where x9 is Element of Y : f . x9 = FALSE } } \ {{}} is a_partition of Y;
proof
defpred S1[ set ] means f . $1 = TRUE ;
reconsider C = { x where x is Element of Y : S1[x] } as Subset of Y from DOMAIN_1:sch_7();
defpred S2[ set ] means f . $1 = FALSE ;
reconsider D = { x9 where x9 is Element of Y : S2[x9] } as Subset of Y from DOMAIN_1:sch_7();
A1: union ({C,D} \ {{}}) = Y
proof
thus union ({C,D} \ {{}}) c= Y :: according to XBOOLE_0:def_10 ::_thesis: Y c= union ({C,D} \ {{}})
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union ({C,D} \ {{}}) or a in Y )
assume a in union ({C,D} \ {{}}) ; ::_thesis: a in Y
then ex b being set st
( a in b & b in {C,D} \ {{}} ) by TARSKI:def_4;
then ( a in C or a in D ) by TARSKI:def_2;
hence a in Y ; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Y or a in union ({C,D} \ {{}}) )
A2: C in {C,D} by TARSKI:def_2;
assume a in Y ; ::_thesis: a in union ({C,D} \ {{}})
then reconsider a = a as Element of Y ;
A3: ( f . a = TRUE or f . a = FALSE ) by TARSKI:def_2;
A4: D in {C,D} by TARSKI:def_2;
percases ( a in C or a in D ) by A3;
supposeA5: a in C ; ::_thesis: a in union ({C,D} \ {{}})
then not C in {{}} by TARSKI:def_1;
then C in {C,D} \ {{}} by A2, XBOOLE_0:def_5;
hence a in union ({C,D} \ {{}}) by A5, TARSKI:def_4; ::_thesis: verum
end;
supposeA6: a in D ; ::_thesis: a in union ({C,D} \ {{}})
then not D in {{}} by TARSKI:def_1;
then D in {C,D} \ {{}} by A4, XBOOLE_0:def_5;
hence a in union ({C,D} \ {{}}) by A6, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
A7: for A being Subset of Y st A in {C,D} \ {{}} holds
( A <> {} & ( for B being Subset of Y holds
( not B in {C,D} \ {{}} or A = B or A misses B ) ) )
proof
let A be Subset of Y; ::_thesis: ( A in {C,D} \ {{}} implies ( A <> {} & ( for B being Subset of Y holds
( not B in {C,D} \ {{}} or A = B or A misses B ) ) ) )
A8: now__::_thesis:_for_b_being_set_holds_
(_not_b_in_C_or_not_b_in_D_)
given b being set such that A9: ( b in C & b in D ) ; ::_thesis: contradiction
now__::_thesis:_(_b_in_C_implies_not_b_in_D_)
assume b in C ; ::_thesis: not b in D
then A10: ex x being Element of Y st
( b = x & f . x = TRUE ) ;
now__::_thesis:_not_b_in_D
assume b in D ; ::_thesis: contradiction
then ex x9 being Element of Y st
( b = x9 & f . x9 = FALSE ) ;
hence contradiction by A10; ::_thesis: verum
end;
hence not b in D ; ::_thesis: verum
end;
hence contradiction by A9; ::_thesis: verum
end;
assume A11: A in {C,D} \ {{}} ; ::_thesis: ( A <> {} & ( for B being Subset of Y holds
( not B in {C,D} \ {{}} or A = B or A misses B ) ) )
then not A in {{}} by XBOOLE_0:def_5;
hence A <> {} by TARSKI:def_1; ::_thesis: for B being Subset of Y holds
( not B in {C,D} \ {{}} or A = B or A misses B )
let B be Subset of Y; ::_thesis: ( not B in {C,D} \ {{}} or A = B or A misses B )
assume A12: B in {C,D} \ {{}} ; ::_thesis: ( A = B or A misses B )
percases ( ( A = C & B = C ) or ( A = D & B = D ) or ( A = C & B = D ) or ( A = D & B = C ) ) by A11, A12, TARSKI:def_2;
suppose ( A = C & B = C ) ; ::_thesis: ( A = B or A misses B )
hence ( A = B or A misses B ) ; ::_thesis: verum
end;
suppose ( A = D & B = D ) ; ::_thesis: ( A = B or A misses B )
hence ( A = B or A misses B ) ; ::_thesis: verum
end;
suppose ( A = C & B = D ) ; ::_thesis: ( A = B or A misses B )
hence ( A = B or A misses B ) by A8, XBOOLE_0:3; ::_thesis: verum
end;
suppose ( A = D & B = C ) ; ::_thesis: ( A = B or A misses B )
hence ( A = B or A misses B ) by A8, XBOOLE_0:3; ::_thesis: verum
end;
end;
end;
{C,D} \ {{}} c= bool Y
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {C,D} \ {{}} or a in bool Y )
assume a in {C,D} \ {{}} ; ::_thesis: a in bool Y
then ( a = C or a = D ) by TARSKI:def_2;
hence a in bool Y ; ::_thesis: verum
end;
hence { { x where x is Element of Y : f . x = TRUE } , { x9 where x9 is Element of Y : f . x9 = FALSE } } \ {{}} is a_partition of Y by A1, A7, EQREL_1:def_4; ::_thesis: verum
end;
end;
:: deftheorem defines GPart BVFUNC_1:def_18_:_
for Y being non empty set
for f being Function of Y,BOOLEAN holds GPart f = { { x where x is Element of Y : f . x = TRUE } , { x9 where x9 is Element of Y : f . x9 = FALSE } } \ {{}};
theorem :: BVFUNC_1:41
for Y being non empty set
for a being Function of Y,BOOLEAN holds a is_dependent_of GPart a
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a is_dependent_of GPart a
let a be Function of Y,BOOLEAN; ::_thesis: a is_dependent_of GPart a
defpred S1[ set ] means a . $1 = TRUE ;
reconsider C = { x where x is Element of Y : S1[x] } as Subset of Y from DOMAIN_1:sch_7();
defpred S2[ set ] means a . $1 = FALSE ;
reconsider D = { x9 where x9 is Element of Y : S2[x9] } as Subset of Y from DOMAIN_1:sch_7();
for F being set st F in GPart a holds
for x1, x2 being set st x1 in F & x2 in F holds
a . x1 = a . x2
proof
let F be set ; ::_thesis: ( F in GPart a implies for x1, x2 being set st x1 in F & x2 in F holds
a . x1 = a . x2 )
assume A1: F in GPart a ; ::_thesis: for x1, x2 being set st x1 in F & x2 in F holds
a . x1 = a . x2
thus for x1, x2 being set st x1 in F & x2 in F holds
a . x1 = a . x2 ::_thesis: verum
proof
let x1, x2 be set ; ::_thesis: ( x1 in F & x2 in F implies a . x1 = a . x2 )
assume A2: ( x1 in F & x2 in F ) ; ::_thesis: a . x1 = a . x2
then reconsider x1 = x1, x2 = x2 as Element of Y by A1;
now__::_thesis:_(_(_F_=_C_&_a_._x1_=_a_._x2_)_or_(_F_=_D_&_a_._x1_=_a_._x2_)_)
percases ( F = C or F = D ) by A1, TARSKI:def_2;
case F = C ; ::_thesis: a . x1 = a . x2
then ( ex x being Element of Y st
( x = x1 & a . x = TRUE ) & ex x5 being Element of Y st
( x5 = x2 & a . x5 = TRUE ) ) by A2;
hence a . x1 = a . x2 ; ::_thesis: verum
end;
case F = D ; ::_thesis: a . x1 = a . x2
then ( ex x being Element of Y st
( x = x1 & a . x = FALSE ) & ex x5 being Element of Y st
( x5 = x2 & a . x5 = FALSE ) ) by A2;
hence a . x1 = a . x2 ; ::_thesis: verum
end;
end;
end;
hence a . x1 = a . x2 ; ::_thesis: verum
end;
end;
hence a is_dependent_of GPart a by Def15; ::_thesis: verum
end;
theorem :: BVFUNC_1:42
for Y being non empty set
for a being Function of Y,BOOLEAN
for PA being a_partition of Y st a is_dependent_of PA holds
PA is_finer_than GPart a
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN
for PA being a_partition of Y st a is_dependent_of PA holds
PA is_finer_than GPart a
let a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y st a is_dependent_of PA holds
PA is_finer_than GPart a
let PA be a_partition of Y; ::_thesis: ( a is_dependent_of PA implies PA is_finer_than GPart a )
defpred S1[ set ] means a . $1 = TRUE ;
reconsider C = { x where x is Element of Y : S1[x] } as Subset of Y from DOMAIN_1:sch_7();
defpred S2[ set ] means a . $1 = FALSE ;
reconsider D = { x9 where x9 is Element of Y : S2[x9] } as Subset of Y from DOMAIN_1:sch_7();
assume A1: a is_dependent_of PA ; ::_thesis: PA is_finer_than GPart a
for g being set st g in PA holds
ex h being set st
( h in GPart a & g c= h )
proof
let g be set ; ::_thesis: ( g in PA implies ex h being set st
( h in GPart a & g c= h ) )
set u = the Element of g;
assume A2: g in PA ; ::_thesis: ex h being set st
( h in GPart a & g c= h )
then A3: g <> {} by EQREL_1:def_4;
then the Element of g in g ;
then reconsider u = the Element of g as Element of Y by A2;
A4: for x1 being set holds
( not x1 in g or a . x1 = TRUE or a . x1 = FALSE )
proof
let x1 be set ; ::_thesis: ( not x1 in g or a . x1 = TRUE or a . x1 = FALSE )
assume x1 in g ; ::_thesis: ( a . x1 = TRUE or a . x1 = FALSE )
then reconsider x1 = x1 as Element of Y by A2;
a . x1 in BOOLEAN ;
hence ( a . x1 = TRUE or a . x1 = FALSE ) by TARSKI:def_2; ::_thesis: verum
end;
now__::_thesis:_(_(_a_._u_=_TRUE_&_ex_h_being_set_st_
(_h_in_GPart_a_&_g_c=_h_)_)_or_(_a_._u_=_FALSE_&_ex_h_being_set_st_
(_h_in_GPart_a_&_g_c=_h_)_)_)
percases ( a . u = TRUE or a . u = FALSE ) by A3, A4;
caseA5: a . u = TRUE ; ::_thesis: ex h being set st
( h in GPart a & g c= h )
A6: g c= C
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in g or t in C )
assume A7: t in g ; ::_thesis: t in C
then reconsider t = t as Element of Y by A2;
now__::_thesis:_(_(_a_._t_=_TRUE_&_t_in_C_)_or_(_a_._t_=_FALSE_&_contradiction_)_)
percases ( a . t = TRUE or a . t = FALSE ) by A4, A7;
case a . t = TRUE ; ::_thesis: t in C
hence t in C ; ::_thesis: verum
end;
case a . t = FALSE ; ::_thesis: contradiction
hence contradiction by A1, A2, A5, A7, Def15; ::_thesis: verum
end;
end;
end;
hence t in C ; ::_thesis: verum
end;
u in C by A5;
then A8: not C in {{}} by TARSKI:def_1;
C in {C,D} by TARSKI:def_2;
then C in {C,D} \ {{}} by A8, XBOOLE_0:def_5;
hence ex h being set st
( h in GPart a & g c= h ) by A6; ::_thesis: verum
end;
caseA9: a . u = FALSE ; ::_thesis: ex h being set st
( h in GPart a & g c= h )
A10: g c= D
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in g or t in D )
assume A11: t in g ; ::_thesis: t in D
then reconsider t = t as Element of Y by A2;
now__::_thesis:_(_(_a_._t_=_TRUE_&_contradiction_)_or_(_a_._t_=_FALSE_&_t_in_D_)_)
percases ( a . t = TRUE or a . t = FALSE ) by A4, A11;
case a . t = TRUE ; ::_thesis: contradiction
hence contradiction by A1, A2, A9, A11, Def15; ::_thesis: verum
end;
case a . t = FALSE ; ::_thesis: t in D
hence t in D ; ::_thesis: verum
end;
end;
end;
hence t in D ; ::_thesis: verum
end;
u in D by A9;
then A12: not D in {{}} by TARSKI:def_1;
D in {C,D} by TARSKI:def_2;
then D in {C,D} \ {{}} by A12, XBOOLE_0:def_5;
hence ex h being set st
( h in GPart a & g c= h ) by A10; ::_thesis: verum
end;
end;
end;
hence ex h being set st
( h in GPart a & g c= h ) ; ::_thesis: verum
end;
hence PA is_finer_than GPart a by SETFAM_1:def_2; ::_thesis: verum
end;
begin
definition
let x, y be Element of BOOLEAN ;
:: original: 'nand'
redefine funcx 'nand' y -> Element of BOOLEAN ;
correctness
coherence
x 'nand' y is Element of BOOLEAN ;
proof
( x 'nand' y = FALSE or x 'nand' y = TRUE ) by XBOOLEAN:def_3;
hence x 'nand' y is Element of BOOLEAN ; ::_thesis: verum
end;
end;
definition
let x, y be Element of BOOLEAN ;
:: original: 'nor'
redefine funcx 'nor' y -> Element of BOOLEAN ;
correctness
coherence
x 'nor' y is Element of BOOLEAN ;
proof
( x 'nor' y = FALSE or x 'nor' y = TRUE ) by XBOOLEAN:def_3;
hence x 'nor' y is Element of BOOLEAN ; ::_thesis: verum
end;
end;
definition
let x, y be boolean set ;
redefine func x <=> y equals :: BVFUNC_1:def 19
'not' (x 'xor' y);
correctness
compatibility
for b1 being set holds
( b1 = x <=> y iff b1 = 'not' (x 'xor' y) );
;
end;
:: deftheorem defines <=> BVFUNC_1:def_19_:_
for x, y being boolean set holds x <=> y = 'not' (x 'xor' y);
definition
let x, y be Element of BOOLEAN ;
:: original: <=>
redefine funcx <=> y -> Element of BOOLEAN ;
correctness
coherence
x <=> y is Element of BOOLEAN ;
proof
( x <=> y = FALSE or x <=> y = TRUE ) by XBOOLEAN:def_3;
hence x <=> y is Element of BOOLEAN ; ::_thesis: verum
end;
end;
theorem :: BVFUNC_1:43
for x being boolean set holds TRUE 'nand' x = 'not' x ;
theorem :: BVFUNC_1:44
for x being boolean set holds FALSE 'nand' x = TRUE ;
theorem :: BVFUNC_1:45
for x being boolean set holds
( x 'nand' x = 'not' x & 'not' (x 'nand' x) = x ) ;
theorem :: BVFUNC_1:46
for x, y being boolean set holds 'not' (x 'nand' y) = x '&' y ;
theorem :: BVFUNC_1:47
for x being boolean set holds
( x 'nand' ('not' x) = TRUE & 'not' (x 'nand' ('not' x)) = FALSE ) by XBOOLEAN:135, XBOOLEAN:138;
theorem :: BVFUNC_1:48
for x, y, z being boolean set holds x 'nand' (y '&' z) = 'not' ((x '&' y) '&' z) ;
theorem :: BVFUNC_1:49
for x, y, z being boolean set holds x 'nand' (y '&' z) = (x '&' y) 'nand' z ;
theorem :: BVFUNC_1:50
for x being boolean set holds TRUE 'nor' x = FALSE ;
theorem :: BVFUNC_1:51
for x being boolean set holds FALSE 'nor' x = 'not' x ;
theorem :: BVFUNC_1:52
for x being boolean set holds
( x 'nor' x = 'not' x & 'not' (x 'nor' x) = x ) ;
theorem :: BVFUNC_1:53
for x, y being boolean set holds 'not' (x 'nor' y) = x 'or' y ;
theorem :: BVFUNC_1:54
for x being boolean set holds
( x 'nor' ('not' x) = FALSE & 'not' (x 'nor' ('not' x)) = TRUE ) by XBOOLEAN:134, XBOOLEAN:138;
theorem :: BVFUNC_1:55
for x, y, z being boolean set holds x 'nor' (y 'or' z) = 'not' ((x 'or' y) 'or' z) ;
theorem :: BVFUNC_1:56
for x being boolean set holds TRUE <=> x = x ;
theorem :: BVFUNC_1:57
for x being boolean set holds FALSE <=> x = 'not' x ;
theorem :: BVFUNC_1:58
for x being boolean set holds
( x <=> x = TRUE & 'not' (x <=> x) = FALSE ) by XBOOLEAN:125, XBOOLEAN:143;
theorem :: BVFUNC_1:59
for x, y being boolean set holds 'not' (x <=> y) = x 'xor' y ;
theorem :: BVFUNC_1:60
for x being boolean set holds
( x <=> ('not' x) = FALSE & 'not' (x <=> ('not' x)) = TRUE ) by XBOOLEAN:129, XBOOLEAN:142;
theorem :: BVFUNC_1:61
for x, y, z being boolean set holds
( x <= y => z iff x '&' y <= z )
proof
let x, y, z be boolean set ; ::_thesis: ( x <= y => z iff x '&' y <= z )
thus ( x <= y => z implies x '&' y <= z ) ::_thesis: ( x '&' y <= z implies x <= y => z )
proof
assume x <= y => z ; ::_thesis: x '&' y <= z
then A1: x => (y => z) = TRUE by Def1;
x => (y => z) = (x '&' y) => z ;
hence x '&' y <= z by A1, Def1; ::_thesis: verum
end;
assume x '&' y <= z ; ::_thesis: x <= y => z
then A2: (x '&' y) => z = TRUE by Def1;
(x '&' y) => z = x => (y => z) ;
hence x <= y => z by A2, Def1; ::_thesis: verum
end;
theorem :: BVFUNC_1:62
for x, y being boolean set holds x <=> y = (x => y) '&' (y => x) ;
theorem :: BVFUNC_1:63
for x, y being boolean set holds x => y = ('not' y) => ('not' x) ;
theorem :: BVFUNC_1:64
for x, y being boolean set holds x <=> y = ('not' x) <=> ('not' y) ;
theorem :: BVFUNC_1:65
for x, y being boolean set st x = TRUE & x => y = TRUE holds
y = TRUE ;
theorem :: BVFUNC_1:66
for y, x being boolean set st y = TRUE holds
x => y = TRUE ;
theorem :: BVFUNC_1:67
for x, y being boolean set st 'not' x = TRUE holds
x => y = TRUE ;
theorem :: BVFUNC_1:68
for z, y, x being boolean set st z => (y => x) = TRUE holds
y => (z => x) = TRUE ;
theorem :: BVFUNC_1:69
for z, y, x being boolean set st z => (y => x) = TRUE & y = TRUE holds
z => x = TRUE ;
theorem :: BVFUNC_1:70
for z, y, x being boolean set st z => (y => x) = TRUE & y = TRUE & z = TRUE holds
x = TRUE ;