environ
vocabularies HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, NAT_1, RELAT_1, FUNCT_1, XCMPLX_0, PARTFUN1, PBOOLE, FUNCT_4, OPOSET_1, FUNCOP_1, FOMODEL0, MCART_1, ABIAN, HILBERT1, HILBERT2, HILBERT3, XBOOLEAN, QC_LANG1, FUNCT_2, CARD_1, RELAT_2, HILBERT4;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, XXREAL_0, PBOOLE, FUNCT_4, PARTIT_2, XTUPLE_0, HILBERT1, HILBERT2, FUNCT_2, ABIAN, HILBERT3, FUNCT_3, DOMAIN_1, RELAT_2, XCMPLX_0, FUNCOP_1, BINOP_1, FOMODEL0;
definitions TARSKI, FUNCT_4, FUNCOP_1, RELAT_1, HILBERT3, XBOOLE_0, ABIAN, PARTIT_2, BINOP_1, FUNCT_1, FOMODEL0, XTUPLE_0, ZFMISC_1;
theorems TARSKI, FUNCT_1, FUNCT_2, RELAT_1, ZFMISC_1, XBOOLE_1, XBOOLE_0, XTUPLE_0, PARTFUN1, FUNCOP_1, PARTIT_2, ABIAN, HILBERT3, CARD_1, FUNCT_3, GRFUNC_1, FUNCT_4, ORDINAL1, PBOOLE, FOMODEL0;
schemes ALTCAT_2, HILBERT2, FOMODEL0;
registrations FOMODEL0, HILBERT3, FUNCT_1, FUNCT_2, FUNCT_4, ORDINAL1, RELAT_1, RELAT_2, RELSET_1, SUBSET_1, XBOOLE_0, XTUPLE_0, ZFMISC_1, FUNCOP_1, XREAL_0, PARTIT_2, FUNCTOR1, CARD_1;
constructors HIDDEN, SETFAM_1, FUNCT_4, PARTIT_2, BORSUK_7, ABIAN, HILBERT1, HILBERT2, FUNCT_2, MSUALG_3, RELAT_2, HILBERT3, FOMODEL0, NAT_D, FUNCT_3, RELSET_1, BINOP_1;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE;
equalities BINOP_1, RELAT_1, FOMODEL0, XTUPLE_0, FUNCOP_1, FUNCT_4, HILBERT3;
expansions FOMODEL0, RELAT_1, XTUPLE_0;
set sw = (0,1) --> (1,0);
set I = id 1;
Lm9:
for a, X being set holds
( ( a in dom (ChoiceOn X) implies (ChoiceOn X) . a in a ) & dom (ChoiceOn X) = X \ {{}} )
Lm23:
for f being Function st f is involutive holds
f .: (SomePoints f) c= OtherPoints f
Lm24:
for f being Function st f is involutive holds
f .: (OtherPoints f) c= SomePoints f
Lm30:
for f being Function st f is involutive & rng f c= dom f holds
( f .: (OtherPoints f) = SomePoints f & f .: (SomePoints f) = OtherPoints f )
Lm25:
for g being Function st g is involutive & (field g) \ (fixpoints g) <> {} & rng g c= dom g holds
SomePoints g <> {}
Lm26:
for g being Function st (rng g) \ (dom g) = {} & g is involutive & (field g) \ (fixpoints g) <> {} holds
( SomePoints g <> {} & OtherPoints g <> {} )
defpred S1[ set ] means verum;
Lm15:
for v being Function holds
( v tohilbval is Function & v tohilbperm is Function & proj1 (v tohilbval) = NAT & proj1 (v tohilbperm) = NAT )
Lm34:
for x being set
for g being Function st x is Nat holds
( (g tohilbperm) . x = (g . x) tohilb & (g tohilbval) . x = dom ((g . x) tohilb) )
Lm37:
for x being set holds
( x tohilb is symmetric & dom (x tohilb) = rng (x tohilb) )
definition
let V be
SetValuation0;
existence
ex b1 being ManySortedSet of HP-WFF st
( b1 . VERUM = 1 & ( for n being Element of NAT holds b1 . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( b1 . (p '&' q) = [:(b1 . p),(b1 . q):] & b1 . (p => q) = Funcs ((b1 . p),(b1 . q)) ) ) )
uniqueness
for b1, b2 being ManySortedSet of HP-WFF st b1 . VERUM = 1 & ( for n being Element of NAT holds b1 . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( b1 . (p '&' q) = [:(b1 . p),(b1 . q):] & b1 . (p => q) = Funcs ((b1 . p),(b1 . q)) ) ) & b2 . VERUM = 1 & ( for n being Element of NAT holds b2 . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( b2 . (p '&' q) = [:(b2 . p),(b2 . q):] & b2 . (p => q) = Funcs ((b2 . p),(b2 . q)) ) ) holds
b1 = b2
end;
Lm100:
for p being Element of HP-WFF
for v being SetValuation0 holds
( fixpoints (Perm ((v tohilbperm),p)) <> {} iff SetVal0 (v,p) <> {} )
::# It is used to arbitrarily partition the field of a function f
::# into three parts, one of which is made of the fixpoints.
::# We will use this construction in Lm100 for the case of f
::# being a permutation, hence some elementary properties are shown
::# for that case.