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