:: 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 ;