:: by Andrzej Trybulec

::

:: Received January 3, 1991

:: Copyright (c) 1991-2019 Association of Mizar Users

:: Preliminaries

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

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

definition

let A be non empty set ;

let B, C be Element of Fin A;

( B c= C iff for a being Element of A st a in B holds

a in C )

end;
let B, C be Element of Fin A;

:: original: c=

redefine pred B c= C means :: HEYTING1:def 1

for a being Element of A st a in B holds

a in C;

compatibility redefine pred B c= C means :: HEYTING1:def 1

for a being Element of A st a in B holds

a in C;

( B c= C iff for a being Element of A st a in B holds

a in C )

proof 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 );

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

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;

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

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

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

hence
{a} is Element of Normal_forms_on A
by NORMFORM:33; :: thesis: verumc = 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;
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

registration

let A be set ;

existence

not for b_{1} being Element of Normal_forms_on A holds b_{1} is empty

end;
existence

not for b

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

definition

let A be set ;

let u be Element of (NormForm A);

coherence

u is Element of Normal_forms_on A by NORMFORM:def 12;

end;
let u be Element of (NormForm A);

coherence

u is Element of Normal_forms_on A by NORMFORM:def 12;

:: deftheorem defines @ HEYTING1:def 3 :

for A being set

for u being Element of (NormForm A) holds @ u = u;

for A being set

for u being Element of (NormForm A) holds @ u = u;

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

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 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)

for u being Element of (NormForm A)

for X being set st X c= u holds

X is Element of (NormForm A)

proof end;

definition

let A be set ;

ex b_{1} being Function of (DISJOINT_PAIRS A), the carrier of (NormForm A) st

for a being Element of DISJOINT_PAIRS A holds b_{1} . a = {a}

for b_{1}, b_{2} being Function of (DISJOINT_PAIRS A), the carrier of (NormForm A) st ( for a being Element of DISJOINT_PAIRS A holds b_{1} . a = {a} ) & ( for a being Element of DISJOINT_PAIRS A holds b_{2} . a = {a} ) holds

b_{1} = b_{2}

end;
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 for a being Element of DISJOINT_PAIRS A holds it . a = {a};

ex b

for a being Element of DISJOINT_PAIRS A holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines Atom HEYTING1:def 4 :

for A being set

for b_{2} being Function of (DISJOINT_PAIRS A), the carrier of (NormForm A) holds

( b_{2} = Atom A iff for a being Element of DISJOINT_PAIRS A holds b_{2} . a = {a} );

for A being set

for b

( b

theorem :: HEYTING1:8

for A being set

for a being Element of DISJOINT_PAIRS A holds (Atom A) . a = (singleton (DISJOINT_PAIRS A)) . a

for a being Element of DISJOINT_PAIRS A holds (Atom A) . a = (singleton (DISJOINT_PAIRS A)) . a

proof 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)))

for K being Element of Normal_forms_on A holds FinJoin (K,(Atom A)) = FinUnion (K,(singleton (DISJOINT_PAIRS A)))

proof 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 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 end;

definition

let A be set ;

ex b_{1} being BinOp of [:(Fin A),(Fin A):] st

for a, b being Element of [:(Fin A),(Fin A):] holds b_{1} . (a,b) = a \ b

uniqueness

for b_{1}, b_{2} being BinOp of [:(Fin A),(Fin A):] st ( for a, b being Element of [:(Fin A),(Fin A):] holds b_{1} . (a,b) = a \ b ) & ( for a, b being Element of [:(Fin A),(Fin A):] holds b_{2} . (a,b) = a \ b ) holds

b_{1} = b_{2};

end;
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 for a, b being Element of [:(Fin A),(Fin A):] holds it . (a,b) = a \ b;

ex b

for a, b being Element of [:(Fin A),(Fin A):] holds b

proof end;

correctness uniqueness

for b

b

proof end;

:: deftheorem Def5 defines pair_diff HEYTING1:def 5 :

for A being set

for b_{2} being BinOp of [:(Fin A),(Fin A):] holds

( b_{2} = pair_diff A iff for a, b being Element of [:(Fin A),(Fin A):] holds b_{2} . (a,b) = a \ b );

for A being set

for b

( b

definition

let A be set ;

let B be Element of Fin (DISJOINT_PAIRS A);

(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)

;

let C be Element of Fin (DISJOINT_PAIRS A);

(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)

;

end;
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) } ;

(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 end;

correctness ;

let C be Element of Fin (DISJOINT_PAIRS A);

func B =>> 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 } ;

(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 end;

correctness ;

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

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

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 ) } ] )

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 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 = {[{},{}]}

