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