:: by Adam Grabowski

::

:: Received December 31, 1998

:: Copyright (c) 1998-2018 Association of Mizar Users

Lm1: for A, B, C being set st A = B \/ C & A c= B holds

A = B

by XBOOLE_1:7;

theorem :: HEYTING2:3

for V, C being set

for A, B being Element of SubstitutionSet (V,C) st A ^ B = A holds

for a being set st a in A holds

ex b being set st

( b in B & b c= a )

for A, B being Element of SubstitutionSet (V,C) st A ^ B = A holds

for a being set st a in A holds

ex b being set st

( b in B & b c= a )

proof end;

theorem Th4: :: HEYTING2:4

for V, C being set

for A, B being Element of SubstitutionSet (V,C) st mi (A ^ B) = A holds

for a being set st a in A holds

ex b being set st

( b in B & b c= a )

for A, B being Element of SubstitutionSet (V,C) st mi (A ^ B) = A holds

for a being set st a in A holds

ex b being set st

( b in B & b c= a )

proof end;

theorem Th5: :: HEYTING2:5

for V, C being set

for A, B being Element of SubstitutionSet (V,C) st ( for a being set st a in A holds

ex b being set st

( b in B & b c= a ) ) holds

mi (A ^ B) = A

for A, B being Element of SubstitutionSet (V,C) st ( for a being set st a in A holds

ex b being set st

( b in B & b c= a ) ) holds

mi (A ^ B) = A

proof end;

definition

let V be set ;

let C be finite set ;

let A be Element of Fin (PFuncs (V,C));

ex b_{1} being set st

for x being object holds

( x in b_{1} iff ex f being finite Function st

( f in A & x in dom f ) )

for b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} iff ex f being finite Function st

( f in A & x in dom f ) ) ) & ( for x being object holds

( x in b_{2} iff ex f being finite Function st

( f in A & x in dom f ) ) ) holds

b_{1} = b_{2}

end;
let C be finite set ;

let A be Element of Fin (PFuncs (V,C));

func Involved A -> set means :Def1: :: HEYTING2:def 1

for x being object holds

( x in it iff ex f being finite Function st

( f in A & x in dom f ) );

existence for x being object holds

( x in it iff ex f being finite Function st

( f in A & x in dom f ) );

ex b

for x being object holds

( x in b

( f in A & x in dom f ) )

proof end;

uniqueness for b

( x in b

( f in A & x in dom f ) ) ) & ( for x being object holds

( x in b

( f in A & x in dom f ) ) ) holds

b

proof end;

:: deftheorem Def1 defines Involved HEYTING2:def 1 :

for V being set

for C being finite set

for A being Element of Fin (PFuncs (V,C))

for b_{4} being set holds

( b_{4} = Involved A iff for x being object holds

( x in b_{4} iff ex f being finite Function st

( f in A & x in dom f ) ) );

for V being set

for C being finite set

for A being Element of Fin (PFuncs (V,C))

for b

( b

( x in b

( f in A & x in dom f ) ) );

theorem Th6: :: HEYTING2:6

for V being set

for C being finite set

for A being Element of Fin (PFuncs (V,C)) holds Involved A c= V

for C being finite set

for A being Element of Fin (PFuncs (V,C)) holds Involved A c= V

proof end;

Lm2: for V being set

for C being finite set

for A being non empty Element of Fin (PFuncs (V,C)) holds Involved A is finite

proof end;

theorem Th7: :: HEYTING2:7

for V being set

for C being finite set

for A being Element of Fin (PFuncs (V,C)) st A = {} holds

Involved A = {}

for C being finite set

for A being Element of Fin (PFuncs (V,C)) st A = {} holds

Involved A = {}

proof end;

registration

let V be set ;

let C be finite set ;

let A be Element of Fin (PFuncs (V,C));

coherence

Involved A is finite

end;
let C be finite set ;

let A be Element of Fin (PFuncs (V,C));

coherence

Involved A is finite

proof end;

theorem :: HEYTING2:8

definition

let V be set ;

let C be finite set ;

let A be Element of Fin (PFuncs (V,C));

{ f where f is Element of PFuncs ((Involved A),C) : for g being Element of PFuncs (V,C) st g in A holds

not f tolerates g } is Element of Fin (PFuncs (V,C))

end;
let C be finite set ;

let A be Element of Fin (PFuncs (V,C));

func - A -> Element of Fin (PFuncs (V,C)) equals :: HEYTING2:def 2