for K, L being Element of Normal_forms_on A st K = {} & L = {} holds

K =>> L = {[{},{}]}

proof end;

Lm4: Fin (DISJOINT_PAIRS {}) = {{},{[{},{}]}}

proof 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))))) )

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 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 )

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

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

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 )

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

definition

let A be set ;

ex b_{1} being UnOp of the carrier of (NormForm A) st

for u being Element of (NormForm A) holds b_{1} . u = mi (- (@ u))

uniqueness

for b_{1}, b_{2} being UnOp of the carrier of (NormForm A) st ( for u being Element of (NormForm A) holds b_{1} . u = mi (- (@ u)) ) & ( for u being Element of (NormForm A) holds b_{2} . u = mi (- (@ u)) ) holds

b_{1} = b_{2};

ex b_{1} being BinOp of the carrier of (NormForm A) st

for u, v being Element of (NormForm A) holds b_{1} . (u,v) = mi ((@ u) =>> (@ v))

uniqueness

for b_{1}, b_{2} being BinOp of the carrier of (NormForm A) st ( for u, v being Element of (NormForm A) holds b_{1} . (u,v) = mi ((@ u) =>> (@ v)) ) & ( for u, v being Element of (NormForm A) holds b_{2} . (u,v) = mi ((@ u) =>> (@ v)) ) holds

b_{1} = b_{2};

coherence

bool u is Element of Fin the carrier of (NormForm A)

;

ex b_{1} being UnOp of the carrier of (NormForm A) st

for v being Element of (NormForm A) holds b_{1} . v = u \ v

uniqueness

for b_{1}, b_{2} being UnOp of the carrier of (NormForm A) st ( for v being Element of (NormForm A) holds b_{1} . v = u \ v ) & ( for v being Element of (NormForm A) holds b_{2} . v = u \ v ) holds

b_{1} = b_{2};

end;
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 for u being Element of (NormForm A) holds it . u = mi (- (@ u));

ex b

for u being Element of (NormForm A) holds b

proof end;

correctness uniqueness

for b

b

proof 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 for u, v being Element of (NormForm A) holds it . (u,v) = mi ((@ u) =>> (@ v));

ex b

for u, v being Element of (NormForm A) holds b

proof end;

correctness uniqueness

for b

b

proof end;

let u be Element of (NormForm A);coherence

bool u is Element of Fin the carrier of (NormForm A)

proof 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 for v being Element of (NormForm A) holds it . v = u \ v;

ex b

for v being Element of (NormForm A) holds b

proof end;

correctness uniqueness

for b

b

proof end;

:: deftheorem Def8 defines pseudo_compl HEYTING1:def 8 :

for A being set

for b_{2} being UnOp of the carrier of (NormForm A) holds

( b_{2} = pseudo_compl A iff for u being Element of (NormForm A) holds b_{2} . u = mi (- (@ u)) );

for A being set

for b

( b

:: deftheorem Def9 defines StrongImpl HEYTING1:def 9 :

for A being set

for b_{2} being BinOp of the carrier of (NormForm A) holds

( b_{2} = StrongImpl A iff for u, v being Element of (NormForm A) holds b_{2} . (u,v) = mi ((@ u) =>> (@ v)) );

for A being set

for b

( b

:: deftheorem defines SUB HEYTING1:def 10 :

for A being set

for u being Element of (NormForm A) holds SUB u = bool u;

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 b_{3} being UnOp of the carrier of (NormForm A) holds

( b_{3} = diff u iff for v being Element of (NormForm A) holds b_{3} . v = u \ v );

for A being set

for u being Element of (NormForm A)

for b

( b

deffunc H

deffunc H

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 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 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)

for u being Element of (NormForm A) holds u "/\" ((pseudo_compl A) . u) = Bottom (NormForm A)

proof 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

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 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)

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

Lm9: now :: thesis: for A being set

for u, v being Element of (NormForm A) holds

( u "/\" H_{3}(u,v) [= v & ( for w being Element of (NormForm A) st u "/\" v [= w holds

v [= H_{3}(u,w) ) )

for u, v being Element of (NormForm A) holds

( u "/\" H

v [= H

let A be set ; :: thesis: for u, v being Element of (NormForm A) holds

( u "/\" H_{3}(u,v) [= v & ( for w being Element of (NormForm A) st u "/\" v [= w holds

v [= H_{3}(u,w) ) )

let u, v be Element of (NormForm A); :: thesis: ( u "/\" H_{3}(u,v) [= v & ( for w being Element of (NormForm A) st u "/\" v [= w holds

v [= H_{3}(u,w) ) )

deffunc H_{3}( Element of (NormForm A), Element of (NormForm A)) -> Element of the carrier of (NormForm A) = FinJoin ((SUB $1),(H_{2}(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff $1),$2)))));

