:: HEYTING1 semantic presentation begin theorem Th1: :: HEYTING1:1 for A, B, C being non empty set for f being Function of A,B st ( for x being Element of A holds f . x in C ) holds f is Function of A,C proof let A, B, C be non empty set ; ::_thesis: for f being Function of A,B st ( for x being Element of A holds f . x in C ) holds f is Function of A,C let f be Function of A,B; ::_thesis: ( ( for x being Element of A holds f . x in C ) implies f is Function of A,C ) assume for x being Element of A holds f . x in C ; ::_thesis: f is Function of A,C then ( dom f = A & ( for x being set st x in A holds f . x in C ) ) by FUNCT_2:def_1; hence f is Function of A,C by FUNCT_2:3; ::_thesis: verum end; definition let A be non empty set ; let B, C be Element of Fin A; :: original: c= redefine predB c= C means :: HEYTING1:def 1 for a being Element of A st a in B holds a in C; compatibility ( B c= C iff for a being Element of A st a in B holds a in C ) proof thus ( B c= C implies for a being Element of A st a in B holds a in C ) ; ::_thesis: ( ( for a being Element of A st a in B holds a in C ) implies B c= C ) assume A1: for a being Element of A st a in B holds a in C ; ::_thesis: B c= C let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in C ) assume A2: x in B ; ::_thesis: x in C then x is Element of A by SETWISEO:9; hence x in C by A1, A2; ::_thesis: verum end; end; :: deftheorem defines c= HEYTING1:def_1_:_ for A being non empty set for B, C being Element of Fin A holds ( B c= C iff for a being Element of A st a in B holds a in C ); definition let A be set ; assume A1: not A is empty ; func[A] -> non empty set equals :Def2: :: HEYTING1:def 2 A; correctness coherence A is non empty set ; by A1; end; :: deftheorem Def2 defines [ HEYTING1:def_2_:_ for A being set st not A is empty holds [A] = A; theorem :: HEYTING1:2 for A being set for B being Element of Fin (DISJOINT_PAIRS A) st B = {} holds mi B = {} by NORMFORM:40, XBOOLE_1:3; Lm1: now__::_thesis:_for_A_being_set_ for_a_being_Element_of_DISJOINT_PAIRS_A_holds_{a}_is_Element_of_Normal_forms_on_A let A be set ; ::_thesis: for a being Element of DISJOINT_PAIRS A holds {a} is Element of Normal_forms_on A let a be Element of DISJOINT_PAIRS A; ::_thesis: {a} is Element of Normal_forms_on A reconsider B = {.a.} as Element of Fin (DISJOINT_PAIRS A) ; now__::_thesis:_for_c,_b_being_Element_of_DISJOINT_PAIRS_A_st_c_in_B_&_b_in_B_&_c_c=_b_holds_ c_=_b let c, b be Element of DISJOINT_PAIRS A; ::_thesis: ( c in B & b in B & c c= b implies c = b ) assume that A1: c in B and A2: b in B and c c= b ; ::_thesis: c = b c = a by A1, TARSKI:def_1; hence c = b by A2, TARSKI:def_1; ::_thesis: verum end; hence {a} is Element of Normal_forms_on A by NORMFORM:33; ::_thesis: verum end; registration let A be set ; cluster non empty for Element of Normal_forms_on A; existence not for b1 being Element of Normal_forms_on A holds b1 is empty proof set a = the Element of DISJOINT_PAIRS A; { the Element of DISJOINT_PAIRS A} is Element of Normal_forms_on A by Lm1; hence not for b1 being Element of Normal_forms_on A holds b1 is empty ; ::_thesis: verum end; end; definition let A be set ; let a be Element of DISJOINT_PAIRS A; :: original: { redefine func{a} -> Element of Normal_forms_on A; coherence {a} is Element of Normal_forms_on A by Lm1; end; definition let A be set ; let u be Element of (NormForm A); func @ u -> Element of Normal_forms_on A equals :: HEYTING1:def 3 u; coherence u is Element of Normal_forms_on A by NORMFORM:def_12; end; :: deftheorem defines @ HEYTING1:def_3_:_ for A being set for u being Element of (NormForm A) holds @ u = u; theorem Th3: :: HEYTING1:3 for A being set for K being Element of Normal_forms_on A holds mi (K ^ K) = K proof let A be set ; ::_thesis: for K being Element of Normal_forms_on A holds mi (K ^ K) = K let K be Element of Normal_forms_on A; ::_thesis: mi (K ^ K) = K thus mi (K ^ K) = mi K by NORMFORM:55 .= K by NORMFORM:42 ; ::_thesis: verum end; theorem Th4: :: HEYTING1:4 for A being set for K being Element of Normal_forms_on A for X being set st X c= K holds X in Normal_forms_on A proof let A be set ; ::_thesis: for K being Element of Normal_forms_on A for X being set st X c= K holds X in Normal_forms_on A let K be Element of Normal_forms_on A; ::_thesis: for X being set st X c= K holds X in Normal_forms_on A let X be set ; ::_thesis: ( X c= K implies X in Normal_forms_on A ) assume A1: X c= K ; ::_thesis: X in Normal_forms_on A K c= DISJOINT_PAIRS A by FINSUB_1:def_5; then X c= DISJOINT_PAIRS A by A1, XBOOLE_1:1; then reconsider B = X as Element of Fin (DISJOINT_PAIRS A) by A1, FINSUB_1:def_5; for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds a = b by A1, NORMFORM:32; hence X in Normal_forms_on A ; ::_thesis: verum end; theorem Th5: :: HEYTING1:5 for A being set for u being Element of (NormForm A) for X being set st X c= u holds X is Element of (NormForm A) proof let A be set ; ::_thesis: for u being Element of (NormForm A) for X being set st X c= u holds X is Element of (NormForm A) let u be Element of (NormForm A); ::_thesis: for X being set st X c= u holds X is Element of (NormForm A) let X be set ; ::_thesis: ( X c= u implies X is Element of (NormForm A) ) assume A1: X c= u ; ::_thesis: X is Element of (NormForm A) u = @ u ; then X in Normal_forms_on A by A1, Th4; hence X is Element of (NormForm A) by NORMFORM:def_12; ::_thesis: verum end; definition let A be set ; func Atom A -> Function of (DISJOINT_PAIRS A), the carrier of (NormForm A) means :Def4: :: HEYTING1:def 4 for a being Element of DISJOINT_PAIRS A holds it . a = {a}; existence ex b1 being Function of (DISJOINT_PAIRS A), the carrier of (NormForm A) st for a being Element of DISJOINT_PAIRS A holds b1 . a = {a} proof set f = singleton (DISJOINT_PAIRS A); A1: dom (singleton (DISJOINT_PAIRS A)) = DISJOINT_PAIRS A by FUNCT_2:def_1; A2: the carrier of (NormForm A) = Normal_forms_on A by NORMFORM:def_12; now__::_thesis:_for_x_being_set_st_x_in_DISJOINT_PAIRS_A_holds_ (singleton_(DISJOINT_PAIRS_A))_._x_in_the_carrier_of_(NormForm_A) let x be set ; ::_thesis: ( x in DISJOINT_PAIRS A implies (singleton (DISJOINT_PAIRS A)) . x in the carrier of (NormForm A) ) assume x in DISJOINT_PAIRS A ; ::_thesis: (singleton (DISJOINT_PAIRS A)) . x in the carrier of (NormForm A) then reconsider a = x as Element of DISJOINT_PAIRS A ; (singleton (DISJOINT_PAIRS A)) . a = {a} by SETWISEO:54; hence (singleton (DISJOINT_PAIRS A)) . x in the carrier of (NormForm A) by A2; ::_thesis: verum end; then reconsider f = singleton (DISJOINT_PAIRS A) as Function of (DISJOINT_PAIRS A), the carrier of (NormForm A) by A1, FUNCT_2:3; take f ; ::_thesis: for a being Element of DISJOINT_PAIRS A holds f . a = {a} thus for a being Element of DISJOINT_PAIRS A holds f . a = {a} by SETWISEO:54; ::_thesis: verum end; uniqueness for b1, b2 being Function of (DISJOINT_PAIRS A), the carrier of (NormForm A) st ( for a being Element of DISJOINT_PAIRS A holds b1 . a = {a} ) & ( for a being Element of DISJOINT_PAIRS A holds b2 . a = {a} ) holds b1 = b2 proof let IT1, IT2 be Function of (DISJOINT_PAIRS A), the carrier of (NormForm A); ::_thesis: ( ( for a being Element of DISJOINT_PAIRS A holds IT1 . a = {a} ) & ( for a being Element of DISJOINT_PAIRS A holds IT2 . a = {a} ) implies IT1 = IT2 ) assume that A3: for a being Element of DISJOINT_PAIRS A holds IT1 . a = {a} and A4: for a being Element of DISJOINT_PAIRS A holds IT2 . a = {a} ; ::_thesis: IT1 = IT2 now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_holds_IT1_._a_=_IT2_._a let a be Element of DISJOINT_PAIRS A; ::_thesis: IT1 . a = IT2 . a IT1 . a = {a} by A3; hence IT1 . a = IT2 . a by A4; ::_thesis: verum end; hence IT1 = IT2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def4 defines Atom HEYTING1:def_4_:_ for A being set for b2 being Function of (DISJOINT_PAIRS A), the carrier of (NormForm A) holds ( b2 = Atom A iff for a being Element of DISJOINT_PAIRS A holds b2 . a = {a} ); theorem Th6: :: HEYTING1:6 for A being set for c, a being Element of DISJOINT_PAIRS A st c in (Atom A) . a holds c = a proof let A be set ; ::_thesis: for c, a being Element of DISJOINT_PAIRS A st c in (Atom A) . a holds c = a let c, a be Element of DISJOINT_PAIRS A; ::_thesis: ( c in (Atom A) . a implies c = a ) (Atom A) . a = {a} by Def4; hence ( c in (Atom A) . a implies c = a ) by TARSKI:def_1; ::_thesis: verum end; theorem Th7: :: HEYTING1:7 for A being set for a being Element of DISJOINT_PAIRS A holds a in (Atom A) . a proof let A be set ; ::_thesis: for a being Element of DISJOINT_PAIRS A holds a in (Atom A) . a let a be Element of DISJOINT_PAIRS A; ::_thesis: a in (Atom A) . a (Atom A) . a = {a} by Def4; hence a in (Atom A) . a by TARSKI:def_1; ::_thesis: verum end; theorem :: HEYTING1:8 for A being set for a being Element of DISJOINT_PAIRS A holds (Atom A) . a = (singleton (DISJOINT_PAIRS A)) . a proof let A be set ; ::_thesis: for a being Element of DISJOINT_PAIRS A holds (Atom A) . a = (singleton (DISJOINT_PAIRS A)) . a let a be Element of DISJOINT_PAIRS A; ::_thesis: (Atom A) . a = (singleton (DISJOINT_PAIRS A)) . a thus (singleton (DISJOINT_PAIRS A)) . a = {a} by SETWISEO:54 .= (Atom A) . a by Def4 ; ::_thesis: verum end; theorem Th9: :: HEYTING1:9 for A being set for K being Element of Normal_forms_on A holds FinJoin (K,(Atom A)) = FinUnion (K,(singleton (DISJOINT_PAIRS A))) proof let A be set ; ::_thesis: for K being Element of Normal_forms_on A holds FinJoin (K,(Atom A)) = FinUnion (K,(singleton (DISJOINT_PAIRS A))) let K be Element of Normal_forms_on A; ::_thesis: FinJoin (K,(Atom A)) = FinUnion (K,(singleton (DISJOINT_PAIRS A))) deffunc H1( Element of Fin (DISJOINT_PAIRS A)) -> Element of Normal_forms_on A = mi $1; A1: FinUnion (K,(singleton (DISJOINT_PAIRS A))) c= mi (FinUnion (K,(singleton (DISJOINT_PAIRS A)))) proof let a be Element of DISJOINT_PAIRS A; :: according to HEYTING1:def_1 ::_thesis: ( a in FinUnion (K,(singleton (DISJOINT_PAIRS A))) implies a in mi (FinUnion (K,(singleton (DISJOINT_PAIRS A)))) ) assume A2: a in FinUnion (K,(singleton (DISJOINT_PAIRS A))) ; ::_thesis: a in mi (FinUnion (K,(singleton (DISJOINT_PAIRS A)))) then consider b being Element of DISJOINT_PAIRS A such that A3: b in K and A4: a in (singleton (DISJOINT_PAIRS A)) . b by SETWISEO:57; A5: a = b by A4, SETWISEO:55; now__::_thesis:_for_s_being_Element_of_DISJOINT_PAIRS_A_st_s_in_FinUnion_(K,(singleton_(DISJOINT_PAIRS_A)))_&_s_c=_a_holds_ s_=_a let s be Element of DISJOINT_PAIRS A; ::_thesis: ( s in FinUnion (K,(singleton (DISJOINT_PAIRS A))) & s c= a implies s = a ) assume that A6: s in FinUnion (K,(singleton (DISJOINT_PAIRS A))) and A7: s c= a ; ::_thesis: s = a consider t being Element of DISJOINT_PAIRS A such that A8: t in K and A9: s in (singleton (DISJOINT_PAIRS A)) . t by A6, SETWISEO:57; s = t by A9, SETWISEO:55; hence s = a by A3, A5, A7, A8, NORMFORM:32; ::_thesis: verum end; hence a in mi (FinUnion (K,(singleton (DISJOINT_PAIRS A)))) by A2, NORMFORM:39; ::_thesis: verum end; A10: mi (FinUnion (K,(singleton (DISJOINT_PAIRS A)))) c= FinUnion (K,(singleton (DISJOINT_PAIRS A))) by NORMFORM:40; consider g being Function of (Fin (DISJOINT_PAIRS A)),(Normal_forms_on A) such that A11: for B being Element of Fin (DISJOINT_PAIRS A) holds g . B = H1(B) from FUNCT_2:sch_4(); reconsider g = g as Function of (Fin (DISJOINT_PAIRS A)), the carrier of (NormForm A) by NORMFORM:def_12; A12: g . ({}. (DISJOINT_PAIRS A)) = mi ({}. (DISJOINT_PAIRS A)) by A11 .= {} by NORMFORM:40, XBOOLE_1:3 .= Bottom (NormForm A) by NORMFORM:57 .= the_unity_wrt the L_join of (NormForm A) by LATTICE2:18 ; A13: now__::_thesis:_for_x,_y_being_Element_of_Fin_(DISJOINT_PAIRS_A)_holds_g_._(x_\/_y)_=_the_L_join_of_(NormForm_A)_._((g_._x),(g_._y)) let x, y be Element of Fin (DISJOINT_PAIRS A); ::_thesis: g . (x \/ y) = the L_join of (NormForm A) . ((g . x),(g . y)) A14: ( @ (g . x) = mi x & @ (g . y) = mi y ) by A11; thus g . (x \/ y) = mi (x \/ y) by A11 .= mi ((mi x) \/ y) by NORMFORM:44 .= mi ((mi x) \/ (mi y)) by NORMFORM:45 .= the L_join of (NormForm A) . ((g . x),(g . y)) by A14, NORMFORM:def_12 ; ::_thesis: verum end; A15: now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_holds_(g_*_(singleton_(DISJOINT_PAIRS_A)))_._a_=_(Atom_A)_._a let a be Element of DISJOINT_PAIRS A; ::_thesis: (g * (singleton (DISJOINT_PAIRS A))) . a = (Atom A) . a thus (g * (singleton (DISJOINT_PAIRS A))) . a = g . ((singleton (DISJOINT_PAIRS A)) . a) by FUNCT_2:15 .= g . {a} by SETWISEO:54 .= mi {a} by A11 .= {a} by NORMFORM:42 .= (Atom A) . a by Def4 ; ::_thesis: verum end; thus FinJoin (K,(Atom A)) = the L_join of (NormForm A) $$ (K,(Atom A)) by LATTICE2:def_3 .= the L_join of (NormForm A) $$ (K,(g * (singleton (DISJOINT_PAIRS A)))) by A15, FUNCT_2:63 .= g . (FinUnion (K,(singleton (DISJOINT_PAIRS A)))) by A12, A13, SETWISEO:53 .= mi (FinUnion (K,(singleton (DISJOINT_PAIRS A)))) by A11 .= FinUnion (K,(singleton (DISJOINT_PAIRS A))) by A10, A1, XBOOLE_0:def_10 ; ::_thesis: verum end; theorem Th10: :: HEYTING1:10 for A being set for u being Element of (NormForm A) holds u = FinJoin ((@ u),(Atom A)) proof let A be set ; ::_thesis: for u being Element of (NormForm A) holds u = FinJoin ((@ u),(Atom A)) let u be Element of (NormForm A); ::_thesis: u = FinJoin ((@ u),(Atom A)) thus u = FinUnion ((@ u),(singleton (DISJOINT_PAIRS A))) by SETWISEO:58 .= FinJoin ((@ u),(Atom A)) by Th9 ; ::_thesis: verum end; Lm2: for A being set for u, v being Element of (NormForm A) st u [= v holds for x being Element of [:(Fin A),(Fin A):] st x in u holds ex b being Element of DISJOINT_PAIRS A st ( b in v & b c= x ) proof let A be set ; ::_thesis: for u, v being Element of (NormForm A) st u [= v holds for x being Element of [:(Fin A),(Fin A):] st x in u holds ex b being Element of DISJOINT_PAIRS A st ( b in v & b c= x ) let u, v be Element of (NormForm A); ::_thesis: ( u [= v implies for x being Element of [:(Fin A),(Fin A):] st x in u holds ex b being Element of DISJOINT_PAIRS A st ( b in v & b c= x ) ) assume u [= v ; ::_thesis: for x being Element of [:(Fin A),(Fin A):] st x in u holds ex b being Element of DISJOINT_PAIRS A st ( b in v & b c= x ) then A1: v = u "\/" v by LATTICES:def_3 .= the L_join of (NormForm A) . (u,v) by LATTICES:def_1 .= mi ((@ u) \/ (@ v)) by NORMFORM:def_12 ; let x be Element of [:(Fin A),(Fin A):]; ::_thesis: ( x in u implies ex b being Element of DISJOINT_PAIRS A st ( b in v & b c= x ) ) assume A2: x in u ; ::_thesis: ex b being Element of DISJOINT_PAIRS A st ( b in v & b c= x ) u = @ u ; then reconsider c = x as Element of DISJOINT_PAIRS A by A2, SETWISEO:9; c in u \/ v by A2, XBOOLE_0:def_3; then consider b being Element of DISJOINT_PAIRS A such that A3: ( b c= c & b in mi ((@ u) \/ (@ v)) ) by NORMFORM:41; take b ; ::_thesis: ( b in v & b c= x ) thus ( b in v & b c= x ) by A1, A3; ::_thesis: verum end; Lm3: for A being set for u, v being Element of (NormForm A) st ( for a being Element of DISJOINT_PAIRS A st a in u holds ex b being Element of DISJOINT_PAIRS A st ( b in v & b c= a ) ) holds u [= v proof let A be set ; ::_thesis: for u, v being Element of (NormForm A) st ( for a being Element of DISJOINT_PAIRS A st a in u holds ex b being Element of DISJOINT_PAIRS A st ( b in v & b c= a ) ) holds u [= v let u, v be Element of (NormForm A); ::_thesis: ( ( for a being Element of DISJOINT_PAIRS A st a in u holds ex b being Element of DISJOINT_PAIRS A st ( b in v & b c= a ) ) implies u [= v ) assume A1: for a being Element of DISJOINT_PAIRS A st a in u holds ex b being Element of DISJOINT_PAIRS A st ( b in v & b c= a ) ; ::_thesis: u [= v A2: mi ((@ u) \/ (@ v)) c= @ v proof let a be Element of DISJOINT_PAIRS A; :: according to HEYTING1:def_1 ::_thesis: ( a in mi ((@ u) \/ (@ v)) implies a in @ v ) assume A3: a in mi ((@ u) \/ (@ v)) ; ::_thesis: a in @ v then a in u \/ v by NORMFORM:36; then ( a in u or a in v ) by XBOOLE_0:def_3; then consider b being Element of DISJOINT_PAIRS A such that A4: b in v and A5: b c= a by A1; b in u \/ v by A4, XBOOLE_0:def_3; hence a in @ v by A3, A4, A5, NORMFORM:38; ::_thesis: verum end; A6: @ v c= mi ((@ u) \/ (@ v)) proof let a be Element of DISJOINT_PAIRS A; :: according to HEYTING1:def_1 ::_thesis: ( a in @ v implies a in mi ((@ u) \/ (@ v)) ) assume A7: a in @ v ; ::_thesis: a in mi ((@ u) \/ (@ v)) then A8: a in mi (@ v) by NORMFORM:42; A9: now__::_thesis:_for_b_being_Element_of_DISJOINT_PAIRS_A_st_b_in_u_\/_v_&_b_c=_a_holds_ b_=_a let b be Element of DISJOINT_PAIRS A; ::_thesis: ( b in u \/ v & b c= a implies b = a ) assume that A10: b in u \/ v and A11: b c= a ; ::_thesis: b = a ( b in u or b in v ) by A10, XBOOLE_0:def_3; then consider c being Element of DISJOINT_PAIRS A such that A12: c in v and A13: c c= b by A1; c = a by A8, A11, A12, A13, NORMFORM:2, NORMFORM:38; hence b = a by A11, A13, NORMFORM:1; ::_thesis: verum end; a in (@ u) \/ (@ v) by A7, XBOOLE_0:def_3; hence a in mi ((@ u) \/ (@ v)) by A9, NORMFORM:39; ::_thesis: verum end; u "\/" v = the L_join of (NormForm A) . (u,v) by LATTICES:def_1 .= mi ((@ u) \/ (@ v)) by NORMFORM:def_12 .= v by A2, A6, XBOOLE_0:def_10 ; hence u [= v by LATTICES:def_3; ::_thesis: verum end; definition let A be set ; func pair_diff A -> BinOp of [:(Fin A),(Fin A):] means :Def5: :: HEYTING1:def 5 for a, b being Element of [:(Fin A),(Fin A):] holds it . (a,b) = a \ b; existence ex b1 being BinOp of [:(Fin A),(Fin A):] st for a, b being Element of [:(Fin A),(Fin A):] holds b1 . (a,b) = a \ b proof deffunc H1( Element of [:(Fin A),(Fin A):], Element of [:(Fin A),(Fin A):]) -> Element of [:(Fin A),(Fin A):] = $1 \ $2; thus ex f being BinOp of [:(Fin A),(Fin A):] st for a, b being Element of [:(Fin A),(Fin A):] holds f . (a,b) = H1(a,b) from BINOP_1:sch_4(); ::_thesis: verum end; correctness uniqueness for b1, b2 being BinOp of [:(Fin A),(Fin A):] st ( for a, b being Element of [:(Fin A),(Fin A):] holds b1 . (a,b) = a \ b ) & ( for a, b being Element of [:(Fin A),(Fin A):] holds b2 . (a,b) = a \ b ) holds b1 = b2; proof let IT, IT9 be BinOp of [:(Fin A),(Fin A):]; ::_thesis: ( ( for a, b being Element of [:(Fin A),(Fin A):] holds IT . (a,b) = a \ b ) & ( for a, b being Element of [:(Fin A),(Fin A):] holds IT9 . (a,b) = a \ b ) implies IT = IT9 ) assume that A1: for a, b being Element of [:(Fin A),(Fin A):] holds IT . (a,b) = a \ b and A2: for a, b being Element of [:(Fin A),(Fin A):] holds IT9 . (a,b) = a \ b ; ::_thesis: IT = IT9 now__::_thesis:_for_a,_b_being_Element_of_[:(Fin_A),(Fin_A):]_holds_IT_._(a,b)_=_IT9_._(a,b) let a, b be Element of [:(Fin A),(Fin A):]; ::_thesis: IT . (a,b) = IT9 . (a,b) IT . (a,b) = a \ b by A1; hence IT . (a,b) = IT9 . (a,b) by A2; ::_thesis: verum end; hence IT = IT9 by BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def5 defines pair_diff HEYTING1:def_5_:_ for A being set for b2 being BinOp of [:(Fin A),(Fin A):] holds ( b2 = pair_diff A iff for a, b being Element of [:(Fin A),(Fin A):] holds b2 . (a,b) = a \ b ); definition let A be set ; let B be Element of Fin (DISJOINT_PAIRS A); func - B -> Element of Fin (DISJOINT_PAIRS A) equals :: HEYTING1:def 6 (DISJOINT_PAIRS A) /\ { [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B ) } ] where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : for s being Element of DISJOINT_PAIRS A st s in B holds g . s in (s `1) \/ (s `2) } ; coherence (DISJOINT_PAIRS A) /\ { [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B ) } ] where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : for s being Element of DISJOINT_PAIRS A st s in B holds g . s in (s `1) \/ (s `2) } is Element of Fin (DISJOINT_PAIRS A) proof deffunc H1( set ) -> set = ($1 `1) \/ ($1 `2); defpred S1[ Function] means $1 .: B c= union { ((s `1) \/ (s `2)) where s is Element of DISJOINT_PAIRS A : s in B } ; defpred S2[ Function] means for s being Element of DISJOINT_PAIRS A st s in B holds $1 . s in (s `1) \/ (s `2); deffunc H2( Element of Funcs ((DISJOINT_PAIRS A),[A])) -> set = [ { ($1 . s1) where s1 is Element of DISJOINT_PAIRS A : ( $1 . s1 in s1 `2 & s1 in B ) } , { ($1 . s2) where s2 is Element of DISJOINT_PAIRS A : ( $1 . s2 in s2 `1 & s2 in B ) } ]; set N = { H2(g) where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : for s being Element of DISJOINT_PAIRS A st s in B holds g . s in (s `1) \/ (s `2) } ; set N9 = { H2(g) where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : g .: B c= union { ((s `1) \/ (s `2)) where s is Element of DISJOINT_PAIRS A : s in B } } ; set M = (DISJOINT_PAIRS A) /\ { H2(g) where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : for s being Element of DISJOINT_PAIRS A st s in B holds g . s in (s `1) \/ (s `2) } ; A1: now__::_thesis:_for_X_being_set_st_X_in__{__((s_`1)_\/_(s_`2))_where_s_is_Element_of_DISJOINT_PAIRS_A_:_s_in_B__}__holds_ X_is_finite let X be set ; ::_thesis: ( X in { ((s `1) \/ (s `2)) where s is Element of DISJOINT_PAIRS A : s in B } implies X is finite ) assume X in { ((s `1) \/ (s `2)) where s is Element of DISJOINT_PAIRS A : s in B } ; ::_thesis: X is finite then ex s being Element of DISJOINT_PAIRS A st ( X = (s `1) \/ (s `2) & s in B ) ; hence X is finite ; ::_thesis: verum end; A2: now__::_thesis:_for_g,_h_being_Element_of_Funcs_((DISJOINT_PAIRS_A),[A])_st_g_|_B_=_h_|_B_holds_ H2(g)_=_H2(h) let g, h be Element of Funcs ((DISJOINT_PAIRS A),[A]); ::_thesis: ( g | B = h | B implies H2(g) = H2(h) ) defpred S3[ set ] means g . $1 in $1 `1 ; defpred S4[ set ] means g . $1 in $1 `2 ; defpred S5[ set ] means h . $1 in $1 `1 ; defpred S6[ set ] means h . $1 in $1 `2 ; assume A3: g | B = h | B ; ::_thesis: H2(g) = H2(h) then A4: for s being Element of DISJOINT_PAIRS A st s in B holds ( S3[s] iff S5[s] ) by FRAENKEL:1; A5: { (g . s2) where s2 is Element of DISJOINT_PAIRS A : ( S3[s2] & s2 in B ) } = { (h . t2) where t2 is Element of DISJOINT_PAIRS A : ( S5[t2] & t2 in B ) } from FRAENKEL:sch_9(A3, A4); A6: for s being Element of DISJOINT_PAIRS A st s in B holds ( S4[s] iff S6[s] ) by A3, FRAENKEL:1; { (g . s1) where s1 is Element of DISJOINT_PAIRS A : ( S4[s1] & s1 in B ) } = { (h . t1) where t1 is Element of DISJOINT_PAIRS A : ( S6[t1] & t1 in B ) } from FRAENKEL:sch_9(A3, A6); hence H2(g) = H2(h) by A5; ::_thesis: verum end; A7: for g being Element of Funcs ((DISJOINT_PAIRS A),[A]) st S2[g] holds S1[g] proof let g be Element of Funcs ((DISJOINT_PAIRS A),[A]); ::_thesis: ( S2[g] implies S1[g] ) assume A8: for s being Element of DISJOINT_PAIRS A st s in B holds g . s in (s `1) \/ (s `2) ; ::_thesis: S1[g] let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in g .: B or x in union { ((s `1) \/ (s `2)) where s is Element of DISJOINT_PAIRS A : s in B } ) assume x in g .: B ; ::_thesis: x in union { ((s `1) \/ (s `2)) where s is Element of DISJOINT_PAIRS A : s in B } then consider y being set such that A9: y in dom g and A10: y in B and A11: x = g . y by FUNCT_1:def_6; reconsider y = y as Element of DISJOINT_PAIRS A by A9; A12: (y `1) \/ (y `2) in { ((s `1) \/ (s `2)) where s is Element of DISJOINT_PAIRS A : s in B } by A10; g . y in (y `1) \/ (y `2) by A8, A10; hence x in union { ((s `1) \/ (s `2)) where s is Element of DISJOINT_PAIRS A : s in B } by A11, A12, TARSKI:def_4; ::_thesis: verum end; A13: { H2(g) where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : S2[g] } c= { H2(g) where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : S1[g] } from FRAENKEL:sch_1(A7); A14: B is finite ; { H1(s) where s is Element of DISJOINT_PAIRS A : s in B } is finite from FRAENKEL:sch_21(A14); then A15: union { ((s `1) \/ (s `2)) where s is Element of DISJOINT_PAIRS A : s in B } is finite by A1, FINSET_1:7; A16: { H2(g) where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : g .: B c= union { ((s `1) \/ (s `2)) where s is Element of DISJOINT_PAIRS A : s in B } } is finite from FRAENKEL:sch_25(A14, A15, A2); (DISJOINT_PAIRS A) /\ { H2(g) where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : for s being Element of DISJOINT_PAIRS A st s in B holds g . s in (s `1) \/ (s `2) } c= DISJOINT_PAIRS A by XBOOLE_1:17; hence (DISJOINT_PAIRS A) /\ { [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B ) } ] where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : for s being Element of DISJOINT_PAIRS A st s in B holds g . s in (s `1) \/ (s `2) } is Element of Fin (DISJOINT_PAIRS A) by A13, A16, FINSUB_1:def_5; ::_thesis: verum end; correctness ; let C be Element of Fin (DISJOINT_PAIRS A); funcB =>> C -> Element of Fin (DISJOINT_PAIRS A) equals :: HEYTING1:def 7 (DISJOINT_PAIRS A) /\ { (FinPairUnion (B,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: B c= C } ; coherence (DISJOINT_PAIRS A) /\ { (FinPairUnion (B,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: B c= C } is Element of Fin (DISJOINT_PAIRS A) proof deffunc H1( Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):])) -> Element of [:(Fin A),(Fin A):] = FinPairUnion (B,((pair_diff A) .: ($1,(incl (DISJOINT_PAIRS A))))); set N = { (FinPairUnion (B,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: B c= C } ; set IT = (DISJOINT_PAIRS A) /\ { (FinPairUnion (B,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: B c= C } ; A17: (DISJOINT_PAIRS A) /\ { (FinPairUnion (B,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: B c= C } c= DISJOINT_PAIRS A by XBOOLE_1:17; A18: now__::_thesis:_for_f,_f9_being_Element_of_Funcs_((DISJOINT_PAIRS_A),[:(Fin_A),(Fin_A):])_st_f_|_B_=_f9_|_B_holds_ H1(f)_=_H1(f9) let f, f9 be Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]); ::_thesis: ( f | B = f9 | B implies H1(f) = H1(f9) ) assume f | B = f9 | B ; ::_thesis: H1(f) = H1(f9) then ((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))) | B = ((pair_diff A) .: (f9,(incl (DISJOINT_PAIRS A)))) | B by FUNCOP_1:23; hence H1(f) = H1(f9) by NORMFORM:22; ::_thesis: verum end; A19: C is finite ; A20: B is finite ; { H1(f) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: B c= C } is finite from FRAENKEL:sch_25(A20, A19, A18); hence (DISJOINT_PAIRS A) /\ { (FinPairUnion (B,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: B c= C } is Element of Fin (DISJOINT_PAIRS A) by A17, FINSUB_1:def_5; ::_thesis: verum end; correctness ; end; :: deftheorem defines - HEYTING1:def_6_:_ for A being set for B being Element of Fin (DISJOINT_PAIRS A) holds - B = (DISJOINT_PAIRS A) /\ { [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B ) } ] where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : for s being Element of DISJOINT_PAIRS A st s in B holds g . s in (s `1) \/ (s `2) } ; :: deftheorem defines =>> HEYTING1:def_7_:_ for A being set for B, C being Element of Fin (DISJOINT_PAIRS A) holds B =>> C = (DISJOINT_PAIRS A) /\ { (FinPairUnion (B,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: B c= C } ; theorem Th11: :: HEYTING1:11 for A being set for B being Element of Fin (DISJOINT_PAIRS A) for c being Element of DISJOINT_PAIRS A st c in - B holds ex g being Element of Funcs ((DISJOINT_PAIRS A),[A]) st ( ( for s being Element of DISJOINT_PAIRS A st s in B holds g . s in (s `1) \/ (s `2) ) & c = [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B ) } ] ) proof let A be set ; ::_thesis: for B being Element of Fin (DISJOINT_PAIRS A) for c being Element of DISJOINT_PAIRS A st c in - B holds ex g being Element of Funcs ((DISJOINT_PAIRS A),[A]) st ( ( for s being Element of DISJOINT_PAIRS A st s in B holds g . s in (s `1) \/ (s `2) ) & c = [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B ) } ] ) let B be Element of Fin (DISJOINT_PAIRS A); ::_thesis: for c being Element of DISJOINT_PAIRS A st c in - B holds ex g being Element of Funcs ((DISJOINT_PAIRS A),[A]) st ( ( for s being Element of DISJOINT_PAIRS A st s in B holds g . s in (s `1) \/ (s `2) ) & c = [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B ) } ] ) let c be Element of DISJOINT_PAIRS A; ::_thesis: ( c in - B implies ex g being Element of Funcs ((DISJOINT_PAIRS A),[A]) st ( ( for s being Element of DISJOINT_PAIRS A st s in B holds g . s in (s `1) \/ (s `2) ) & c = [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B ) } ] ) ) assume c in - B ; ::_thesis: ex g being Element of Funcs ((DISJOINT_PAIRS A),[A]) st ( ( for s being Element of DISJOINT_PAIRS A st s in B holds g . s in (s `1) \/ (s `2) ) & c = [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B ) } ] ) then c in { [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B ) } ] where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : for s being Element of DISJOINT_PAIRS A st s in B holds g . s in (s `1) \/ (s `2) } by XBOOLE_0:def_4; then ex g being Element of Funcs ((DISJOINT_PAIRS A),[A]) st ( c = [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B ) } ] & ( for s being Element of DISJOINT_PAIRS A st s in B holds g . s in (s `1) \/ (s `2) ) ) ; hence ex g being Element of Funcs ((DISJOINT_PAIRS A),[A]) st ( ( for s being Element of DISJOINT_PAIRS A st s in B holds g . s in (s `1) \/ (s `2) ) & c = [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B ) } ] ) ; ::_thesis: verum end; theorem Th12: :: HEYTING1:12 for A being set holds [{},{}] is Element of DISJOINT_PAIRS A proof let A be set ; ::_thesis: [{},{}] is Element of DISJOINT_PAIRS A ( [{},{}] = [({}. A),({}. A)] & [{},{}] `1 misses [{},{}] `2 ) by XBOOLE_1:65; hence [{},{}] is Element of DISJOINT_PAIRS A by NORMFORM:29; ::_thesis: verum end; theorem Th13: :: HEYTING1:13 for A being set for K being Element of Normal_forms_on A st K = {} holds - K = {[{},{}]} proof let A be set ; ::_thesis: for K being Element of Normal_forms_on A st K = {} holds - K = {[{},{}]} let K be Element of Normal_forms_on A; ::_thesis: ( K = {} implies - K = {[{},{}]} ) assume A1: K = {} ; ::_thesis: - K = {[{},{}]} A2: { [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ] where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : for s being Element of DISJOINT_PAIRS A st s in K holds g . s in (s `1) \/ (s `2) } = {[{},{}]} proof thus { [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ] where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : for s being Element of DISJOINT_PAIRS A st s in K holds g . s in (s `1) \/ (s `2) } c= {[{},{}]} :: according to XBOOLE_0:def_10 ::_thesis: {[{},{}]} c= { [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ] where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : for s being Element of DISJOINT_PAIRS A st s in K holds g . s in (s `1) \/ (s `2) } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ] where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : for s being Element of DISJOINT_PAIRS A st s in K holds g . s in (s `1) \/ (s `2) } or x in {[{},{}]} ) assume x in { [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ] where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : for s being Element of DISJOINT_PAIRS A st s in K holds g . s in (s `1) \/ (s `2) } ; ::_thesis: x in {[{},{}]} then consider g being Element of Funcs ((DISJOINT_PAIRS A),[A]) such that A3: x = [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ] and for s being Element of DISJOINT_PAIRS A st s in K holds g . s in (s `1) \/ (s `2) ; A4: x `2 = { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } by A3, MCART_1:7; A5: now__::_thesis:_not_x_`2_<>_{} set y = the Element of x `2 ; assume x `2 <> {} ; ::_thesis: contradiction then the Element of x `2 in x `2 ; then ex t1 being Element of DISJOINT_PAIRS A st ( the Element of x `2 = g . t1 & g . t1 in t1 `1 & t1 in K ) by A4; hence contradiction by A1; ::_thesis: verum end; A6: x `1 = { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } by A3, MCART_1:7; now__::_thesis:_not_x_`1_<>_{} set y = the Element of x `1 ; assume x `1 <> {} ; ::_thesis: contradiction then the Element of x `1 in x `1 ; then ex t1 being Element of DISJOINT_PAIRS A st ( the Element of x `1 = g . t1 & g . t1 in t1 `2 & t1 in K ) by A6; hence contradiction by A1; ::_thesis: verum end; then x = [{},{}] by A3, A5, MCART_1:8; hence x in {[{},{}]} by TARSKI:def_1; ::_thesis: verum end; thus {[{},{}]} c= { [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ] where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : for s being Element of DISJOINT_PAIRS A st s in K holds g . s in (s `1) \/ (s `2) } ::_thesis: verum proof set g = the Element of Funcs ((DISJOINT_PAIRS A),[A]); let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {[{},{}]} or x in { [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ] where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : for s being Element of DISJOINT_PAIRS A st s in K holds g . s in (s `1) \/ (s `2) } ) assume x in {[{},{}]} ; ::_thesis: x in { [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ] where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : for s being Element of DISJOINT_PAIRS A st s in K holds g . s in (s `1) \/ (s `2) } then A7: x = [{},{}] by TARSKI:def_1; A8: now__::_thesis:_not__{__(_the_Element_of_Funcs_((DISJOINT_PAIRS_A),[A])_._t1)_where_t1_is_Element_of_DISJOINT_PAIRS_A_:_(_the_Element_of_Funcs_((DISJOINT_PAIRS_A),[A])_._t1_in_t1_`2_&_t1_in_K_)__}__<>_{} set y = the Element of { ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1) where t1 is Element of DISJOINT_PAIRS A : ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1 in t1 `2 & t1 in K ) } ; assume { ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1) where t1 is Element of DISJOINT_PAIRS A : ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1 in t1 `2 & t1 in K ) } <> {} ; ::_thesis: contradiction then the Element of { ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1) where t1 is Element of DISJOINT_PAIRS A : ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1 in t1 `2 & t1 in K ) } in { ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1) where t1 is Element of DISJOINT_PAIRS A : ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1 in t1 `2 & t1 in K ) } ; then ex t1 being Element of DISJOINT_PAIRS A st ( the Element of { ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1) where t1 is Element of DISJOINT_PAIRS A : ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1 in t1 `2 & t1 in K ) } = the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1 & the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1 in t1 `2 & t1 in K ) ; hence contradiction by A1; ::_thesis: verum end; A9: now__::_thesis:_not__{__(_the_Element_of_Funcs_((DISJOINT_PAIRS_A),[A])_._t2)_where_t2_is_Element_of_DISJOINT_PAIRS_A_:_(_the_Element_of_Funcs_((DISJOINT_PAIRS_A),[A])_._t2_in_t2_`1_&_t2_in_K_)__}__<>_{} set y = the Element of { ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t2) where t2 is Element of DISJOINT_PAIRS A : ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t2 in t2 `1 & t2 in K ) } ; assume { ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t2) where t2 is Element of DISJOINT_PAIRS A : ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t2 in t2 `1 & t2 in K ) } <> {} ; ::_thesis: contradiction then the Element of { ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t2) where t2 is Element of DISJOINT_PAIRS A : ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t2 in t2 `1 & t2 in K ) } in { ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t2) where t2 is Element of DISJOINT_PAIRS A : ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t2 in t2 `1 & t2 in K ) } ; then ex t1 being Element of DISJOINT_PAIRS A st ( the Element of { ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t2) where t2 is Element of DISJOINT_PAIRS A : ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t2 in t2 `1 & t2 in K ) } = the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1 & the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1 in t1 `1 & t1 in K ) ; hence contradiction by A1; ::_thesis: verum end; for s being Element of DISJOINT_PAIRS A st s in K holds the Element of Funcs ((DISJOINT_PAIRS A),[A]) . s in (s `1) \/ (s `2) by A1; hence x in { [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ] where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : for s being Element of DISJOINT_PAIRS A st s in K holds g . s in (s `1) \/ (s `2) } by A7, A8, A9; ::_thesis: verum end; end; [{},{}] is Element of DISJOINT_PAIRS A by Th12; hence - K = {[{},{}]} by A2, ZFMISC_1:46; ::_thesis: verum end; theorem Th14: :: HEYTING1:14 for A being set for K, L being Element of Normal_forms_on A st K = {} & L = {} holds K =>> L = {[{},{}]} proof let A be set ; ::_thesis: for K, L being Element of Normal_forms_on A st K = {} & L = {} holds K =>> L = {[{},{}]} let K, L be Element of Normal_forms_on A; ::_thesis: ( K = {} & L = {} implies K =>> L = {[{},{}]} ) assume that A1: K = {} and A2: L = {} ; ::_thesis: K =>> L = {[{},{}]} A3: {} = {}. A ; A4: K = {}. (DISJOINT_PAIRS A) by A1; A5: now__::_thesis:_for_f_being_Element_of_Funcs_((DISJOINT_PAIRS_A),[:(Fin_A),(Fin_A):])_holds_FinPairUnion_(K,((pair_diff_A)_.:_(f,(incl_(DISJOINT_PAIRS_A)))))_=_[{},{}] let f be Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]); ::_thesis: FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A))))) = [{},{}] thus FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A))))) = the_unity_wrt (FinPairUnion A) by A4, NORMFORM:18, SETWISEO:31 .= [{},{}] by A3, NORMFORM:19 ; ::_thesis: verum end; A6: { (FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: K c= L } = {[{},{}]} proof thus { (FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: K c= L } c= {[{},{}]} :: according to XBOOLE_0:def_10 ::_thesis: {[{},{}]} c= { (FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: K c= L } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: K c= L } or x in {[{},{}]} ) assume x in { (FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: K c= L } ; ::_thesis: x in {[{},{}]} then ex f being Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) st ( x = FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A))))) & f .: K c= L ) ; then x = [{},{}] by A5; hence x in {[{},{}]} by TARSKI:def_1; ::_thesis: verum end; thus {[{},{}]} c= { (FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: K c= L } ::_thesis: verum proof set f9 = the Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]); let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {[{},{}]} or x in { (FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: K c= L } ) assume x in {[{},{}]} ; ::_thesis: x in { (FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: K c= L } then x = [{},{}] by TARSKI:def_1; then A7: x = FinPairUnion (K,((pair_diff A) .: ( the Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]),(incl (DISJOINT_PAIRS A))))) by A5; the Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) .: K c= L by A1, A2; hence x in { (FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: K c= L } by A7; ::_thesis: verum end; end; [{},{}] is Element of DISJOINT_PAIRS A by Th12; hence K =>> L = {[{},{}]} by A6, ZFMISC_1:46; ::_thesis: verum end; theorem Th15: :: HEYTING1:15 for a being Element of DISJOINT_PAIRS {} holds a = [{},{}] proof let a be Element of DISJOINT_PAIRS {}; ::_thesis: a = [{},{}] consider x, y being Element of Fin {} such that A1: a = [x,y] by DOMAIN_1:1; x = {} by FINSUB_1:15, TARSKI:def_1; hence a = [{},{}] by A1, FINSUB_1:15, TARSKI:def_1; ::_thesis: verum end; theorem Th16: :: HEYTING1:16 DISJOINT_PAIRS {} = {[{},{}]} proof thus DISJOINT_PAIRS {} c= {[{},{}]} :: according to XBOOLE_0:def_10 ::_thesis: {[{},{}]} c= DISJOINT_PAIRS {} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in DISJOINT_PAIRS {} or x in {[{},{}]} ) assume x in DISJOINT_PAIRS {} ; ::_thesis: x in {[{},{}]} then x = [{},{}] by Th15; hence x in {[{},{}]} by TARSKI:def_1; ::_thesis: verum end; thus {[{},{}]} c= DISJOINT_PAIRS {} ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {[{},{}]} or x in DISJOINT_PAIRS {} ) assume x in {[{},{}]} ; ::_thesis: x in DISJOINT_PAIRS {} then x = [{},{}] by TARSKI:def_1; then x is Element of DISJOINT_PAIRS {} by Th12; hence x in DISJOINT_PAIRS {} ; ::_thesis: verum end; end; Lm4: Fin (DISJOINT_PAIRS {}) = {{},{[{},{}]}} proof thus Fin (DISJOINT_PAIRS {}) = bool (DISJOINT_PAIRS {}) by Th16, FINSUB_1:14 .= {{},{[{},{}]}} by Th16, ZFMISC_1:24 ; ::_thesis: verum end; theorem Th17: :: HEYTING1:17 for A being set holds {[{},{}]} is Element of Normal_forms_on A proof let A be set ; ::_thesis: {[{},{}]} is Element of Normal_forms_on A [{},{}] is Element of DISJOINT_PAIRS A by Th12; then {[{},{}]} c= DISJOINT_PAIRS A by ZFMISC_1:31; then reconsider B = {[{},{}]} as Element of Fin (DISJOINT_PAIRS A) by FINSUB_1:def_5; now__::_thesis:_for_a,_b_being_Element_of_DISJOINT_PAIRS_A_st_a_in_B_&_b_in_B_&_a_c=_b_holds_ a_=_b let a, b be Element of DISJOINT_PAIRS A; ::_thesis: ( a in B & b in B & a c= b implies a = b ) assume that A1: a in B and A2: b in B and a c= b ; ::_thesis: a = b a = [{},{}] by A1, TARSKI:def_1; hence a = b by A2, TARSKI:def_1; ::_thesis: verum end; hence {[{},{}]} is Element of Normal_forms_on A by NORMFORM:33; ::_thesis: verum end; theorem Th18: :: HEYTING1:18 for A being set for B, C being Element of Fin (DISJOINT_PAIRS A) for c being Element of DISJOINT_PAIRS A st c in B =>> C holds ex f being Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) st ( f .: B c= C & c = FinPairUnion (B,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A))))) ) proof let A be set ; ::_thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) for c being Element of DISJOINT_PAIRS A st c in B =>> C holds ex f being Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) st ( f .: B c= C & c = FinPairUnion (B,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A))))) ) let B, C be Element of Fin (DISJOINT_PAIRS A); ::_thesis: for c being Element of DISJOINT_PAIRS A st c in B =>> C holds ex f being Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) st ( f .: B c= C & c = FinPairUnion (B,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A))))) ) let c be Element of DISJOINT_PAIRS A; ::_thesis: ( c in B =>> C implies ex f being Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) st ( f .: B c= C & c = FinPairUnion (B,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A))))) ) ) assume c in B =>> C ; ::_thesis: ex f being Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) st ( f .: B c= C & c = FinPairUnion (B,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A))))) ) then c in { (FinPairUnion (B,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: B c= C } by XBOOLE_0:def_4; then ex f being Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) st ( c = FinPairUnion (B,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A))))) & f .: B c= C ) ; hence ex f being Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) st ( f .: B c= C & c = FinPairUnion (B,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A))))) ) ; ::_thesis: verum end; theorem Th19: :: HEYTING1:19 for A being set for a being Element of DISJOINT_PAIRS A for K being Element of Normal_forms_on A st K ^ {a} = {} holds ex b being Element of DISJOINT_PAIRS A st ( b in - K & b c= a ) proof let A be set ; ::_thesis: for a being Element of DISJOINT_PAIRS A for K being Element of Normal_forms_on A st K ^ {a} = {} holds ex b being Element of DISJOINT_PAIRS A st ( b in - K & b c= a ) let a be Element of DISJOINT_PAIRS A; ::_thesis: for K being Element of Normal_forms_on A st K ^ {a} = {} holds ex b being Element of DISJOINT_PAIRS A st ( b in - K & b c= a ) let K be Element of Normal_forms_on A; ::_thesis: ( K ^ {a} = {} implies ex b being Element of DISJOINT_PAIRS A st ( b in - K & b c= a ) ) assume A1: K ^ {a} = {} ; ::_thesis: ex b being Element of DISJOINT_PAIRS A st ( b in - K & b c= a ) now__::_thesis:_ex_c_being_Element_of_DISJOINT_PAIRS_A_st_ (_c_in_-_K_&_c_c=_a_) percases ( not A is empty or A is empty ) ; supposeA2: not A is empty ; ::_thesis: ex c being Element of DISJOINT_PAIRS A st ( c in - K & c c= a ) defpred S1[ set , set ] means $2 in (($1 `1) /\ (a `2)) \/ (($1 `2) /\ (a `1)); A3: A = [A] by A2, Def2; A4: now__::_thesis:_for_s_being_Element_of_DISJOINT_PAIRS_A_st_s_in_K_holds_ ex_x_being_Element_of_[A]_st_S1[s,x] A5: a in {a} by TARSKI:def_1; let s be Element of DISJOINT_PAIRS A; ::_thesis: ( s in K implies ex x being Element of [A] st S1[s,x] ) assume s in K ; ::_thesis: ex x being Element of [A] st S1[s,x] then not s \/ a in DISJOINT_PAIRS A by A1, A5, NORMFORM:35; then consider x being Element of [A] such that A6: ( ( x in s `1 & x in a `2 ) or ( x in a `1 & x in s `2 ) ) by A3, NORMFORM:28; take x = x; ::_thesis: S1[s,x] ( x in (s `1) /\ (a `2) or x in (s `2) /\ (a `1) ) by A6, XBOOLE_0:def_4; hence S1[s,x] by XBOOLE_0:def_3; ::_thesis: verum end; consider g being Element of Funcs ((DISJOINT_PAIRS A),[A]) such that A7: for s being Element of DISJOINT_PAIRS A st s in K holds S1[s,g . s] from FRAENKEL:sch_27(A4); set c1 = { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } ; set c2 = { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ; A8: { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } c= a `2 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } or x in a `2 ) assume x in { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ; ::_thesis: x in a `2 then consider t being Element of DISJOINT_PAIRS A such that A9: ( x = g . t & g . t in t `1 ) and A10: t in K ; g . t in ((t `1) /\ (a `2)) \/ ((t `2) /\ (a `1)) by A7, A10; then ( g . t in (t `1) /\ (a `2) or g . t in (t `2) /\ (a `1) ) by XBOOLE_0:def_3; then ( ( g . t in t `1 & g . t in a `2 ) or ( g . t in t `2 & g . t in a `1 ) ) by XBOOLE_0:def_4; hence x in a `2 by A9, NORMFORM:27; ::_thesis: verum end; A11: { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } c= a `1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } or x in a `1 ) assume x in { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } ; ::_thesis: x in a `1 then consider t being Element of DISJOINT_PAIRS A such that A12: ( x = g . t & g . t in t `2 ) and A13: t in K ; g . t in ((t `1) /\ (a `2)) \/ ((t `2) /\ (a `1)) by A7, A13; then ( g . t in (t `1) /\ (a `2) or g . t in (t `2) /\ (a `1) ) by XBOOLE_0:def_3; then ( ( g . t in t `1 & g . t in a `2 ) or ( g . t in t `2 & g . t in a `1 ) ) by XBOOLE_0:def_4; hence x in a `1 by A12, NORMFORM:27; ::_thesis: verum end; then reconsider c = [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ] as Element of DISJOINT_PAIRS A by A8, NORMFORM:30; take c = c; ::_thesis: ( c in - K & c c= a ) now__::_thesis:_for_s_being_Element_of_DISJOINT_PAIRS_A_st_s_in_K_holds_ g_._s_in_(s_`1)_\/_(s_`2) let s be Element of DISJOINT_PAIRS A; ::_thesis: ( s in K implies g . s in (s `1) \/ (s `2) ) assume s in K ; ::_thesis: g . s in (s `1) \/ (s `2) then g . s in ((s `1) /\ (a `2)) \/ ((s `2) /\ (a `1)) by A7; then ( g . s in (s `1) /\ (a `2) or g . s in (s `2) /\ (a `1) ) by XBOOLE_0:def_3; then ( ( g . s in s `1 & g . s in a `2 ) or ( g . s in s `2 & g . s in a `1 ) ) by XBOOLE_0:def_4; hence g . s in (s `1) \/ (s `2) by XBOOLE_0:def_3; ::_thesis: verum end; then c in { [ { (h . t1) where t1 is Element of DISJOINT_PAIRS A : ( h . t1 in t1 `2 & t1 in K ) } , { (h . t2) where t2 is Element of DISJOINT_PAIRS A : ( h . t2 in t2 `1 & t2 in K ) } ] where h is Element of Funcs ((DISJOINT_PAIRS A),[A]) : for s being Element of DISJOINT_PAIRS A st s in K holds h . s in (s `1) \/ (s `2) } ; hence c in - K by XBOOLE_0:def_4; ::_thesis: c c= a ( c `1 = { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } & c `2 = { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ) by MCART_1:7; hence c c= a by A11, A8, NORMFORM:def_1; ::_thesis: verum end; supposeA14: A is empty ; ::_thesis: ex b being Element of DISJOINT_PAIRS A st ( b in - K & b c= a ) reconsider Z = {[{},{}]} as Element of Normal_forms_on {} by Th17; take b = a; ::_thesis: ( b in - K & b c= a ) A15: a = [{},{}] by A14, Th15; mi (Z ^ Z) <> {} by Th3; then K <> {[{},{}]} by A1, A14, A15, NORMFORM:40, XBOOLE_1:3; then K = {} by A14, Lm4, TARSKI:def_2; then - K = {[{},{}]} by Th13; hence b in - K by A15, TARSKI:def_1; ::_thesis: b c= a thus b c= a ; ::_thesis: verum end; end; end; hence ex b being Element of DISJOINT_PAIRS A st ( b in - K & b c= a ) ; ::_thesis: verum end; Lm5: now__::_thesis:_for_A_being_set_ for_K_being_Element_of_Normal_forms_on_A for_b_being_Element_of_DISJOINT_PAIRS_A for_f_being_Element_of_Funcs_((DISJOINT_PAIRS_A),[:(Fin_A),(Fin_A):])_holds_((pair_diff_A)_.:_(f,(incl_(DISJOINT_PAIRS_A))))_._b_=_(f_._b)_\_b let A be set ; ::_thesis: for K being Element of Normal_forms_on A for b being Element of DISJOINT_PAIRS A for f being Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) holds ((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))) . b = (f . b) \ b let K be Element of Normal_forms_on A; ::_thesis: for b being Element of DISJOINT_PAIRS A for f being Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) holds ((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))) . b = (f . b) \ b let b be Element of DISJOINT_PAIRS A; ::_thesis: for f being Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) holds ((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))) . b = (f . b) \ b let f be Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]); ::_thesis: ((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))) . b = (f . b) \ b thus ((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))) . b = (pair_diff A) . ((f . b),((incl (DISJOINT_PAIRS A)) . b)) by FUNCOP_1:37 .= (pair_diff A) . ((f . b),b) by FUNCT_1:18 .= (f . b) \ b by Def5 ; ::_thesis: verum end; theorem Th20: :: HEYTING1:20 for A being set for a being Element of DISJOINT_PAIRS A for u, v being Element of (NormForm A) st ( for c being Element of DISJOINT_PAIRS A st c in u holds ex b being Element of DISJOINT_PAIRS A st ( b in v & b c= c \/ a ) ) holds ex b being Element of DISJOINT_PAIRS A st ( b in (@ u) =>> (@ v) & b c= a ) proof let A be set ; ::_thesis: for a being Element of DISJOINT_PAIRS A for u, v being Element of (NormForm A) st ( for c being Element of DISJOINT_PAIRS A st c in u holds ex b being Element of DISJOINT_PAIRS A st ( b in v & b c= c \/ a ) ) holds ex b being Element of DISJOINT_PAIRS A st ( b in (@ u) =>> (@ v) & b c= a ) let a be Element of DISJOINT_PAIRS A; ::_thesis: for u, v being Element of (NormForm A) st ( for c being Element of DISJOINT_PAIRS A st c in u holds ex b being Element of DISJOINT_PAIRS A st ( b in v & b c= c \/ a ) ) holds ex b being Element of DISJOINT_PAIRS A st ( b in (@ u) =>> (@ v) & b c= a ) let u, v be Element of (NormForm A); ::_thesis: ( ( for c being Element of DISJOINT_PAIRS A st c in u holds ex b being Element of DISJOINT_PAIRS A st ( b in v & b c= c \/ a ) ) implies ex b being Element of DISJOINT_PAIRS A st ( b in (@ u) =>> (@ v) & b c= a ) ) defpred S1[ Element of DISJOINT_PAIRS A, Element of [:(Fin A),(Fin A):]] means ( $2 in @ v & $2 c= $1 \/ a ); assume A1: for b being Element of DISJOINT_PAIRS A st b in u holds ex c being Element of DISJOINT_PAIRS A st ( c in v & c c= b \/ a ) ; ::_thesis: ex b being Element of DISJOINT_PAIRS A st ( b in (@ u) =>> (@ v) & b c= a ) A2: now__::_thesis:_for_b_being_Element_of_DISJOINT_PAIRS_A_st_b_in_@_u_holds_ ex_x_being_Element_of_[:(Fin_A),(Fin_A):]_st_S1[b,x] let b be Element of DISJOINT_PAIRS A; ::_thesis: ( b in @ u implies ex x being Element of [:(Fin A),(Fin A):] st S1[b,x] ) assume b in @ u ; ::_thesis: ex x being Element of [:(Fin A),(Fin A):] st S1[b,x] then consider c being Element of DISJOINT_PAIRS A such that A3: ( c in v & c c= b \/ a ) by A1; reconsider c = c as Element of [:(Fin A),(Fin A):] ; take x = c; ::_thesis: S1[b,x] thus S1[b,x] by A3; ::_thesis: verum end; consider f9 being Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) such that A4: for b being Element of DISJOINT_PAIRS A st b in @ u holds S1[b,f9 . b] from FRAENKEL:sch_27(A2); set d = FinPairUnion ((@ u),((pair_diff A) .: (f9,(incl (DISJOINT_PAIRS A))))); A5: now__::_thesis:_for_s_being_Element_of_DISJOINT_PAIRS_A_st_s_in_u_holds_ ((pair_diff_A)_.:_(f9,(incl_(DISJOINT_PAIRS_A))))_._s_c=_a let s be Element of DISJOINT_PAIRS A; ::_thesis: ( s in u implies ((pair_diff A) .: (f9,(incl (DISJOINT_PAIRS A)))) . s c= a ) assume s in u ; ::_thesis: ((pair_diff A) .: (f9,(incl (DISJOINT_PAIRS A)))) . s c= a then A6: f9 . s c= a \/ s by A4; ((pair_diff A) .: (f9,(incl (DISJOINT_PAIRS A)))) . s = (f9 . s) \ s by Lm5; hence ((pair_diff A) .: (f9,(incl (DISJOINT_PAIRS A)))) . s c= a by A6, NORMFORM:15; ::_thesis: verum end; then reconsider d = FinPairUnion ((@ u),((pair_diff A) .: (f9,(incl (DISJOINT_PAIRS A))))) as Element of DISJOINT_PAIRS A by NORMFORM:21, NORMFORM:26; take d ; ::_thesis: ( d in (@ u) =>> (@ v) & d c= a ) for b being Element of DISJOINT_PAIRS A st b in u holds f9 . b in v by A4; then f9 .: (@ u) c= v by SETWISEO:10; then d in { (FinPairUnion ((@ u),((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: (@ u) c= v } ; hence d in (@ u) =>> (@ v) by XBOOLE_0:def_4; ::_thesis: d c= a thus d c= a by A5, NORMFORM:21; ::_thesis: verum end; Lm6: for A being set for a being Element of DISJOINT_PAIRS A for u being Element of (NormForm A) for K being Element of Normal_forms_on A st a in K ^ (K =>> (@ u)) holds ex b being Element of DISJOINT_PAIRS A st ( b in u & b c= a ) proof let A be set ; ::_thesis: for a being Element of DISJOINT_PAIRS A for u being Element of (NormForm A) for K being Element of Normal_forms_on A st a in K ^ (K =>> (@ u)) holds ex b being Element of DISJOINT_PAIRS A st ( b in u & b c= a ) let a be Element of DISJOINT_PAIRS A; ::_thesis: for u being Element of (NormForm A) for K being Element of Normal_forms_on A st a in K ^ (K =>> (@ u)) holds ex b being Element of DISJOINT_PAIRS A st ( b in u & b c= a ) let u be Element of (NormForm A); ::_thesis: for K being Element of Normal_forms_on A st a in K ^ (K =>> (@ u)) holds ex b being Element of DISJOINT_PAIRS A st ( b in u & b c= a ) let K be Element of Normal_forms_on A; ::_thesis: ( a in K ^ (K =>> (@ u)) implies ex b being Element of DISJOINT_PAIRS A st ( b in u & b c= a ) ) assume a in K ^ (K =>> (@ u)) ; ::_thesis: ex b being Element of DISJOINT_PAIRS A st ( b in u & b c= a ) then consider b, c being Element of DISJOINT_PAIRS A such that A1: b in K and A2: c in K =>> (@ u) and A3: a = b \/ c by NORMFORM:34; consider f being Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) such that A4: f .: K c= u and A5: c = FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A))))) by A2, Th18; A6: f . b in f .: K by A1, FUNCT_2:35; u = @ u ; then reconsider d = f . b as Element of DISJOINT_PAIRS A by A4, A6, SETWISEO:9; take d ; ::_thesis: ( d in u & d c= a ) thus d in u by A4, A6; ::_thesis: d c= a ((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))) . b = (f . b) \ b by Lm5; hence d c= a by A1, A3, A5, NORMFORM:14, NORMFORM:16; ::_thesis: verum end; theorem Th21: :: HEYTING1:21 for A being set for K being Element of Normal_forms_on A holds K ^ (- K) = {} proof let A be set ; ::_thesis: for K being Element of Normal_forms_on A holds K ^ (- K) = {} let K be Element of Normal_forms_on A; ::_thesis: K ^ (- K) = {} set x = the Element of K ^ (- K); assume A1: K ^ (- K) <> {} ; ::_thesis: contradiction then reconsider a = the Element of K ^ (- K) as Element of DISJOINT_PAIRS A by SETWISEO:9; consider b, c being Element of DISJOINT_PAIRS A such that A2: b in K and A3: c in - K and A4: a = b \/ c by A1, NORMFORM:34; A5: a `1 = (b `1) \/ (c `1) by A4, MCART_1:7; A6: a `2 = (b `2) \/ (c `2) by A4, MCART_1:7; consider g being Element of Funcs ((DISJOINT_PAIRS A),[A]) such that A7: for s being Element of DISJOINT_PAIRS A st s in K holds g . s in (s `1) \/ (s `2) and A8: c = [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ] by A3, Th11; A9: g . b in (b `1) \/ (b `2) by A2, A7; now__::_thesis:_(_(_g_._b_in_b_`1_&_g_._b_in_a_`1_&_g_._b_in_a_`2_)_or_(_g_._b_in_b_`2_&_g_._b_in_a_`2_&_g_._b_in_a_`1_)_) percases ( g . b in b `1 or g . b in b `2 ) by A9, XBOOLE_0:def_3; caseA10: g . b in b `1 ; ::_thesis: ( g . b in a `1 & g . b in a `2 ) hence g . b in a `1 by A5, XBOOLE_0:def_3; ::_thesis: g . b in a `2 g . b in { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } by A2, A10; then g . b in c `2 by A8, MCART_1:7; hence g . b in a `2 by A6, XBOOLE_0:def_3; ::_thesis: verum end; caseA11: g . b in b `2 ; ::_thesis: ( g . b in a `2 & g . b in a `1 ) hence g . b in a `2 by A6, XBOOLE_0:def_3; ::_thesis: g . b in a `1 g . b in { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } by A2, A11; then g . b in c `1 by A8, MCART_1:7; hence g . b in a `1 by A5, XBOOLE_0:def_3; ::_thesis: verum end; end; end; then (a `1) /\ (a `2) <> {} by XBOOLE_0:def_4; then a `1 meets a `2 by XBOOLE_0:def_7; hence contradiction by NORMFORM:25; ::_thesis: verum end; definition let A be set ; func pseudo_compl A -> UnOp of the carrier of (NormForm A) means :Def8: :: HEYTING1:def 8 for u being Element of (NormForm A) holds it . u = mi (- (@ u)); existence ex b1 being UnOp of the carrier of (NormForm A) st for u being Element of (NormForm A) holds b1 . u = mi (- (@ u)) proof deffunc H1( Element of (NormForm A)) -> Element of Normal_forms_on A = mi (- (@ $1)); consider IT being Function of the carrier of (NormForm A),(Normal_forms_on A) such that A1: for u being Element of (NormForm A) holds IT . u = H1(u) from FUNCT_2:sch_4(); reconsider IT = IT as UnOp of the carrier of (NormForm A) by NORMFORM:def_12; take IT ; ::_thesis: for u being Element of (NormForm A) holds IT . u = mi (- (@ u)) let u be Element of (NormForm A); ::_thesis: IT . u = mi (- (@ u)) thus IT . u = mi (- (@ u)) by A1; ::_thesis: verum end; correctness uniqueness for b1, b2 being UnOp of the carrier of (NormForm A) st ( for u being Element of (NormForm A) holds b1 . u = mi (- (@ u)) ) & ( for u being Element of (NormForm A) holds b2 . u = mi (- (@ u)) ) holds b1 = b2; proof let IT, IT9 be UnOp of the carrier of (NormForm A); ::_thesis: ( ( for u being Element of (NormForm A) holds IT . u = mi (- (@ u)) ) & ( for u being Element of (NormForm A) holds IT9 . u = mi (- (@ u)) ) implies IT = IT9 ) assume that A2: for u being Element of (NormForm A) holds IT . u = mi (- (@ u)) and A3: for u being Element of (NormForm A) holds IT9 . u = mi (- (@ u)) ; ::_thesis: IT = IT9 now__::_thesis:_for_u_being_Element_of_(NormForm_A)_holds_IT_._u_=_IT9_._u let u be Element of (NormForm A); ::_thesis: IT . u = IT9 . u thus IT . u = mi (- (@ u)) by A2 .= IT9 . u by A3 ; ::_thesis: verum end; hence IT = IT9 by FUNCT_2:63; ::_thesis: verum end; func StrongImpl A -> BinOp of the carrier of (NormForm A) means :Def9: :: HEYTING1:def 9 for u, v being Element of (NormForm A) holds it . (u,v) = mi ((@ u) =>> (@ v)); existence ex b1 being BinOp of the carrier of (NormForm A) st for u, v being Element of (NormForm A) holds b1 . (u,v) = mi ((@ u) =>> (@ v)) proof deffunc H1( Element of (NormForm A), Element of (NormForm A)) -> Element of Normal_forms_on A = mi ((@ $1) =>> (@ $2)); consider IT being Function of [: the carrier of (NormForm A), the carrier of (NormForm A):],(Normal_forms_on A) such that A4: for u, v being Element of (NormForm A) holds IT . (u,v) = H1(u,v) from BINOP_1:sch_4(); reconsider IT = IT as BinOp of the carrier of (NormForm A) by NORMFORM:def_12; take IT ; ::_thesis: for u, v being Element of (NormForm A) holds IT . (u,v) = mi ((@ u) =>> (@ v)) let u, v be Element of (NormForm A); ::_thesis: IT . (u,v) = mi ((@ u) =>> (@ v)) thus IT . (u,v) = mi ((@ u) =>> (@ v)) by A4; ::_thesis: verum end; correctness uniqueness for b1, b2 being BinOp of the carrier of (NormForm A) st ( for u, v being Element of (NormForm A) holds b1 . (u,v) = mi ((@ u) =>> (@ v)) ) & ( for u, v being Element of (NormForm A) holds b2 . (u,v) = mi ((@ u) =>> (@ v)) ) holds b1 = b2; proof let IT, IT9 be BinOp of the carrier of (NormForm A); ::_thesis: ( ( for u, v being Element of (NormForm A) holds IT . (u,v) = mi ((@ u) =>> (@ v)) ) & ( for u, v being Element of (NormForm A) holds IT9 . (u,v) = mi ((@ u) =>> (@ v)) ) implies IT = IT9 ) assume that A5: for u, v being Element of (NormForm A) holds IT . (u,v) = mi ((@ u) =>> (@ v)) and A6: for u, v being Element of (NormForm A) holds IT9 . (u,v) = mi ((@ u) =>> (@ v)) ; ::_thesis: IT = IT9 now__::_thesis:_for_u,_v_being_Element_of_(NormForm_A)_holds_IT_._(u,v)_=_IT9_._(u,v) let u, v be Element of (NormForm A); ::_thesis: IT . (u,v) = IT9 . (u,v) thus IT . (u,v) = mi ((@ u) =>> (@ v)) by A5 .= IT9 . (u,v) by A6 ; ::_thesis: verum end; hence IT = IT9 by BINOP_1:2; ::_thesis: verum end; let u be Element of (NormForm A); func SUB u -> Element of Fin the carrier of (NormForm A) equals :: HEYTING1:def 10 bool u; coherence bool u is Element of Fin the carrier of (NormForm A) proof A7: bool u c= the carrier of (NormForm A) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in bool u or x in the carrier of (NormForm A) ) assume x in bool u ; ::_thesis: x in the carrier of (NormForm A) then x is Element of (NormForm A) by Th5; hence x in the carrier of (NormForm A) ; ::_thesis: verum end; u = @ u ; hence bool u is Element of Fin the carrier of (NormForm A) by A7, FINSUB_1:def_5; ::_thesis: verum end; correctness ; func diff u -> UnOp of the carrier of (NormForm A) means :Def11: :: HEYTING1:def 11 for v being Element of (NormForm A) holds it . v = u \ v; existence ex b1 being UnOp of the carrier of (NormForm A) st for v being Element of (NormForm A) holds b1 . v = u \ v proof deffunc H1( Element of (NormForm A)) -> Element of Fin (DISJOINT_PAIRS A) = (@ u) \ (@ $1); consider IT being Function of the carrier of (NormForm A),(Fin (DISJOINT_PAIRS A)) such that A8: for v being Element of (NormForm A) holds IT . v = H1(v) from FUNCT_2:sch_4(); now__::_thesis:_for_v_being_Element_of_(NormForm_A)_holds_IT_._v_in_the_carrier_of_(NormForm_A) let v be Element of (NormForm A); ::_thesis: IT . v in the carrier of (NormForm A) (@ u) \ (@ v) in Normal_forms_on A by Th4, XBOOLE_1:36; then IT . v in Normal_forms_on A by A8; hence IT . v in the carrier of (NormForm A) by NORMFORM:def_12; ::_thesis: verum end; then reconsider IT = IT as UnOp of the carrier of (NormForm A) by Th1; take IT ; ::_thesis: for v being Element of (NormForm A) holds IT . v = u \ v let v be Element of (NormForm A); ::_thesis: IT . v = u \ v v = @ v ; hence IT . v = u \ v by A8; ::_thesis: verum end; correctness uniqueness for b1, b2 being UnOp of the carrier of (NormForm A) st ( for v being Element of (NormForm A) holds b1 . v = u \ v ) & ( for v being Element of (NormForm A) holds b2 . v = u \ v ) holds b1 = b2; proof let IT, IT9 be UnOp of the carrier of (NormForm A); ::_thesis: ( ( for v being Element of (NormForm A) holds IT . v = u \ v ) & ( for v being Element of (NormForm A) holds IT9 . v = u \ v ) implies IT = IT9 ) assume that A9: for v being Element of (NormForm A) holds IT . v = u \ v and A10: for v being Element of (NormForm A) holds IT9 . v = u \ v ; ::_thesis: IT = IT9 now__::_thesis:_for_v_being_Element_of_(NormForm_A)_holds_IT_._v_=_IT9_._v let v be Element of (NormForm A); ::_thesis: IT . v = IT9 . v thus IT . v = u \ v by A9 .= IT9 . v by A10 ; ::_thesis: verum end; hence IT = IT9 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def8 defines pseudo_compl HEYTING1:def_8_:_ for A being set for b2 being UnOp of the carrier of (NormForm A) holds ( b2 = pseudo_compl A iff for u being Element of (NormForm A) holds b2 . u = mi (- (@ u)) ); :: deftheorem Def9 defines StrongImpl HEYTING1:def_9_:_ for A being set for b2 being BinOp of the carrier of (NormForm A) holds ( b2 = StrongImpl A iff for u, v being Element of (NormForm A) holds b2 . (u,v) = mi ((@ u) =>> (@ v)) ); :: deftheorem defines SUB HEYTING1:def_10_:_ for A being set for u being Element of (NormForm A) holds SUB u = bool u; :: deftheorem Def11 defines diff HEYTING1:def_11_:_ for A being set for u being Element of (NormForm A) for b3 being UnOp of the carrier of (NormForm A) holds ( b3 = diff u iff for v being Element of (NormForm A) holds b3 . v = u \ v ); deffunc H1( set ) -> Element of bool [:[: the carrier of (NormForm $1), the carrier of (NormForm $1):], the carrier of (NormForm $1):] = the L_join of (NormForm $1); deffunc H2( set ) -> Element of bool [:[: the carrier of (NormForm $1), the carrier of (NormForm $1):], the carrier of (NormForm $1):] = the L_meet of (NormForm $1); Lm7: for A being set for u, v being Element of (NormForm A) st v in SUB u holds v "\/" ((diff u) . v) = u proof let A be set ; ::_thesis: for u, v being Element of (NormForm A) st v in SUB u holds v "\/" ((diff u) . v) = u let u, v be Element of (NormForm A); ::_thesis: ( v in SUB u implies v "\/" ((diff u) . v) = u ) assume A1: v in SUB u ; ::_thesis: v "\/" ((diff u) . v) = u A2: (@ u) \ (@ v) = @ ((diff u) . v) by Def11; thus v "\/" ((diff u) . v) = H1(A) . (v,((diff u) . v)) by LATTICES:def_1 .= mi ((@ v) \/ ((@ u) \ (@ v))) by A2, NORMFORM:def_12 .= mi (@ u) by A1, XBOOLE_1:45 .= u by NORMFORM:42 ; ::_thesis: verum end; theorem Th22: :: HEYTING1:22 for A being set for u, v being Element of (NormForm A) holds (diff u) . v [= u proof let A be set ; ::_thesis: for u, v being Element of (NormForm A) holds (diff u) . v [= u let u, v be Element of (NormForm A); ::_thesis: (diff u) . v [= u (diff u) . v = u \ v by Def11; then for a being Element of DISJOINT_PAIRS A st a in (diff u) . v holds ex b being Element of DISJOINT_PAIRS A st ( b in u & b c= a ) ; hence (diff u) . v [= u by Lm3; ::_thesis: verum end; Lm8: for A being set for a being Element of DISJOINT_PAIRS A for u being Element of (NormForm A) ex v being Element of (NormForm A) st ( v in SUB u & (@ v) ^ {a} = {} & ( for b being Element of DISJOINT_PAIRS A st b in (diff u) . v holds b \/ a in DISJOINT_PAIRS A ) ) proof let A be set ; ::_thesis: for a being Element of DISJOINT_PAIRS A for u being Element of (NormForm A) ex v being Element of (NormForm A) st ( v in SUB u & (@ v) ^ {a} = {} & ( for b being Element of DISJOINT_PAIRS A st b in (diff u) . v holds b \/ a in DISJOINT_PAIRS A ) ) let a be Element of DISJOINT_PAIRS A; ::_thesis: for u being Element of (NormForm A) ex v being Element of (NormForm A) st ( v in SUB u & (@ v) ^ {a} = {} & ( for b being Element of DISJOINT_PAIRS A st b in (diff u) . v holds b \/ a in DISJOINT_PAIRS A ) ) let u be Element of (NormForm A); ::_thesis: ex v being Element of (NormForm A) st ( v in SUB u & (@ v) ^ {a} = {} & ( for b being Element of DISJOINT_PAIRS A st b in (diff u) . v holds b \/ a in DISJOINT_PAIRS A ) ) defpred S1[ set ] means verum; deffunc H3( set ) -> set = $1; defpred S2[ Element of DISJOINT_PAIRS A] means not $1 \/ a in DISJOINT_PAIRS A; set M = { H3(s) where s is Element of DISJOINT_PAIRS A : ( H3(s) in u & S2[s] ) } ; deffunc H4( Element of DISJOINT_PAIRS A) -> Element of [:(Fin A),(Fin A):] = $1 \/ a; defpred S3[ set ] means $1 in u; defpred S4[ Element of DISJOINT_PAIRS A] means ( S3[$1] & S2[$1] ); A1: { H4(t) where t is Element of DISJOINT_PAIRS A : ( t in { s where s is Element of DISJOINT_PAIRS A : S4[s] } & S1[t] ) } = { H4(s) where s is Element of DISJOINT_PAIRS A : ( S4[s] & S1[s] ) } from FRAENKEL:sch_14(); defpred S5[ set , set ] means $1 in { H3(s) where s is Element of DISJOINT_PAIRS A : ( H3(s) in u & S2[s] ) } ; defpred S6[ set , set ] means ( $1 in { H3(s) where s is Element of DISJOINT_PAIRS A : ( H3(s) in u & S2[s] ) } & $2 in {a} ); A2: { H4(s1) where s1 is Element of DISJOINT_PAIRS A : ( S4[s1] & S1[s1] ) } = { H4(s2) where s2 is Element of DISJOINT_PAIRS A : S4[s2] } proof thus { H4(s1) where s1 is Element of DISJOINT_PAIRS A : ( S4[s1] & S1[s1] ) } c= { H4(s2) where s2 is Element of DISJOINT_PAIRS A : S4[s2] } :: according to XBOOLE_0:def_10 ::_thesis: { H4(s2) where s2 is Element of DISJOINT_PAIRS A : S4[s2] } c= { H4(s1) where s1 is Element of DISJOINT_PAIRS A : ( S4[s1] & S1[s1] ) } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { H4(s1) where s1 is Element of DISJOINT_PAIRS A : ( S4[s1] & S1[s1] ) } or x in { H4(s2) where s2 is Element of DISJOINT_PAIRS A : S4[s2] } ) assume x in { H4(s1) where s1 is Element of DISJOINT_PAIRS A : ( S4[s1] & S1[s1] ) } ; ::_thesis: x in { H4(s2) where s2 is Element of DISJOINT_PAIRS A : S4[s2] } then ex s1 being Element of DISJOINT_PAIRS A st ( x = H4(s1) & S4[s1] & S1[s1] ) ; hence x in { H4(s2) where s2 is Element of DISJOINT_PAIRS A : S4[s2] } ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { H4(s2) where s2 is Element of DISJOINT_PAIRS A : S4[s2] } or x in { H4(s1) where s1 is Element of DISJOINT_PAIRS A : ( S4[s1] & S1[s1] ) } ) assume x in { H4(s1) where s1 is Element of DISJOINT_PAIRS A : S4[s1] } ; ::_thesis: x in { H4(s1) where s1 is Element of DISJOINT_PAIRS A : ( S4[s1] & S1[s1] ) } then ex s1 being Element of DISJOINT_PAIRS A st ( x = H4(s1) & S4[s1] ) ; hence x in { H4(s1) where s1 is Element of DISJOINT_PAIRS A : ( S4[s1] & S1[s1] ) } ; ::_thesis: verum end; A3: { H3(s) where s is Element of DISJOINT_PAIRS A : ( H3(s) in u & S2[s] ) } c= u from FRAENKEL:sch_17(); then reconsider v = { H3(s) where s is Element of DISJOINT_PAIRS A : ( H3(s) in u & S2[s] ) } as Element of (NormForm A) by Th5; take v ; ::_thesis: ( v in SUB u & (@ v) ^ {a} = {} & ( for b being Element of DISJOINT_PAIRS A st b in (diff u) . v holds b \/ a in DISJOINT_PAIRS A ) ) thus v in SUB u by A3; ::_thesis: ( (@ v) ^ {a} = {} & ( for b being Element of DISJOINT_PAIRS A st b in (diff u) . v holds b \/ a in DISJOINT_PAIRS A ) ) defpred S7[ set , set ] means ( $2 = a & $1 in { H3(s) where s is Element of DISJOINT_PAIRS A : ( H3(s) in u & S2[s] ) } ); deffunc H5( Element of DISJOINT_PAIRS A, Element of DISJOINT_PAIRS A) -> Element of [:(Fin A),(Fin A):] = $1 \/ $2; A4: { H4(t) where t is Element of DISJOINT_PAIRS A : ( t in { s where s is Element of DISJOINT_PAIRS A : S4[s] } & S1[t] ) } = { H4(t1) where t1 is Element of DISJOINT_PAIRS A : t1 in { s1 where s1 is Element of DISJOINT_PAIRS A : S4[s1] } } proof thus { H4(t) where t is Element of DISJOINT_PAIRS A : ( t in { s where s is Element of DISJOINT_PAIRS A : S4[s] } & S1[t] ) } c= { H4(t1) where t1 is Element of DISJOINT_PAIRS A : t1 in { s1 where s1 is Element of DISJOINT_PAIRS A : S4[s1] } } :: according to XBOOLE_0:def_10 ::_thesis: { H4(t1) where t1 is Element of DISJOINT_PAIRS A : t1 in { s1 where s1 is Element of DISJOINT_PAIRS A : S4[s1] } } c= { H4(t) where t is Element of DISJOINT_PAIRS A : ( t in { s where s is Element of DISJOINT_PAIRS A : S4[s] } & S1[t] ) } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { H4(t) where t is Element of DISJOINT_PAIRS A : ( t in { s where s is Element of DISJOINT_PAIRS A : S4[s] } & S1[t] ) } or x in { H4(t1) where t1 is Element of DISJOINT_PAIRS A : t1 in { s1 where s1 is Element of DISJOINT_PAIRS A : S4[s1] } } ) assume x in { H4(t) where t is Element of DISJOINT_PAIRS A : ( t in { s where s is Element of DISJOINT_PAIRS A : S4[s] } & S1[t] ) } ; ::_thesis: x in { H4(t1) where t1 is Element of DISJOINT_PAIRS A : t1 in { s1 where s1 is Element of DISJOINT_PAIRS A : S4[s1] } } then ex t being Element of DISJOINT_PAIRS A st ( x = H4(t) & t in { s where s is Element of DISJOINT_PAIRS A : S4[s] } & S1[t] ) ; hence x in { H4(t1) where t1 is Element of DISJOINT_PAIRS A : t1 in { s1 where s1 is Element of DISJOINT_PAIRS A : S4[s1] } } ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { H4(t1) where t1 is Element of DISJOINT_PAIRS A : t1 in { s1 where s1 is Element of DISJOINT_PAIRS A : S4[s1] } } or x in { H4(t) where t is Element of DISJOINT_PAIRS A : ( t in { s where s is Element of DISJOINT_PAIRS A : S4[s] } & S1[t] ) } ) assume x in { H4(t) where t is Element of DISJOINT_PAIRS A : t in { s where s is Element of DISJOINT_PAIRS A : S4[s] } } ; ::_thesis: x in { H4(t) where t is Element of DISJOINT_PAIRS A : ( t in { s where s is Element of DISJOINT_PAIRS A : S4[s] } & S1[t] ) } then ex t being Element of DISJOINT_PAIRS A st ( x = H4(t) & t in { s where s is Element of DISJOINT_PAIRS A : S4[s] } ) ; hence x in { H4(t) where t is Element of DISJOINT_PAIRS A : ( t in { s where s is Element of DISJOINT_PAIRS A : S4[s] } & S1[t] ) } ; ::_thesis: verum end; A5: { H5(s,t) where s, t is Element of DISJOINT_PAIRS A : ( t = a & S5[s,t] ) } = { H5(s9,a) where s9 is Element of DISJOINT_PAIRS A : S5[s9,a] } from FRAENKEL:sch_20(); A6: for s, t being Element of DISJOINT_PAIRS A holds ( S6[s,t] iff S7[s,t] ) by TARSKI:def_1; A7: { H5(s,t) where s, t is Element of DISJOINT_PAIRS A : S6[s,t] } = { H5(s9,t9) where s9, t9 is Element of DISJOINT_PAIRS A : S7[s9,t9] } from FRAENKEL:sch_4(A6); { H4(s) where s is Element of DISJOINT_PAIRS A : ( S3[s] & not H4(s) in DISJOINT_PAIRS A ) } misses DISJOINT_PAIRS A from FRAENKEL:sch_18(); hence (@ v) ^ {a} = {} by A1, A4, A2, A7, A5, XBOOLE_0:def_7; ::_thesis: for b being Element of DISJOINT_PAIRS A st b in (diff u) . v holds b \/ a in DISJOINT_PAIRS A let b be Element of DISJOINT_PAIRS A; ::_thesis: ( b in (diff u) . v implies b \/ a in DISJOINT_PAIRS A ) assume b in (diff u) . v ; ::_thesis: b \/ a in DISJOINT_PAIRS A then A8: b in u \ v by Def11; then not b in { H3(s) where s is Element of DISJOINT_PAIRS A : ( H3(s) in u & S2[s] ) } by XBOOLE_0:def_5; hence b \/ a in DISJOINT_PAIRS A by A8; ::_thesis: verum end; theorem Th23: :: HEYTING1:23 for A being set for u being Element of (NormForm A) holds u "/\" ((pseudo_compl A) . u) = Bottom (NormForm A) proof let A be set ; ::_thesis: for u being Element of (NormForm A) holds u "/\" ((pseudo_compl A) . u) = Bottom (NormForm A) let u be Element of (NormForm A); ::_thesis: u "/\" ((pseudo_compl A) . u) = Bottom (NormForm A) reconsider zero = {} as Element of Normal_forms_on A by NORMFORM:31; A1: @ ((pseudo_compl A) . u) = mi (- (@ u)) by Def8; thus u "/\" ((pseudo_compl A) . u) = H2(A) . (u,((pseudo_compl A) . u)) by LATTICES:def_2 .= mi ((@ u) ^ (mi (- (@ u)))) by A1, NORMFORM:def_12 .= mi ((@ u) ^ (- (@ u))) by NORMFORM:51 .= mi zero by Th21 .= {} by NORMFORM:40, XBOOLE_1:3 .= Bottom (NormForm A) by NORMFORM:57 ; ::_thesis: verum end; theorem Th24: :: HEYTING1:24 for A being set for u, v being Element of (NormForm A) holds u "/\" ((StrongImpl A) . (u,v)) [= v proof let A be set ; ::_thesis: for u, v being Element of (NormForm A) holds u "/\" ((StrongImpl A) . (u,v)) [= v let u, v be Element of (NormForm A); ::_thesis: u "/\" ((StrongImpl A) . (u,v)) [= v now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_st_a_in_u_"/\"_((StrongImpl_A)_._(u,v))_holds_ ex_b_being_Element_of_DISJOINT_PAIRS_A_st_ (_b_in_v_&_b_c=_a_) let a be Element of DISJOINT_PAIRS A; ::_thesis: ( a in u "/\" ((StrongImpl A) . (u,v)) implies ex b being Element of DISJOINT_PAIRS A st ( b in v & b c= a ) ) assume A1: a in u "/\" ((StrongImpl A) . (u,v)) ; ::_thesis: ex b being Element of DISJOINT_PAIRS A st ( b in v & b c= a ) A2: @ ((StrongImpl A) . (u,v)) = mi ((@ u) =>> (@ v)) by Def9; u "/\" ((StrongImpl A) . (u,v)) = H2(A) . (u,((StrongImpl A) . (u,v))) by LATTICES:def_2 .= mi ((@ u) ^ (mi ((@ u) =>> (@ v)))) by A2, NORMFORM:def_12 .= mi ((@ u) ^ ((@ u) =>> (@ v))) by NORMFORM:51 ; then a in (@ u) ^ ((@ u) =>> (@ v)) by A1, NORMFORM:36; hence ex b being Element of DISJOINT_PAIRS A st ( b in v & b c= a ) by Lm6; ::_thesis: verum end; hence u "/\" ((StrongImpl A) . (u,v)) [= v by Lm3; ::_thesis: verum end; theorem Th25: :: HEYTING1:25 for A being set for a being Element of DISJOINT_PAIRS A for u being Element of (NormForm A) st (@ u) ^ {a} = {} holds (Atom A) . a [= (pseudo_compl A) . u proof let A be set ; ::_thesis: for a being Element of DISJOINT_PAIRS A for u being Element of (NormForm A) st (@ u) ^ {a} = {} holds (Atom A) . a [= (pseudo_compl A) . u let a be Element of DISJOINT_PAIRS A; ::_thesis: for u being Element of (NormForm A) st (@ u) ^ {a} = {} holds (Atom A) . a [= (pseudo_compl A) . u let u be Element of (NormForm A); ::_thesis: ( (@ u) ^ {a} = {} implies (Atom A) . a [= (pseudo_compl A) . u ) assume A1: (@ u) ^ {a} = {} ; ::_thesis: (Atom A) . a [= (pseudo_compl A) . u now__::_thesis:_for_c_being_Element_of_DISJOINT_PAIRS_A_st_c_in_(Atom_A)_._a_holds_ ex_e_being_Element_of_DISJOINT_PAIRS_A_st_ (_e_in_(pseudo_compl_A)_._u_&_e_c=_c_) let c be Element of DISJOINT_PAIRS A; ::_thesis: ( c in (Atom A) . a implies ex e being Element of DISJOINT_PAIRS A st ( e in (pseudo_compl A) . u & e c= c ) ) assume c in (Atom A) . a ; ::_thesis: ex e being Element of DISJOINT_PAIRS A st ( e in (pseudo_compl A) . u & e c= c ) then c = a by Th6; then consider b being Element of DISJOINT_PAIRS A such that A2: b in - (@ u) and A3: b c= c by A1, Th19; consider d being Element of DISJOINT_PAIRS A such that A4: d c= b and A5: d in mi (- (@ u)) by A2, NORMFORM:41; take e = d; ::_thesis: ( e in (pseudo_compl A) . u & e c= c ) thus e in (pseudo_compl A) . u by A5, Def8; ::_thesis: e c= c thus e c= c by A3, A4, NORMFORM:2; ::_thesis: verum end; hence (Atom A) . a [= (pseudo_compl A) . u by Lm3; ::_thesis: verum end; theorem Th26: :: HEYTING1:26 for A being set for a being Element of DISJOINT_PAIRS A for u, w being Element of (NormForm A) st ( for b being Element of DISJOINT_PAIRS A st b in u holds b \/ a in DISJOINT_PAIRS A ) & u "/\" ((Atom A) . a) [= w holds (Atom A) . a [= (StrongImpl A) . (u,w) proof let A be set ; ::_thesis: for a being Element of DISJOINT_PAIRS A for u, w being Element of (NormForm A) st ( for b being Element of DISJOINT_PAIRS A st b in u holds b \/ a in DISJOINT_PAIRS A ) & u "/\" ((Atom A) . a) [= w holds (Atom A) . a [= (StrongImpl A) . (u,w) let a be Element of DISJOINT_PAIRS A; ::_thesis: for u, w being Element of (NormForm A) st ( for b being Element of DISJOINT_PAIRS A st b in u holds b \/ a in DISJOINT_PAIRS A ) & u "/\" ((Atom A) . a) [= w holds (Atom A) . a [= (StrongImpl A) . (u,w) let u, w be Element of (NormForm A); ::_thesis: ( ( for b being Element of DISJOINT_PAIRS A st b in u holds b \/ a in DISJOINT_PAIRS A ) & u "/\" ((Atom A) . a) [= w implies (Atom A) . a [= (StrongImpl A) . (u,w) ) assume that A1: for b being Element of DISJOINT_PAIRS A st b in u holds b \/ a in DISJOINT_PAIRS A and A2: u "/\" ((Atom A) . a) [= w ; ::_thesis: (Atom A) . a [= (StrongImpl A) . (u,w) A3: now__::_thesis:_for_c_being_Element_of_DISJOINT_PAIRS_A_st_c_in_u_holds_ ex_e_being_Element_of_DISJOINT_PAIRS_A_st_ (_e_in_w_&_e_c=_c_\/_a_) let c be Element of DISJOINT_PAIRS A; ::_thesis: ( c in u implies ex e being Element of DISJOINT_PAIRS A st ( e in w & e c= c \/ a ) ) assume A4: c in u ; ::_thesis: ex e being Element of DISJOINT_PAIRS A st ( e in w & e c= c \/ a ) then A5: c \/ a is Element of DISJOINT_PAIRS A by A1; a in @ ((Atom A) . a) by Th7; then c \/ a in (@ u) ^ (@ ((Atom A) . a)) by A1, A4, NORMFORM:35; then consider b being Element of DISJOINT_PAIRS A such that A6: b c= c \/ a and A7: b in mi ((@ u) ^ (@ ((Atom A) . a))) by A5, NORMFORM:41; b in H2(A) . (u,((Atom A) . a)) by A7, NORMFORM:def_12; then b in u "/\" ((Atom A) . a) by LATTICES:def_2; then consider d being Element of DISJOINT_PAIRS A such that A8: d in w and A9: d c= b by A2, Lm2; take e = d; ::_thesis: ( e in w & e c= c \/ a ) thus e in w by A8; ::_thesis: e c= c \/ a thus e c= c \/ a by A6, A9, NORMFORM:2; ::_thesis: verum end; now__::_thesis:_for_c_being_Element_of_DISJOINT_PAIRS_A_st_c_in_(Atom_A)_._a_holds_ ex_e_being_Element_of_DISJOINT_PAIRS_A_st_ (_e_in_(StrongImpl_A)_._(u,w)_&_e_c=_c_) let c be Element of DISJOINT_PAIRS A; ::_thesis: ( c in (Atom A) . a implies ex e being Element of DISJOINT_PAIRS A st ( e in (StrongImpl A) . (u,w) & e c= c ) ) assume c in (Atom A) . a ; ::_thesis: ex e being Element of DISJOINT_PAIRS A st ( e in (StrongImpl A) . (u,w) & e c= c ) then c = a by Th6; then consider b being Element of DISJOINT_PAIRS A such that A10: b in (@ u) =>> (@ w) and A11: b c= c by A3, Th20; consider d being Element of DISJOINT_PAIRS A such that A12: d c= b and A13: d in mi ((@ u) =>> (@ w)) by A10, NORMFORM:41; take e = d; ::_thesis: ( e in (StrongImpl A) . (u,w) & e c= c ) thus e in (StrongImpl A) . (u,w) by A13, Def9; ::_thesis: e c= c thus e c= c by A11, A12, NORMFORM:2; ::_thesis: verum end; hence (Atom A) . a [= (StrongImpl A) . (u,w) by Lm3; ::_thesis: verum end; Lm9: now__::_thesis:_for_A_being_set_ for_u,_v_being_Element_of_(NormForm_A)_holds_ (_u_"/\"_H3(u,v)_[=_v_&_(_for_w_being_Element_of_(NormForm_A)_st_u_"/\"_v_[=_w_holds_ v_[=_H3(u,w)_)_) let A be set ; ::_thesis: for u, v being Element of (NormForm A) holds ( u "/\" H3(u,v) [= v & ( for w being Element of (NormForm A) st u "/\" v [= w holds v [= H3(u,w) ) ) let u, v be Element of (NormForm A); ::_thesis: ( u "/\" H3(u,v) [= v & ( for w being Element of (NormForm A) st u "/\" v [= w holds v [= H3(u,w) ) ) deffunc H3( Element of (NormForm A), Element of (NormForm A)) -> Element of the carrier of (NormForm A) = FinJoin ((SUB $1),(H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff $1),$2))))); set Psi = H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v))); A1: now__::_thesis:_for_w_being_Element_of_(NormForm_A)_st_w_in_SUB_u_holds_ (H2(A)_[;]_(u,(H2(A)_.:_((pseudo_compl_A),((StrongImpl_A)_[:]_((diff_u),v))))))_._w_[=_v let w be Element of (NormForm A); ::_thesis: ( w in SUB u implies (H2(A) [;] (u,(H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v)))))) . w [= v ) set u2 = (diff u) . w; set pc = (pseudo_compl A) . w; set si = (StrongImpl A) . (((diff u) . w),v); A2: w "/\" (((pseudo_compl A) . w) "/\" ((StrongImpl A) . (((diff u) . w),v))) = (w "/\" ((pseudo_compl A) . w)) "/\" ((StrongImpl A) . (((diff u) . w),v)) by LATTICES:def_7 .= (Bottom (NormForm A)) "/\" ((StrongImpl A) . (((diff u) . w),v)) by Th23 .= Bottom (NormForm A) ; assume w in SUB u ; ::_thesis: (H2(A) [;] (u,(H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v)))))) . w [= v then A3: w "\/" ((diff u) . w) = u by Lm7; (H2(A) [;] (u,(H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v)))))) . w = H2(A) . (u,((H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v)))) . w)) by FUNCOP_1:53 .= u "/\" ((H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v)))) . w) by LATTICES:def_2 .= u "/\" (H2(A) . (((pseudo_compl A) . w),(((StrongImpl A) [:] ((diff u),v)) . w))) by FUNCOP_1:37 .= u "/\" (((pseudo_compl A) . w) "/\" (((StrongImpl A) [:] ((diff u),v)) . w)) by LATTICES:def_2 .= u "/\" (((pseudo_compl A) . w) "/\" ((StrongImpl A) . (((diff u) . w),v))) by FUNCOP_1:48 .= (w "/\" (((pseudo_compl A) . w) "/\" ((StrongImpl A) . (((diff u) . w),v)))) "\/" (((diff u) . w) "/\" (((pseudo_compl A) . w) "/\" ((StrongImpl A) . (((diff u) . w),v)))) by A3, LATTICES:def_11 .= ((diff u) . w) "/\" (((StrongImpl A) . (((diff u) . w),v)) "/\" ((pseudo_compl A) . w)) by A2, LATTICES:14 .= (((diff u) . w) "/\" ((StrongImpl A) . (((diff u) . w),v))) "/\" ((pseudo_compl A) . w) by LATTICES:def_7 ; then A4: (H2(A) [;] (u,(H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v)))))) . w [= ((diff u) . w) "/\" ((StrongImpl A) . (((diff u) . w),v)) by LATTICES:6; ((diff u) . w) "/\" ((StrongImpl A) . (((diff u) . w),v)) [= v by Th24; hence (H2(A) [;] (u,(H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v)))))) . w [= v by A4, LATTICES:7; ::_thesis: verum end; u "/\" H3(u,v) = FinJoin ((SUB u),(H2(A) [;] (u,(H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v))))))) by LATTICE2:66; hence u "/\" H3(u,v) [= v by A1, LATTICE2:54; ::_thesis: for w being Element of (NormForm A) st u "/\" v [= w holds v [= H3(u,w) let w be Element of (NormForm A); ::_thesis: ( u "/\" v [= w implies v [= H3(u,w) ) assume A5: u "/\" v [= w ; ::_thesis: v [= H3(u,w) A6: v = FinJoin ((@ v),(Atom A)) by Th10; then A7: u "/\" v = FinJoin ((@ v),(H2(A) [;] (u,(Atom A)))) by LATTICE2:66; now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_st_a_in_@_v_holds_ (Atom_A)_._a_[=_H3(u,w) set pf = pseudo_compl A; set sf = (StrongImpl A) [:] ((diff u),w); let a be Element of DISJOINT_PAIRS A; ::_thesis: ( a in @ v implies (Atom A) . a [= H3(u,w) ) assume a in @ v ; ::_thesis: (Atom A) . a [= H3(u,w) then (H2(A) [;] (u,(Atom A))) . a [= w by A7, A5, LATTICE2:31; then H2(A) . (u,((Atom A) . a)) [= w by FUNCOP_1:53; then A8: u "/\" ((Atom A) . a) [= w by LATTICES:def_2; consider v being Element of (NormForm A) such that A9: v in SUB u and A10: (@ v) ^ {a} = {} and A11: for b being Element of DISJOINT_PAIRS A st b in (diff u) . v holds b \/ a in DISJOINT_PAIRS A by Lm8; ((diff u) . v) "/\" ((Atom A) . a) [= u "/\" ((Atom A) . a) by Th22, LATTICES:9; then ((diff u) . v) "/\" ((Atom A) . a) [= w by A8, LATTICES:7; then (Atom A) . a [= (StrongImpl A) . (((diff u) . v),w) by A11, Th26; then A12: (Atom A) . a [= ((StrongImpl A) [:] ((diff u),w)) . v by FUNCOP_1:48; A13: ((pseudo_compl A) . v) "/\" (((StrongImpl A) [:] ((diff u),w)) . v) = H2(A) . (((pseudo_compl A) . v),(((StrongImpl A) [:] ((diff u),w)) . v)) by LATTICES:def_2 .= (H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),w)))) . v by FUNCOP_1:37 ; (Atom A) . a [= (pseudo_compl A) . v by A10, Th25; then (Atom A) . a [= (H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),w)))) . v by A12, A13, FILTER_0:7; hence (Atom A) . a [= H3(u,w) by A9, LATTICE2:29; ::_thesis: verum end; hence v [= H3(u,w) by A6, LATTICE2:54; ::_thesis: verum end; Lm10: for A being set holds NormForm A is implicative proof let A be set ; ::_thesis: NormForm A is implicative let p, q be Element of (NormForm A); :: according to FILTER_0:def_6 ::_thesis: ex b1 being Element of the carrier of (NormForm A) st ( p "/\" b1 [= q & ( for b2 being Element of the carrier of (NormForm A) holds ( not p "/\" b2 [= q or b2 [= b1 ) ) ) take r = FinJoin ((SUB p),(H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff p),q))))); ::_thesis: ( p "/\" r [= q & ( for b1 being Element of the carrier of (NormForm A) holds ( not p "/\" b1 [= q or b1 [= r ) ) ) thus ( p "/\" r [= q & ( for r1 being Element of (NormForm A) st p "/\" r1 [= q holds r1 [= r ) ) by Lm9; ::_thesis: verum end; registration let A be set ; cluster NormForm A -> implicative ; coherence NormForm A is implicative by Lm10; end; theorem Th27: :: HEYTING1:27 for A being set for u, v being Element of (NormForm A) holds u => v = FinJoin ((SUB u),( the L_meet of (NormForm A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v))))) proof let A be set ; ::_thesis: for u, v being Element of (NormForm A) holds u => v = FinJoin ((SUB u),( the L_meet of (NormForm A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v))))) let u, v be Element of (NormForm A); ::_thesis: u => v = FinJoin ((SUB u),( the L_meet of (NormForm A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v))))) deffunc H3( Element of (NormForm A), Element of (NormForm A)) -> Element of the carrier of (NormForm A) = FinJoin ((SUB $1),(H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff $1),$2))))); ( u "/\" H3(u,v) [= v & ( for w being Element of (NormForm A) st u "/\" w [= v holds w [= H3(u,v) ) ) by Lm9; hence u => v = FinJoin ((SUB u),( the L_meet of (NormForm A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v))))) by FILTER_0:def_7; ::_thesis: verum end; theorem :: HEYTING1:28 for A being set holds Top (NormForm A) = {[{},{}]} proof let A be set ; ::_thesis: Top (NormForm A) = {[{},{}]} reconsider O = {[{},{}]} as Element of Normal_forms_on A by Th17; set sd = (StrongImpl A) [:] ((diff (Bottom (NormForm A))),(Bottom (NormForm A))); set F = H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff (Bottom (NormForm A))),(Bottom (NormForm A))))); A1: @ ((pseudo_compl A) . (Bottom (NormForm A))) = mi (- (@ (Bottom (NormForm A)))) by Def8 .= mi O by Th13, NORMFORM:57 .= O by NORMFORM:42 ; A2: Bottom (NormForm A) = {} by NORMFORM:57; then (diff (Bottom (NormForm A))) . (Bottom (NormForm A)) = {} \ {} by Def11 .= Bottom (NormForm A) by NORMFORM:57 ; then A3: @ (((StrongImpl A) [:] ((diff (Bottom (NormForm A))),(Bottom (NormForm A)))) . (Bottom (NormForm A))) = (StrongImpl A) . ((Bottom (NormForm A)),(Bottom (NormForm A))) by FUNCOP_1:48 .= mi ((@ (Bottom (NormForm A))) =>> (@ (Bottom (NormForm A)))) by Def9 .= mi O by A2, Th14 .= O by NORMFORM:42 ; thus Top (NormForm A) = (Bottom (NormForm A)) => (Bottom (NormForm A)) by FILTER_0:28 .= FinJoin ((SUB (Bottom (NormForm A))),(H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff (Bottom (NormForm A))),(Bottom (NormForm A))))))) by Th27 .= H1(A) $$ ((SUB (Bottom (NormForm A))),(H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff (Bottom (NormForm A))),(Bottom (NormForm A))))))) by LATTICE2:def_3 .= (H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff (Bottom (NormForm A))),(Bottom (NormForm A)))))) . (Bottom (NormForm A)) by A2, SETWISEO:17, ZFMISC_1:1 .= H2(A) . (((pseudo_compl A) . (Bottom (NormForm A))),(((StrongImpl A) [:] ((diff (Bottom (NormForm A))),(Bottom (NormForm A)))) . (Bottom (NormForm A)))) by FUNCOP_1:37 .= mi (O ^ O) by A1, A3, NORMFORM:def_12 .= {[{},{}]} by Th3 ; ::_thesis: verum end;