{ f where f is Element of PFuncs ((Involved A),C) : for g being Element of PFuncs (V,C) st g in A holds

not f tolerates g } ;

coherence { f where f is Element of PFuncs ((Involved A),C) : for g being Element of PFuncs (V,C) st g in A holds

not f tolerates g } ;

{ f where f is Element of PFuncs ((Involved A),C) : for g being Element of PFuncs (V,C) st g in A holds

not f tolerates g } is Element of Fin (PFuncs (V,C))

proof end;

:: deftheorem defines - HEYTING2:def 2 :

for V being set

for C being finite set

for A being Element of Fin (PFuncs (V,C)) holds - A = { f where f is Element of PFuncs ((Involved A),C) : for g being Element of PFuncs (V,C) st g in A holds

not f tolerates g } ;

for V being set

for C being finite set

for A being Element of Fin (PFuncs (V,C)) holds - A = { f where f is Element of PFuncs ((Involved A),C) : for g being Element of PFuncs (V,C) st g in A holds

not f tolerates g } ;

theorem Th9: :: HEYTING2:9

for V being set

for C being finite set

for A being Element of SubstitutionSet (V,C) holds A ^ (- A) = {}

for C being finite set

for A being Element of SubstitutionSet (V,C) holds A ^ (- A) = {}

proof end;

theorem Th10: :: HEYTING2:10

for V being set

for C being finite set

for A being Element of SubstitutionSet (V,C) st A = {} holds

- A = {{}}

for C being finite set

for A being Element of SubstitutionSet (V,C) st A = {} holds

- A = {{}}

proof end;

theorem :: HEYTING2:11

for V being set

for C being finite set

for A being Element of SubstitutionSet (V,C) st A = {{}} holds

- A = {}

for C being finite set

for A being Element of SubstitutionSet (V,C) st A = {{}} holds

- A = {}

proof end;

theorem Th12: :: HEYTING2:12

for V being set

for C being finite set

for A being Element of SubstitutionSet (V,C) holds mi (A ^ (- A)) = Bottom (SubstLatt (V,C))

for C being finite set

for A being Element of SubstitutionSet (V,C) holds mi (A ^ (- A)) = Bottom (SubstLatt (V,C))

proof end;

theorem :: HEYTING2:13

for V being non empty set

for C being non empty finite set

for A being Element of SubstitutionSet (V,C) st A = {} holds

mi (- A) = Top (SubstLatt (V,C))

for C being non empty finite set

for A being Element of SubstitutionSet (V,C) st A = {} holds

mi (- A) = Top (SubstLatt (V,C))

proof end;

theorem Th14: :: HEYTING2:14

for V being set

for C being finite set

for A being Element of SubstitutionSet (V,C)

for a being Element of PFuncs (V,C)

for B being Element of SubstitutionSet (V,C) st B = {a} & A ^ B = {} holds

ex b being finite set st

( b in - A & b c= a )

for C being finite set

for A being Element of SubstitutionSet (V,C)

for a being Element of PFuncs (V,C)

for B being Element of SubstitutionSet (V,C) st B = {a} & A ^ B = {} holds

ex b being finite set st

( b in - A & b c= a )

proof end;

definition

let V be set ;

let C be finite set ;

let A, B be Element of Fin (PFuncs (V,C));

(PFuncs (V,C)) /\ { (union { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A } ) where f is Element of PFuncs (A,B) : dom f = A } is Element of Fin (PFuncs (V,C))

end;
let C be finite set ;

let A, B be Element of Fin (PFuncs (V,C));

func A =>> B -> Element of Fin (PFuncs (V,C)) equals :: HEYTING2:def 3

(PFuncs (V,C)) /\ { (union { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A } ) where f is Element of PFuncs (A,B) : dom f = A } ;

coherence (PFuncs (V,C)) /\ { (union { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A } ) where f is Element of PFuncs (A,B) : dom f = A } ;

(PFuncs (V,C)) /\ { (union { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A } ) where f is Element of PFuncs (A,B) : dom f = A } is Element of Fin (PFuncs (V,C))

proof end;

:: deftheorem defines =>> HEYTING2:def 3 :

for V being set

for C being finite set

for A, B being Element of Fin (PFuncs (V,C)) holds A =>> B = (PFuncs (V,C)) /\ { (union { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A } ) where f is Element of PFuncs (A,B) : dom f = A } ;

for V being set

for C being finite set

for A, B being Element of Fin (PFuncs (V,C)) holds A =>> B = (PFuncs (V,C)) /\ { (union { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A } ) where f is Element of PFuncs (A,B) : dom f = A } ;