set Psi = H_{2}(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v)));

_{3}(u,v) = FinJoin ((SUB u),(H_{2}(A) [;] (u,(H_{2}(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v)))))))
by LATTICE2:66;

hence u "/\" H_{3}(u,v) [= v
by A1, LATTICE2:54; :: thesis: for w being Element of (NormForm A) st u "/\" v [= w holds

v [= H_{3}(u,w)

let w be Element of (NormForm A); :: thesis: ( u "/\" v [= w implies v [= H_{3}(u,w) )

assume A5: u "/\" v [= w ; :: thesis: v [= H_{3}(u,w)

A6: v = FinJoin ((@ v),(Atom A)) by Th10;

then A7: u "/\" v = FinJoin ((@ v),(H_{2}(A) [;] (u,(Atom A))))
by LATTICE2:66;

_{3}(u,w)
by A6, LATTICE2:54; :: thesis: verum

end;
( u "/\" H

v [= H

let u, v be Element of (NormForm A); :: thesis: ( u "/\" H

v [= H

deffunc H

set Psi = H

A1: now :: thesis: for w being Element of (NormForm A) st w in SUB u holds

(H_{2}(A) [;] (u,(H_{2}(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v)))))) . w [= v

u "/\" H(H

let w be Element of (NormForm A); :: thesis: ( w in SUB u implies (H_{2}(A) [;] (u,(H_{2}(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: (H_{2}(A) [;] (u,(H_{2}(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v)))))) . w [= v

then A3: w "\/" ((diff u) . w) = u by Lm7;

(H_{2}(A) [;] (u,(H_{2}(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v)))))) . w =
H_{2}(A) . (u,((H_{2}(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v)))) . w))
by FUNCOP_1:53

.= u "/\" ((H_{2}(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v)))) . w)
by LATTICES:def 2

.= u "/\" (H_{2}(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

.= (((diff u) . w) "/\" ((StrongImpl A) . (((diff u) . w),v))) "/\" ((pseudo_compl A) . w) by LATTICES:def 7 ;

then A4: (H_{2}(A) [;] (u,(H_{2}(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 (H_{2}(A) [;] (u,(H_{2}(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v)))))) . w [= v
by A4, LATTICES:7; :: thesis: verum

end;
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: (H

then A3: w "\/" ((diff u) . w) = u by Lm7;

(H

.= u "/\" ((H

.= u "/\" (H

.= 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

.= (((diff u) . w) "/\" ((StrongImpl A) . (((diff u) . w),v))) "/\" ((pseudo_compl A) . w) by LATTICES:def 7 ;

then A4: (H

((diff u) . w) "/\" ((StrongImpl A) . (((diff u) . w),v)) [= v by Th24;

hence (H

hence u "/\" H

v [= H

let w be Element of (NormForm A); :: thesis: ( u "/\" v [= w implies v [= H

assume A5: u "/\" v [= w ; :: thesis: v [= H

A6: v = FinJoin ((@ v),(Atom A)) by Th10;

then A7: u "/\" v = FinJoin ((@ v),(H

now :: thesis: for a being Element of DISJOINT_PAIRS A st a in @ v holds

(Atom A) . a [= H_{3}(u,w)

hence
v [= H(Atom A) . a [= H

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 [= H_{3}(u,w) )

assume a in @ v ; :: thesis: (Atom A) . a [= H_{3}(u,w)

then (H_{2}(A) [;] (u,(Atom A))) . a [= w
by A7, A5, LATTICE2:31;

then H_{2}(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) = H_{2}(A) . (((pseudo_compl A) . v),(((StrongImpl A) [:] ((diff u),w)) . v))
by LATTICES:def 2

.= (H_{2}(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 [= (H_{2}(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),w)))) . v
by A12, A13, FILTER_0:7;

hence (Atom A) . a [= H_{3}(u,w)
by A9, LATTICE2:29; :: thesis: verum

end;
set sf = (StrongImpl A) [:] ((diff u),w);

let a be Element of DISJOINT_PAIRS A; :: thesis: ( a in @ v implies (Atom A) . a [= H

assume a in @ v ; :: thesis: (Atom A) . a [= H

then (H

then H

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) = H

.= (H

(Atom A) . a [= (pseudo_compl A) . v by A10, Th25;

then (Atom A) . a [= (H

hence (Atom A) . a [= H

Lm10: for A being set holds NormForm A is implicative

proof end;

registration
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)))))

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