environ
vocabularies HIDDEN, NUMBERS, ZF_LANG, XBOOLE_0, SUBSET_1, FUNCT_1, ARYTM_3, CARD_1, ZF_MODEL, TARSKI, ORDINAL1, BVFUNC_2, XBOOLEAN, ZFMISC_1, CLASSES2, ZF_REFLE, CARD_3, RELAT_1, ORDINAL2, ZF_LANG1, ZFMODEL1, XXREAL_0, REALSET1, ZF_FUND1, FUNCT_2, ORDINAL4, NAT_1, ZF_FUND2;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, XCMPLX_0, NAT_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, ZF_LANG, ZF_MODEL, ZFMODEL1, ORDINAL2, NUMBERS, CARD_3, ZF_LANG1, CLASSES2, ORDINAL4, ZF_REFLE, ZF_FUND1, XXREAL_0;
definitions TARSKI, ORDINAL1, XBOOLE_0;
theorems TARSKI, NAT_1, ENUMSET1, FUNCT_1, FUNCT_2, ORDINAL1, ORDINAL2, CARD_1, ZF_MODEL, ZFMODEL1, ZFMODEL2, ZF_LANG1, CARD_3, ZF_REFLE, ZFREFLE1, CLASSES2, ZFMISC_1, ZF_FUND1, GRFUNC_1, RELAT_1, CLASSES1, RELSET_1, XBOOLE_0, XBOOLE_1, XREAL_1, FUNCT_7;
schemes ZF_REFLE, NAT_1;
registrations ORDINAL1, RELSET_1, FINSET_1, XREAL_0, CARD_1, CLASSES2, ZF_LANG, ORDINAL4, FUNCT_1, ZF_FUND1, ZF_LANG1;
constructors HIDDEN, PARTFUN1, WELLORD2, DOMAIN_1, XXREAL_0, XREAL_0, NAT_1, CLASSES1, ZFMODEL1, ZF_LANG1, ZF_REFLE, ZF_FUND1, ORDINAL4, RELSET_1, ZF_MODEL, NUMBERS;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities ORDINAL1, XBOOLE_0;
expansions TARSKI, ORDINAL1, XBOOLE_0;
Lm1:
for g being Function
for u1 being set st u1 in Union g holds
ex u2 being set st
( u2 in dom g & u1 in g . u2 )
Lm2:
for H being ZF-formula
for M being non empty set
for v being Function of VAR,M
for x being Variable st not x in variables_in H & {(x. 0),(x. 1),(x. 2)} misses Free H & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
( {(x. 0),(x. 1),(x. 2)} misses Free (H / ((x. 0),x)) & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / ((x. 0),x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / ((x. 0),x)),v) )
Lm3:
for H being ZF-formula
for M being non empty set
for v being Function of VAR,M st M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & not x. 4 in Free H holds
for m being Element of M holds (def_func' (H,v)) .: m = {}
Lm4:
for H being ZF-formula
for x, y being Variable st not y in variables_in H & x <> x. 0 & y <> x. 0 & y <> x. 4 holds
( x. 4 in Free H iff x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) )
Lm5:
for H being ZF-formula
for M being non empty set
for m being Element of M
for v being Function of VAR,M
for i being Element of NAT st x. i in Free H holds
{[i,m]} \/ ((v * decode) | ((code (Free H)) \ {i})) = ((v / ((x. i),m)) * decode) | (code (Free H))