theorem Th15: :: HEYTING2:15

for V being set

for C being finite set

for A, B being Element of Fin (PFuncs (V,C))

for s being set st s in A =>> B holds

ex f being PartFunc of A,B st

( s = union { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A } & dom f = A )

for C being finite set

for A, B being Element of Fin (PFuncs (V,C))

for s being set st s in A =>> B holds

ex f being PartFunc of A,B st

( s = union { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A } & dom f = A )

proof end;

Lm3: for a, V being set

for C being finite set

for A being Element of Fin (PFuncs (V,C))

for K being Element of SubstitutionSet (V,C) st a in A ^ (A =>> K) holds

ex b being set st

( b in K & b c= a )

proof end;

theorem :: HEYTING2:16

for V being set

for C being finite set

for A being Element of Fin (PFuncs (V,C)) st A = {} holds

A =>> A = {{}}

for C being finite set

for A being Element of Fin (PFuncs (V,C)) st A = {} holds

A =>> A = {{}}

proof end;

Lm4: for V being set

for C being finite set

for K being Element of SubstitutionSet (V,C)

for X being set st X c= K holds

X in SubstitutionSet (V,C)

proof end;

theorem Th17: :: HEYTING2:17

for V being set

for C being finite set

for u being Element of (SubstLatt (V,C))

for X being set st X c= u holds

X is Element of (SubstLatt (V,C))

for C being finite set

for u being Element of (SubstLatt (V,C))

for X being set st X c= u holds

X is Element of (SubstLatt (V,C))

proof end;

definition

let V be set ;

let C be finite set ;

ex b_{1} being UnOp of the carrier of (SubstLatt (V,C)) st

for u being Element of (SubstLatt (V,C))

for u9 being Element of SubstitutionSet (V,C) st u9 = u holds

b_{1} . u = mi (- u9)

uniqueness

for b_{1}, b_{2} being UnOp of the carrier of (SubstLatt (V,C)) st ( for u being Element of (SubstLatt (V,C))

for u9 being Element of SubstitutionSet (V,C) st u9 = u holds

b_{1} . u = mi (- u9) ) & ( for u being Element of (SubstLatt (V,C))

for u9 being Element of SubstitutionSet (V,C) st u9 = u holds

b_{2} . u = mi (- u9) ) holds

b_{1} = b_{2};

ex b_{1} being BinOp of the carrier of (SubstLatt (V,C)) st

for u, v being Element of (SubstLatt (V,C))

for u9, v9 being Element of SubstitutionSet (V,C) st u9 = u & v9 = v holds

b_{1} . (u,v) = mi (u9 =>> v9)

uniqueness

for b_{1}, b_{2} being BinOp of the carrier of (SubstLatt (V,C)) st ( for u, v being Element of (SubstLatt (V,C))

for u9, v9 being Element of SubstitutionSet (V,C) st u9 = u & v9 = v holds

b_{1} . (u,v) = mi (u9 =>> v9) ) & ( for u, v being Element of (SubstLatt (V,C))

for u9, v9 being Element of SubstitutionSet (V,C) st u9 = u & v9 = v holds

b_{2} . (u,v) = mi (u9 =>> v9) ) holds

b_{1} = b_{2};

coherence

bool u is Element of Fin the carrier of (SubstLatt (V,C))

;

ex b_{1} being UnOp of the carrier of (SubstLatt (V,C)) st

for v being Element of (SubstLatt (V,C)) holds b_{1} . v = u \ v

uniqueness

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

b_{1} = b_{2};

end;
let C be finite set ;

func pseudo_compl (V,C) -> UnOp of the carrier of (SubstLatt (V,C)) means :Def4: :: HEYTING2:def 4

for u being Element of (SubstLatt (V,C))

for u9 being Element of SubstitutionSet (V,C) st u9 = u holds

it . u = mi (- u9);

existence for u being Element of (SubstLatt (V,C))

for u9 being Element of SubstitutionSet (V,C) st u9 = u holds

it . u = mi (- u9);

ex b

for u being Element of (SubstLatt (V,C))

for u9 being Element of SubstitutionSet (V,C) st u9 = u holds

b

proof end;

correctness uniqueness

for b

for u9 being Element of SubstitutionSet (V,C) st u9 = u holds

b

for u9 being Element of SubstitutionSet (V,C) st u9 = u holds

b

b

proof end;

func StrongImpl (V,C) -> BinOp of the carrier of (SubstLatt (V,C)) means :Def5: :: HEYTING2:def 5

