:: by Adam Grabowski

::

:: Received July 17, 2000

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

Lm1: for A, x being set holds [:A,{x}:] is Function

proof end;

registration
end;

Lm2: 0 = 2 * 0

;

Lm3: 1 = 0 + 1

;

theorem Th3: :: HEYTING3:3

for k being Element of NAT

for X being non empty finite Subset of [:NAT,{k}:] ex n being non zero Element of NAT st X c= [:((Seg n) \/ {0}),{k}:]

for X being non empty finite Subset of [:NAT,{k}:] ex n being non zero Element of NAT st X c= [:((Seg n) \/ {0}),{k}:]

proof end;

theorem Th4: :: HEYTING3:4

for m being Element of NAT

for X being non empty finite Subset of [:NAT,{m}:] holds

not for k being non zero Element of NAT holds [((2 * k) + 1),m] in X

for X being non empty finite Subset of [:NAT,{m}:] holds

not for k being non zero Element of NAT holds [((2 * k) + 1),m] in X

proof end;

theorem :: HEYTING3:5

for m being Element of NAT

for X being finite Subset of [:NAT,{m}:] ex k being Element of NAT st

for l being Element of NAT st l >= k holds

not [l,m] in X

for X being finite Subset of [:NAT,{m}:] ex k being Element of NAT st

for l being Element of NAT st l >= k holds

not [l,m] in X

proof end;

theorem :: HEYTING3:8

for V being set

for C being finite set

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

B =>> A = {}

for C being finite set

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

B =>> A = {}

proof end;

theorem Th9: :: HEYTING3:9

for V, V9, C, C9 being set st V c= V9 & C c= C9 holds

SubstitutionSet (V,C) c= SubstitutionSet (V9,C9)

SubstitutionSet (V,C) c= SubstitutionSet (V9,C9)

proof end;

theorem Th10: :: HEYTING3:10

for V, V9, C, C9 being set

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

for B being Element of Fin (PFuncs (V9,C9)) st V c= V9 & C c= C9 & A = B holds

mi A = mi B

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

for B being Element of Fin (PFuncs (V9,C9)) st V c= V9 & C c= C9 & A = B holds

mi A = mi B

proof end;

theorem :: HEYTING3:11

for V, V9, C, C9 being set st V c= V9 & C c= C9 holds

the L_join of (SubstLatt (V,C)) = the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C))

the L_join of (SubstLatt (V,C)) = the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C))

proof end;

:: deftheorem defines SubstPoset HEYTING3:def 1 :

for V, C being set holds SubstPoset (V,C) = LattPOSet (SubstLatt (V,C));

for V, C being set holds SubstPoset (V,C) = LattPOSet (SubstLatt (V,C));

registration

let V, C be set ;

coherence

( SubstPoset (V,C) is with_suprema & SubstPoset (V,C) is with_infima ) ;

end;
coherence

( SubstPoset (V,C) is with_suprema & SubstPoset (V,C) is with_infima ) ;

registration

let V, C be set ;

coherence

( SubstPoset (V,C) is reflexive & SubstPoset (V,C) is antisymmetric & SubstPoset (V,C) is transitive ) ;

end;
coherence

( SubstPoset (V,C) is reflexive & SubstPoset (V,C) is antisymmetric & SubstPoset (V,C) is transitive ) ;

theorem Th12: :: HEYTING3:12

for V, C being set

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

( a <= b iff for x being set st x in a holds

ex y being set st

( y in b & y c= x ) )

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

( a <= b iff for x being set st x in a holds

ex y being set st

( y in b & y c= x ) )

proof end;

theorem :: HEYTING3:13

for V, V9, C, C9 being set st V c= V9 & C c= C9 holds

SubstPoset (V,C) is full SubRelStr of SubstPoset (V9,C9)

SubstPoset (V,C) is full SubRelStr of SubstPoset (V9,C9)

proof end;

definition

let n, k be Nat;

ex b_{1} being Element of PFuncs (NAT,{k}) st

for x being object holds

