begin
scheme
SSubsetUniq{
F1()
-> RelStr ,
P1[
set ] } :
for
A1,
A2 being
Subset of
F1() st ( for
x being
set holds
(
x in A1 iff
P1[
x] ) ) & ( for
x being
set holds
(
x in A2 iff
P1[
x] ) ) holds
A1 = A2
Lm1:
for A, x being set holds [:A,{x}:] is Function
Lm2:
0 = 2 * 0
;
Lm3:
1 = 0 + 1
;
theorem
canceled;
theorem
canceled;
theorem Th3:
theorem
theorem Th5:
theorem Th6:
theorem
theorem
theorem
begin
theorem
canceled;
theorem
theorem Th12:
theorem Th13:
theorem
:: deftheorem defines SubstPoset HEYTING3:def 1 :
for V, C being set holds SubstPoset (V,C) = LattPOSet (SubstLatt (V,C));
theorem Th15:
theorem
definition
let n,
k be
Element of
NAT ;
func PFArt (
n,
k)
-> Element of
PFuncs (
NAT,
{k})
means :
Def2:
for
x being
set 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
ex b1 being Element of PFuncs (NAT,{k}) st
for x being set holds
( x in b1 iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) )
uniqueness
for b1, b2 being Element of PFuncs (NAT,{k}) st ( for x being set holds
( x in b1 iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) ) ) & ( for x being set holds
( x in b2 iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) ) ) holds
b1 = b2
end;
:: deftheorem Def2 defines PFArt HEYTING3:def 2 :
for n, k being Element of NAT
for b3 being Element of PFuncs (NAT,{k}) holds
( b3 = PFArt (n,k) iff for x being set holds
( x in b3 iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) ) );
definition
let n,
k be
Element of
NAT ;
func PFCrt (
n,
k)
-> Element of
PFuncs (
NAT,
{k})
means :
Def3:
for
x being
set holds
(
x in it iff ex
m being
odd Element of
NAT st
(
m <= (2 * n) + 1 &
[m,k] = x ) );
existence
ex b1 being Element of PFuncs (NAT,{k}) st
for x being set holds
( x in b1 iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) )
uniqueness
for b1, b2 being Element of PFuncs (NAT,{k}) st ( for x being set holds
( x in b1 iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) ) ) & ( for x being set holds
( x in b2 iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) ) ) holds
b1 = b2
end;
:: deftheorem Def3 defines PFCrt HEYTING3:def 3 :
for n, k being Element of NAT
for b3 being Element of PFuncs (NAT,{k}) holds
( b3 = PFCrt (n,k) iff for x being set holds
( x in b3 iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) ) );
theorem
theorem Th18:
Lm4:
for n being Element of NAT holds (2 * n) + 1 <= (2 * (n + 1)) + 1
theorem Th19:
Lm5:
for n, n9 being Element of NAT holds not PFCrt ((n + 1),n9) c= PFCrt (n,n9)
theorem Th20:
theorem Th21:
Lm6:
for n, k being Element of NAT holds PFCrt (n,k) c= PFCrt ((n + 1),k)
theorem
Lm7:
for n, m, k being Element of NAT st n < k holds
PFCrt (n,m) c= PFArt (k,m)
theorem
definition
let n,
k be
Element of
NAT ;
func PFBrt (
n,
k)
-> Element of
Fin (PFuncs (NAT,{k})) means :
Def4:
for
x being
set holds
(
x in it iff ( ex
m being non
empty Element of
NAT st
(
m <= n &
x = PFArt (
m,
k) ) or
x = PFCrt (
n,
k) ) );
existence
ex b1 being Element of Fin (PFuncs (NAT,{k})) st
for x being set holds
( x in b1 iff ( ex m being non empty Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) )
uniqueness
for b1, b2 being Element of Fin (PFuncs (NAT,{k})) st ( for x being set holds
( x in b1 iff ( ex m being non empty Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) ) ) & ( for x being set holds
( x in b2 iff ( ex m being non empty Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) ) ) holds
b1 = b2
end;
:: deftheorem Def4 defines PFBrt HEYTING3:def 4 :
for n, k being Element of NAT
for b3 being Element of Fin (PFuncs (NAT,{k})) holds
( b3 = PFBrt (n,k) iff for x being set holds
( x in b3 iff ( ex m being non empty Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) ) );
theorem
theorem
Lm8:
for n, k being Element of NAT
for x being set st x in PFBrt (n,k) holds
x is finite
theorem Th26:
theorem Th27:
begin
theorem Th28:
:: deftheorem Def5 defines PFDrt HEYTING3:def 5 :
for k being Element of NAT
for b2 being Subset of (SubstPoset (NAT,{k})) holds
( b2 = PFDrt k iff for x being set holds
( x in b2 iff ex n being non empty Element of NAT st x = PFBrt (n,k) ) );
theorem
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
Lm9:
for a being non empty set st a <> {{}} & {} in a holds
ex b being set st
( b in a & b <> {} )
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
Lm10:
for m being Element of NAT holds not SubstPoset (NAT,{m}) is complete