for u, v being Element of (SubstLatt (V,C))

for u9, v9 being Element of SubstitutionSet (V,C) st u9 = u & v9 = v holds

it . (u,v) = mi (u9 =>> v9);

existence for u, v being Element of (SubstLatt (V,C))

for u9, v9 being Element of SubstitutionSet (V,C) st u9 = u & v9 = v holds

it . (u,v) = mi (u9 =>> v9);

ex b

for u, v being Element of (SubstLatt (V,C))

for u9, v9 being Element of SubstitutionSet (V,C) st u9 = u & v9 = v holds

b

proof end;

correctness uniqueness

for b

for u9, v9 being Element of SubstitutionSet (V,C) st u9 = u & v9 = v holds

b

for u9, v9 being Element of SubstitutionSet (V,C) st u9 = u & v9 = v holds

b

b

proof end;

let u be Element of (SubstLatt (V,C));coherence

bool u is Element of Fin the carrier of (SubstLatt (V,C))

proof end;

correctness ;

func diff u -> UnOp of the carrier of (SubstLatt (V,C)) means :Def7: :: HEYTING2:def 7

for v being Element of (SubstLatt (V,C)) holds it . v = u \ v;

existence for v being Element of (SubstLatt (V,C)) holds it . v = u \ v;

ex b

for v being Element of (SubstLatt (V,C)) holds b

proof end;

correctness uniqueness

for b

b

proof end;

:: deftheorem Def4 defines pseudo_compl HEYTING2:def 4 :

for V being set

for C being finite set

for b_{3} being UnOp of the carrier of (SubstLatt (V,C)) holds

( b_{3} = pseudo_compl (V,C) iff for u being Element of (SubstLatt (V,C))

for u9 being Element of SubstitutionSet (V,C) st u9 = u holds

b_{3} . u = mi (- u9) );

for V being set

for C being finite set

for b