( x in b_{1} iff ( ex m being odd Element of NAT st

( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) )

for b_{1}, b_{2} being Element of PFuncs (NAT,{k}) st ( for x being object holds

( x in b_{1} iff ( ex m being odd Element of NAT st

( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) ) ) & ( for x being object holds

( x in b_{2} iff ( ex m being odd Element of NAT st

( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) ) ) holds

b_{1} = b_{2}

end;
func PFArt (n,k) -> Element of PFuncs (NAT,{k}) means :Def2: :: HEYTING3:def 2

for x being object holds

( x in it iff ( ex m being odd Element of NAT st

( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) );

existence for x being object holds

( x in it iff ( ex m being odd Element of NAT st

( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) );

ex b

for x being object holds

( x in b

( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) )

proof end;

uniqueness for b

( x in b

( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) ) ) & ( for x being object holds

( x in b

( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) ) ) holds

b

proof end;

:: deftheorem Def2 defines PFArt HEYTING3:def 2 :

for n, k being Nat

for b_{3} being Element of PFuncs (NAT,{k}) holds

( b_{3} = PFArt (n,k) iff for x being object holds

( x in b_{3} iff ( ex m being odd Element of NAT st

( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) ) );

for n, k being Nat

for b

( b

( x in b

( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) ) );

definition

let n, k be Nat;

ex b_{1} being Element of PFuncs (NAT,{k}) st

for x being object holds

( x in b_{1} iff ex m being odd Element of NAT st

( m <= (2 * n) + 1 & [m,k] = x ) )

for b_{1}, b_{2} being Element of PFuncs (NAT,{k}) st ( for x being object holds

( x in b_{1} iff ex m being odd Element of NAT st

( m <= (2 * n) + 1 & [m,k] = x ) ) ) & ( for x being object holds

( x in b_{2} iff ex m being odd Element of NAT st

( m <= (2 * n) + 1 & [m,k] = x ) ) ) holds

b_{1} = b_{2}

end;
func PFCrt (n,k) -> Element of PFuncs (NAT,{k}) means :Def3: :: HEYTING3:def 3

for x being object holds

( x in it iff ex m being odd Element of NAT st

( m <= (2 * n) + 1 & [m,k] = x ) );

existence for x being object holds

( x in it iff ex m being odd Element of NAT st

( m <= (2 * n) + 1 & [m,k] = x ) );

ex b

for x being object holds

( x in b

( m <= (2 * n) + 1 & [m,k] = x ) )

proof end;

uniqueness for b

( x in b

( m <= (2 * n) + 1 & [m,k] = x ) ) ) & ( for x being object holds

( x in b

( m <= (2 * n) + 1 & [m,k] = x ) ) ) holds

b

proof end;

:: deftheorem Def3 defines PFCrt HEYTING3:def 3 :

for n, k being Nat

for b_{3} being Element of PFuncs (NAT,{k}) holds

( b_{3} = PFCrt (n,k) iff for x being object holds

( x in b_{3} iff ex m being odd Element of NAT st

( m <= (2 * n) + 1 & [m,k] = x ) ) );

for n, k being Nat

for b

( b

( x in b

( m <= (2 * n) + 1 & [m,k] = x ) ) );

theorem :: HEYTING3:14

Lm4: for n being Element of NAT holds (2 * n) + 1 <= (2 * (n + 1)) + 1

proof end;

Lm5: for n, n9 being Element of NAT holds not PFCrt ((n + 1),n9) c= PFCrt (n,n9)

proof end;

Lm6: for n, k being Element of NAT holds PFCrt (n,k) c= PFCrt ((n + 1),k)

proof end;

Lm7: for n, m, k being Element of NAT st n < k holds

PFCrt (n,m) c= PFArt (k,m)

proof end;

definition

let n, k be Nat;

ex b_{1} being Element of Fin (PFuncs (NAT,{k})) st

for x being object holds

( x in b_{1} iff ( ex m being non zero Element of NAT st

( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) )

for b_{1}, b_{2} being Element of Fin (PFuncs (NAT,{k})) st ( for x being object holds

( x in b_{1} iff ( ex m being non zero Element of NAT st

( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) ) ) & ( for x being object holds

( x in b_{2} iff ( ex m being non zero Element of NAT st

( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) ) ) holds

b_{1} = b_{2}

end;
func PFBrt (n,k) -> Element of Fin (PFuncs (NAT,{k})) means :Def4: :: HEYTING3:def 4

for x being object holds

( x in it iff ( ex m being non zero Element of NAT st

( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) );

existence for x being object holds

( x in it iff ( ex m being non zero Element of NAT st

( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) );

ex b

for x being object holds

( x in b

( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) )

proof end;

uniqueness for b

( x in b

( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) ) ) & ( for x being object holds

( x in b

( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) ) ) holds

b

proof end;

:: deftheorem Def4 defines PFBrt HEYTING3:def 4 :

for n, k being Nat

for b_{3} being Element of Fin (PFuncs (NAT,{k})) holds

( b_{3} = PFBrt (n,k) iff for x being object holds

( x in b_{3} iff ( ex m being non zero Element of NAT st

( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) ) );

for n, k being Nat

for b

( b

( x in b

( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) ) );

theorem :: HEYTING3:21

for n, k being Element of NAT

for x being set st x in PFBrt ((n + 1),k) holds

ex y being set st

( y in PFBrt (n,k) & y c= x )

for x being set st x in PFBrt ((n + 1),k) holds

ex y being set st

( y in PFBrt (n,k) & y c= x )

proof end;

Lm8: for n, k being Element of NAT

for x being set st x in PFBrt (n,k) holds

x is finite

proof end;

definition

let k be Element of NAT ;

ex b_{1} being Subset of (SubstPoset (NAT,{k})) st

for x being object holds

( x in b_{1} iff ex n being non zero Element of NAT st x = PFBrt (n,k) )

for b_{1}, b_{2} being Subset of (SubstPoset (NAT,{k})) st ( for x being object holds

( x in b_{1} iff ex n being non zero Element of NAT st x = PFBrt (n,k) ) ) & ( for x being object holds

( x in b_{2} iff ex n being non zero Element of NAT st x = PFBrt (n,k) ) ) holds

b_{1} = b_{2}

end;
func PFDrt k -> Subset of (SubstPoset (NAT,{k})) means :Def5: :: HEYTING3:def 5

for x being object holds

( x in it iff ex n being non zero Element of NAT st x = PFBrt (n,k) );

existence for x being object holds

( x in it iff ex n being non zero Element of NAT st x = PFBrt (n,k) );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def5 defines PFDrt HEYTING3:def 5 :

for k being Element of NAT

for b_{2} being Subset of (SubstPoset (NAT,{k})) holds

( b_{2} = PFDrt k iff for x being object holds

( x in b_{2} iff ex n being non zero Element of NAT st x = PFBrt (n,k) ) );

for k being Element of NAT

for b

( b

( x in b

theorem Th29: :: HEYTING3:29

for k being Element of NAT

for V, X being set

for a being Element of (SubstPoset (V,{k})) st X in a holds

X is finite Subset of [:V,{k}:]

for V, X being set

for a being Element of (SubstPoset (V,{k})) st X in a holds

X is finite Subset of [:V,{k}:]

proof end;

theorem Th30: :: HEYTING3:30

for m being Element of NAT

for a being Element of (SubstPoset (NAT,{m})) st PFDrt m is_>=_than a holds

for X being non empty set st X in a holds

ex n being Element of NAT st

( [n,m] in X & not n is odd )

for a being Element of (SubstPoset (NAT,{m})) st PFDrt m is_>=_than a holds

for X being non empty set st X in a holds

ex n being Element of NAT st

( [n,m] in X & not n is odd )

proof end;

theorem Th31: :: HEYTING3:31

for k being Element of NAT

for a, b being Element of (SubstPoset (NAT,{k}))

for X being Subset of (SubstPoset (NAT,{k})) st a is_<=_than X & b is_<=_than X holds

a "\/" b is_<=_than X

for a, b being Element of (SubstPoset (NAT,{k}))

for X being Subset of (SubstPoset (NAT,{k})) st a is_<=_than X & b is_<=_than X holds

a "\/" b is_<=_than X

proof end;

registration

let k be Element of NAT ;

existence

not for b_{1} being Element of (SubstPoset (NAT,{k})) holds b_{1} is empty

end;
existence

not for b

proof end;

Lm9: for a being non empty set st a <> {{}} & {} in a holds

ex b being set st

( b in a & b <> {} )

proof end;

theorem Th33: :: HEYTING3:33

for k being Element of NAT

for a being non empty Element of (SubstPoset (NAT,{k})) st a <> {{}} holds

ex f being finite Function st

( f in a & f <> {} )

for a being non empty Element of (SubstPoset (NAT,{k})) st a <> {{}} holds

ex f being finite Function st

( f in a & f <> {} )

proof end;

theorem Th34: :: HEYTING3:34

for k being Element of NAT

for a being non empty Element of (SubstPoset (NAT,{k}))

for a9 being Element of Fin (PFuncs (NAT,{k})) st a <> {{}} & a = a9 holds

Involved a9 is non empty finite Subset of NAT

for a being non empty Element of (SubstPoset (NAT,{k}))

for a9 being Element of Fin (PFuncs (NAT,{k})) st a <> {{}} & a = a9 holds

Involved a9 is non empty finite Subset of NAT

proof end;

theorem Th35: :: HEYTING3:35

for k being Element of NAT

for a being Element of (SubstPoset (NAT,{k}))

for a9 being Element of Fin (PFuncs (NAT,{k}))

for B being non empty finite Subset of NAT st B = Involved a9 & a9 = a holds

for X being set st X in a holds

for l being Element of NAT st l > (max B) + 1 holds

not [l,k] in X

for a being Element of (SubstPoset (NAT,{k}))

for a9 being Element of Fin (PFuncs (NAT,{k}))

for B being non empty finite Subset of NAT st B = Involved a9 & a9 = a holds

for X being set st X in a holds

for l being Element of NAT st l > (max B) + 1 holds

not [l,k] in X

proof end;

theorem Th38: :: HEYTING3:38

for k being Element of NAT

for a, b being Element of (SubstPoset (NAT,{k})) st a <= b & a = {{}} holds

b = {{}}

for a, b being Element of (SubstPoset (NAT,{k})) st a <= b & a = {{}} holds

b = {{}}

proof end;

theorem Th39: :: HEYTING3:39

for k being Element of NAT

for a, b being Element of (SubstPoset (NAT,{k})) st a <= b & b = {} holds

a = {}

for a, b being Element of (SubstPoset (NAT,{k})) st a <= b & b = {} holds

a = {}

proof end;

theorem Th40: :: HEYTING3:40

for m being Element of NAT

for a being Element of (SubstPoset (NAT,{m})) st PFDrt m is_>=_than a holds

a <> {{}}

for a being Element of (SubstPoset (NAT,{m})) st PFDrt m is_>=_than a holds

a <> {{}}

proof end;

Lm10: for m being Element of NAT holds not SubstPoset (NAT,{m}) is complete

proof end;

registration
end;