environ
vocabularies HIDDEN, CLASSES2, SUBSET_1, ZF_REFLE, ORDINAL1, FINSET_1, FUNCT_1, XBOOLE_0, ZF_LANG, NUMBERS, VALUED_1, RELAT_1, TARSKI, ZFMISC_1, MCART_1, CARD_1, XXREAL_0, NAT_1, ARYTM_3, ZF_MODEL, FUNCT_2, ORDINAL4, FUNCOP_1, XBOOLEAN, BVFUNC_2, ZF_FUND1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, DOMAIN_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, ORDINAL4, CARD_1, FINSET_1, RELAT_1, CLASSES2, ZF_REFLE, ZF_LANG, ZF_MODEL, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, MCART_1, FUNCOP_1, XXREAL_0;
definitions TARSKI, XBOOLE_0, RELAT_1;
theorems TARSKI, ORDINAL1, ORDINAL3, CARD_1, CLASSES2, ZFMISC_1, ZF_LANG, ZF_LANG1, ZF_MODEL, ENUMSET1, FUNCT_1, FUNCT_2, FUNCT_5, RELAT_1, FINSET_1, GRFUNC_1, NAT_1, FUNCOP_1, WELLORD2, CLASSES1, RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, XTUPLE_0;
schemes FUNCT_1, FUNCT_2, ORDINAL1, FINSET_1, ZF_LANG1, BINOP_2, XBOOLE_0;
registrations FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, FINSET_1, XREAL_0, CARD_1, CLASSES2, ZF_LANG, ZF_LANG1, RELAT_1, XTUPLE_0;
constructors HIDDEN, PARTFUN1, WELLORD2, DOMAIN_1, FUNCOP_1, XXREAL_0, XREAL_0, NAT_1, CLASSES1, ORDINAL4, ZF_MODEL, RELSET_1, NUMBERS;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE;
equalities TARSKI, XBOOLE_0, ORDINAL1, ORDINAL4;
expansions TARSKI, XBOOLE_0;
Lm1:
( dom decode = omega & rng decode = VAR & decode is one-to-one & decode " is one-to-one & dom (decode ") = VAR & rng (decode ") = omega )
Lm2:
for A being Element of omega holds A = x". (x. (card A))
by Def2;
Lm3:
for fs being finite Subset of omega
for E being non empty set
for f being Function of VAR,E holds
( dom ((f * decode) | fs) = fs & rng ((f * decode) | fs) c= E & (f * decode) | fs in Funcs (fs,E) & dom (f * decode) = omega )
Lm4:
for E being non empty set
for f being Function of VAR,E
for v1 being Element of VAR holds
( decode . (x". v1) = v1 & (decode ") . v1 = x". v1 & (f * decode) . (x". v1) = f . v1 )
Lm5:
for p being set
for A being finite Subset of VAR holds
( p in code A iff ex v1 being Element of VAR st
( v1 in A & p = x". v1 ) )
Lm6:
for v1 being Element of VAR holds code {v1} = {(x". v1)}
Lm7:
for v1, v2 being Element of VAR holds code {v1,v2} = {(x". v1),(x". v2)}
Lm8:
for A being finite Subset of VAR holds A, code A are_equipotent
Lm9:
for E being non empty set
for f being Function of VAR,E
for v1 being Element of VAR
for H being ZF-formula st v1 in Free H holds
((f * decode) | (code (Free H))) . (x". v1) = f . v1
Lm10:
for E being non empty set
for H being ZF-formula
for f, g being Function of VAR,E st (f * decode) | (code (Free H)) = (g * decode) | (code (Free H)) & f in St (H,E) holds
g in St (H,E)
Lm11:
for p being set
for fs being finite Subset of omega
for E being non empty set st p in Funcs (fs,E) holds
ex f being Function of VAR,E st p = (f * decode) | fs
Lm12:
for V being Universe
for X being Subclass of V
for n being Element of omega st X is closed_wrt_A1-A7 holds
n in X
by Th7, TARSKI:def 3;
Lm13:
for V being Universe
for X being Subclass of V st X is closed_wrt_A1-A7 holds
( 0-element_of V in X & 1-element_of V in X )
Lm14:
for o, p, q being set holds {[o,p],[p,p]} (#) {[p,q]} = {[o,q],[p,q]}
Lm15:
for o, p, q, r, s, t being set st p <> r holds
{[o,p],[q,r]} (#) {[p,s],[r,t]} = {[o,s],[q,t]}
Lm16:
for o, q being set
for g being Function holds
( dom g = {o,q} iff g = {[o,(g . o)],[q,(g . q)]} )
theorem
for
o,
p,
q,
r,
s,
t being
set st
p <> r holds
{[o,p],[q,r]} (#) {[p,s],[r,t]} = {[o,s],[q,t]} by Lm15;