( b

for u9 being Element of SubstitutionSet (V,C) st u9 = u holds

b

:: deftheorem Def5 defines StrongImpl HEYTING2:def 5 :

for V being set

for C being finite set

for b_{3} being BinOp of the carrier of (SubstLatt (V,C)) holds

( b_{3} = StrongImpl (V,C) iff for u, v being Element of (SubstLatt (V,C))

for u9, v9 being Element of SubstitutionSet (V,C) st u9 = u & v9 = v holds

b_{3} . (u,v) = mi (u9 =>> v9) );

for V being set

for C being finite set

for b

( b

for u9, v9 being Element of SubstitutionSet (V,C) st u9 = u & v9 = v holds

b

:: deftheorem defines SUB HEYTING2:def 6 :

for V being set

for C being finite set

for u being Element of (SubstLatt (V,C)) holds SUB u = bool u;

for V being set

for C being finite set

for u being Element of (SubstLatt (V,C)) holds SUB u = bool u;

:: deftheorem Def7 defines diff HEYTING2:def 7 :

for V being set

for C being finite set

for u being Element of (SubstLatt (V,C))

for b_{4} being UnOp of the carrier of (SubstLatt (V,C)) holds

( b_{4} = diff u iff for v being Element of (SubstLatt (V,C)) holds b_{4} . v = u \ v );

for V being set

for C being finite set

for u being Element of (SubstLatt (V,C))

for b

( b

Lm5: for V being set

for C being finite set

for u, v being Element of (SubstLatt (V,C)) st v in SUB u holds

v "\/" ((diff u) . v) = u

proof end;

Lm6: for V being set

for C being finite set

for u being Element of (SubstLatt (V,C))

for a being Element of PFuncs (V,C)

for K being Element of Fin (PFuncs (V,C)) st K = {a} holds

ex v being Element of SubstitutionSet (V,C) st

( v in SUB u & v ^ K = {} & ( for b being Element of PFuncs (V,C) st b in (diff u) . v holds

b tolerates a ) )

proof end;

definition

let V be set ;

let C be finite set ;

ex b_{1} being Function of (PFuncs (V,C)), the carrier of (SubstLatt (V,C)) st

for a being Element of PFuncs (V,C) holds b_{1} . a = mi {.a.}

uniqueness

for b_{1}, b_{2} being Function of (PFuncs (V,C)), the carrier of (SubstLatt (V,C)) st ( for a being Element of PFuncs (V,C) holds b_{1} . a = mi {.a.} ) & ( for a being Element of PFuncs (V,C) holds b_{2} . a = mi {.a.} ) holds

b_{1} = b_{2};

end;
let C be finite set ;

func Atom (V,C) -> Function of (PFuncs (V,C)), the carrier of (SubstLatt (V,C)) means :Def8: :: HEYTING2:def 8

for a being Element of PFuncs (V,C) holds it . a = mi {.a.};

existence for a being Element of PFuncs (V,C) holds it . a = mi {.a.};

ex b

for a being Element of PFuncs (V,C) holds b

proof end;

correctness uniqueness

for b

b

proof end;

:: deftheorem Def8 defines Atom HEYTING2:def 8 :

for V being set

for C being finite set

for b_{3} being Function of (PFuncs (V,C)), the carrier of (SubstLatt (V,C)) holds

( b_{3} = Atom (V,C) iff for a being Element of PFuncs (V,C) holds b_{3} . a = mi {.a.} );

for V being set

for C being finite set

for b

( b

Lm7: for V being set

for C being finite set

for a being Element of PFuncs (V,C) st a is finite holds

(Atom (V,C)) . a = {a}

proof end;

theorem Th18: :: HEYTING2:18

for V being set

for C being finite set

for K being Element of SubstitutionSet (V,C) holds FinJoin (K,(Atom (V,C))) = FinUnion (K,(singleton (PFuncs (V,C))))

for C being finite set

for K being Element of SubstitutionSet (V,C) holds FinJoin (K,(Atom (V,C))) = FinUnion (K,(singleton (PFuncs (V,C))))

proof end;

theorem Th19: :: HEYTING2:19

for V being set

for C being finite set

for u being Element of SubstitutionSet (V,C) holds u = FinJoin (u,(Atom (V,C)))

for C being finite set

for u being Element of SubstitutionSet (V,C) holds u = FinJoin (u,(Atom (V,C)))

proof end;

Lm8: for V being set

for C being finite set

for u, v being Element of (SubstLatt (V,C)) st ( for a being set st a in u holds

ex b being set st

( b in v & b c= a ) ) holds

u [= v

proof end;

theorem Th20: :: HEYTING2:20

for V being set

for C being finite set

for u, v being Element of (SubstLatt (V,C)) holds (diff u) . v [= u

for C being finite set

for u, v being Element of (SubstLatt (V,C)) holds (diff u) . v [= u

proof end;

theorem Th21: :: HEYTING2:21

for V being set

for C being finite set

for a being Element of PFuncs (V,C) st a is finite holds

for c being set st c in (Atom (V,C)) . a holds

c = a

for C being finite set

for a being Element of PFuncs (V,C) st a is finite holds

for c being set st c in (Atom (V,C)) . a holds

c = a

proof end;

theorem Th22: :: HEYTING2:22

for V being set

for C being finite set

for u being Element of (SubstLatt (V,C))

for K, L being Element of SubstitutionSet (V,C)

for a being Element of PFuncs (V,C) st K = {a} & L = u & L ^ K = {} holds

(Atom (V,C)) . a [= (pseudo_compl (V,C)) . u

for C being finite set

for u being Element of (SubstLatt (V,C))

for K, L being Element of SubstitutionSet (V,C)

for a being Element of PFuncs (V,C) st K = {a} & L = u & L ^ K = {} holds

(Atom (V,C)) . a [= (pseudo_compl (V,C)) . u

proof end;

theorem Th23: :: HEYTING2:23

for V being set

for C being finite set

for a being finite Element of PFuncs (V,C) holds a in (Atom (V,C)) . a

for C being finite set

for a being finite Element of PFuncs (V,C) holds a in (Atom (V,C)) . a

proof end;

Lm9: for V being set

for C being finite set

for u, v being Element of (SubstLatt (V,C)) st u [= v holds

for x being set st x in u holds

ex b being set st

( b in v & b c= x )

proof end;

theorem Th24: :: HEYTING2:24

for V being set

for C being finite set

for a being Element of PFuncs (V,C)

for u, v being Element of SubstitutionSet (V,C) st ( for c being set st c in u holds

ex b being set st

( b in v & b c= c \/ a ) ) holds

ex b being set st

( b in u =>> v & b c= a )

for C being finite set

for a being Element of PFuncs (V,C)

for u, v being Element of SubstitutionSet (V,C) st ( for c being set st c in u holds

ex b being set st

( b in v & b c= c \/ a ) ) holds

ex b being set st

( b in u =>> v & b c= a )

proof end;

theorem Th25: :: HEYTING2:25

for V being set

for C being finite set

for u, v being Element of (SubstLatt (V,C))

for a being finite Element of PFuncs (V,C) st ( for b being Element of PFuncs (V,C) st b in u holds

b tolerates a ) & u "/\" ((Atom (V,C)) . a) [= v holds

(Atom (V,C)) . a [= (StrongImpl (V,C)) . (u,v)

for C being finite set

for u, v being Element of (SubstLatt (V,C))

for a being finite Element of PFuncs (V,C) st ( for b being Element of PFuncs (V,C) st b in u holds

b tolerates a ) & u "/\" ((Atom (V,C)) . a) [= v holds

(Atom (V,C)) . a [= (StrongImpl (V,C)) . (u,v)

proof end;

deffunc H

theorem Th26: :: HEYTING2:26

for V being set

for C being finite set

for u being Element of (SubstLatt (V,C)) holds u "/\" ((pseudo_compl (V,C)) . u) = Bottom (SubstLatt (V,C))

for C being finite set

for u being Element of (SubstLatt (V,C)) holds u "/\" ((pseudo_compl (V,C)) . u) = Bottom (SubstLatt (V,C))

proof end;

theorem Th27: :: HEYTING2:27

for V being set

for C being finite set

for u, v being Element of (SubstLatt (V,C)) holds u "/\" ((StrongImpl (V,C)) . (u,v)) [= v

for C being finite set

for u, v being Element of (SubstLatt (V,C)) holds u "/\" ((StrongImpl (V,C)) . (u,v)) [= v

proof end;

Lm10: now :: thesis: for V being set

for C being finite set

for u, v being Element of (SubstLatt (V,C)) holds

( u "/\" H_{2}(u,v) [= v & ( for w being Element of (SubstLatt (V,C)) st u "/\" v [= w holds

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

for C being finite set

for u, v being Element of (SubstLatt (V,C)) holds

( u "/\" H

v [= H

let V be set ; :: thesis: for C being finite set

for u, v being Element of (SubstLatt (V,C)) holds

( u "/\" H_{2}(u,v) [= v & ( for w being Element of (SubstLatt (V,C)) st u "/\" v [= w holds

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

let C be finite set ; :: thesis: for u, v being Element of (SubstLatt (V,C)) holds

( u "/\" H_{2}(u,v) [= v & ( for w being Element of (SubstLatt (V,C)) st u "/\" v [= w holds

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

let u, v be Element of (SubstLatt (V,C)); :: thesis: ( u "/\" H_{2}(u,v) [= v & ( for w being Element of (SubstLatt (V,C)) st u "/\" v [= w holds

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

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

set Psi = H_{1}(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v)));

reconsider v9 = v as Element of SubstitutionSet (V,C) by SUBSTLAT:def 4;

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

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

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

let w be Element of (SubstLatt (V,C)); :: thesis: ( u "/\" v [= w implies v [= H_{2}(u,w) )

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

A6: v = FinJoin (v9,(Atom (V,C))) by Th19;

then A7: u "/\" v = FinJoin (v9,(H_{1}(V,C) [;] (u,(Atom (V,C)))))
by LATTICE2:66;

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

end;
for u, v being Element of (SubstLatt (V,C)) holds

( u "/\" H

v [= H

let C be finite set ; :: thesis: for u, v being Element of (SubstLatt (V,C)) holds

( u "/\" H

v [= H

let u, v be Element of (SubstLatt (V,C)); :: thesis: ( u "/\" H

v [= H

deffunc H

set Psi = H

reconsider v9 = v as Element of SubstitutionSet (V,C) by SUBSTLAT:def 4;

A1: now :: thesis: for w being Element of (SubstLatt (V,C)) st w in SUB u holds

(H_{1}(V,C) [;] (u,(H_{1}(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v)))))) . w [= v

u "/\" H(H

let w be Element of (SubstLatt (V,C)); :: thesis: ( w in SUB u implies (H_{1}(V,C) [;] (u,(H_{1}(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v)))))) . w [= v )

set u2 = (diff u) . w;

set pc = (pseudo_compl (V,C)) . w;

set si = (StrongImpl (V,C)) . (((diff u) . w),v);

A2: w "/\" (((pseudo_compl (V,C)) . w) "/\" ((StrongImpl (V,C)) . (((diff u) . w),v))) = (w "/\" ((pseudo_compl (V,C)) . w)) "/\" ((StrongImpl (V,C)) . (((diff u) . w),v)) by LATTICES:def 7

.= (Bottom (SubstLatt (V,C))) "/\" ((StrongImpl (V,C)) . (((diff u) . w),v)) by Th26

.= Bottom (SubstLatt (V,C)) ;

assume w in SUB u ; :: thesis: (H_{1}(V,C) [;] (u,(H_{1}(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v)))))) . w [= v

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

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

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

.= u "/\" (H_{1}(V,C) . (((pseudo_compl (V,C)) . w),(((StrongImpl (V,C)) [:] ((diff u),v)) . w)))
by FUNCOP_1:37

.= u "/\" (((pseudo_compl (V,C)) . w) "/\" (((StrongImpl (V,C)) [:] ((diff u),v)) . w)) by LATTICES:def 2

.= u "/\" (((pseudo_compl (V,C)) . w) "/\" ((StrongImpl (V,C)) . (((diff u) . w),v))) by FUNCOP_1:48

.= (w "/\" (((pseudo_compl (V,C)) . w) "/\" ((StrongImpl (V,C)) . (((diff u) . w),v)))) "\/" (((diff u) . w) "/\" (((pseudo_compl (V,C)) . w) "/\" ((StrongImpl (V,C)) . (((diff u) . w),v)))) by A3, LATTICES:def 11

.= ((diff u) . w) "/\" (((StrongImpl (V,C)) . (((diff u) . w),v)) "/\" ((pseudo_compl (V,C)) . w)) by A2

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

then A4: (H_{1}(V,C) [;] (u,(H_{1}(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v)))))) . w [= ((diff u) . w) "/\" ((StrongImpl (V,C)) . (((diff u) . w),v))
by LATTICES:6;

((diff u) . w) "/\" ((StrongImpl (V,C)) . (((diff u) . w),v)) [= v by Th27;

hence (H_{1}(V,C) [;] (u,(H_{1}(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v)))))) . w [= v
by A4, LATTICES:7; :: thesis: verum

end;
set u2 = (diff u) . w;

set pc = (pseudo_compl (V,C)) . w;

set si = (StrongImpl (V,C)) . (((diff u) . w),v);

A2: w "/\" (((pseudo_compl (V,C)) . w) "/\" ((StrongImpl (V,C)) . (((diff u) . w),v))) = (w "/\" ((pseudo_compl (V,C)) . w)) "/\" ((StrongImpl (V,C)) . (((diff u) . w),v)) by LATTICES:def 7

.= (Bottom (SubstLatt (V,C))) "/\" ((StrongImpl (V,C)) . (((diff u) . w),v)) by Th26

.= Bottom (SubstLatt (V,C)) ;

assume w in SUB u ; :: thesis: (H

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

(H

.= u "/\" ((H

.= u "/\" (H

.= u "/\" (((pseudo_compl (V,C)) . w) "/\" (((StrongImpl (V,C)) [:] ((diff u),v)) . w)) by LATTICES:def 2

.= u "/\" (((pseudo_compl (V,C)) . w) "/\" ((StrongImpl (V,C)) . (((diff u) . w),v))) by FUNCOP_1:48

.= (w "/\" (((pseudo_compl (V,C)) . w) "/\" ((StrongImpl (V,C)) . (((diff u) . w),v)))) "\/" (((diff u) . w) "/\" (((pseudo_compl (V,C)) . w) "/\" ((StrongImpl (V,C)) . (((diff u) . w),v)))) by A3, LATTICES:def 11

.= ((diff u) . w) "/\" (((StrongImpl (V,C)) . (((diff u) . w),v)) "/\" ((pseudo_compl (V,C)) . w)) by A2

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

then A4: (H

((diff u) . w) "/\" ((StrongImpl (V,C)) . (((diff u) . w),v)) [= v by Th27;

hence (H

hence u "/\" H

v [= H

let w be Element of (SubstLatt (V,C)); :: thesis: ( u "/\" v [= w implies v [= H

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

A6: v = FinJoin (v9,(Atom (V,C))) by Th19;

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

now :: thesis: for a being Element of PFuncs (V,C) st a in v9 holds

(Atom (V,C)) . a [= H_{2}(u,w)

hence
v [= H(Atom (V,C)) . a [= H

set pf = pseudo_compl (V,C);

set sf = (StrongImpl (V,C)) [:] ((diff u),w);

let a be Element of PFuncs (V,C); :: thesis: ( a in v9 implies (Atom (V,C)) . a [= H_{2}(u,w) )

reconsider SA = {.a.} as Element of Fin (PFuncs (V,C)) ;

consider v being Element of SubstitutionSet (V,C) such that

A8: v in SUB u and

A9: v ^ SA = {} and

A10: for b being Element of PFuncs (V,C) st b in (diff u) . v holds

b tolerates a by Lm6;

assume A11: a in v9 ; :: thesis: (Atom (V,C)) . a [= H_{2}(u,w)

then A12: a is finite by Th1;

reconsider v9 = v as Element of (SubstLatt (V,C)) by SUBSTLAT:def 4;

set dv = (diff u) . v9;

(H_{1}(V,C) [;] (u,(Atom (V,C)))) . a [= w
by A7, A5, A11, LATTICE2:31;

then H_{1}(V,C) . (u,((Atom (V,C)) . a)) [= w
by FUNCOP_1:53;

then A13: u "/\" ((Atom (V,C)) . a) [= w by LATTICES:def 2;

a is finite by A11, Th1;

then reconsider SS = {a} as Element of SubstitutionSet (V,C) by Th2;

v ^ SS = {} by A9;

then A14: (Atom (V,C)) . a [= (pseudo_compl (V,C)) . v9 by Th22;

((diff u) . v9) "/\" ((Atom (V,C)) . a) [= u "/\" ((Atom (V,C)) . a) by Th20, LATTICES:9;

then ((diff u) . v9) "/\" ((Atom (V,C)) . a) [= w by A13, LATTICES:7;

then (Atom (V,C)) . a [= (StrongImpl (V,C)) . (((diff u) . v9),w) by A10, A12, Th25;

then A15: (Atom (V,C)) . a [= ((StrongImpl (V,C)) [:] ((diff u),w)) . v9 by FUNCOP_1:48;

((pseudo_compl (V,C)) . v9) "/\" (((StrongImpl (V,C)) [:] ((diff u),w)) . v9) = H_{1}(V,C) . (((pseudo_compl (V,C)) . v9),(((StrongImpl (V,C)) [:] ((diff u),w)) . v9))
by LATTICES:def 2

.= (H_{1}(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),w)))) . v9
by FUNCOP_1:37
;

then (Atom (V,C)) . a [= (H_{1}(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),w)))) . v9
by A14, A15, FILTER_0:7;

hence (Atom (V,C)) . a [= H_{2}(u,w)
by A8, LATTICE2:29; :: thesis: verum

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

let a be Element of PFuncs (V,C); :: thesis: ( a in v9 implies (Atom (V,C)) . a [= H

reconsider SA = {.a.} as Element of Fin (PFuncs (V,C)) ;

consider v being Element of SubstitutionSet (V,C) such that

A8: v in SUB u and

A9: v ^ SA = {} and

A10: for b being Element of PFuncs (V,C) st b in (diff u) . v holds

b tolerates a by Lm6;

assume A11: a in v9 ; :: thesis: (Atom (V,C)) . a [= H

then A12: a is finite by Th1;

reconsider v9 = v as Element of (SubstLatt (V,C)) by SUBSTLAT:def 4;

set dv = (diff u) . v9;

(H

then H

then A13: u "/\" ((Atom (V,C)) . a) [= w by LATTICES:def 2;

a is finite by A11, Th1;

then reconsider SS = {a} as Element of SubstitutionSet (V,C) by Th2;

v ^ SS = {} by A9;

then A14: (Atom (V,C)) . a [= (pseudo_compl (V,C)) . v9 by Th22;

((diff u) . v9) "/\" ((Atom (V,C)) . a) [= u "/\" ((Atom (V,C)) . a) by Th20, LATTICES:9;

then ((diff u) . v9) "/\" ((Atom (V,C)) . a) [= w by A13, LATTICES:7;

then (Atom (V,C)) . a [= (StrongImpl (V,C)) . (((diff u) . v9),w) by A10, A12, Th25;

then A15: (Atom (V,C)) . a [= ((StrongImpl (V,C)) [:] ((diff u),w)) . v9 by FUNCOP_1:48;

((pseudo_compl (V,C)) . v9) "/\" (((StrongImpl (V,C)) [:] ((diff u),w)) . v9) = H

.= (H

then (Atom (V,C)) . a [= (H

hence (Atom (V,C)) . a [= H

Lm11: for V being set

for C being finite set holds SubstLatt (V,C) is implicative

proof end;

registration
end;

theorem :: HEYTING2:28

for V being set

for C being finite set

for u, v being Element of (SubstLatt (V,C)) holds u => v = FinJoin ((SUB u),( the L_meet of (SubstLatt (V,C)) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v)))))

for C being finite set

for u, v being Element of (SubstLatt (V,C)) holds u => v = FinJoin ((SUB u),( the L_meet of (SubstLatt (V,C)) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v)))))

proof end;