:: Properties of ZF Models
:: by Grzegorz Bancerek
::
:: Received July 5, 1989
:: Copyright (c) 1990-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ZF_LANG, XBOOLE_0, SUBSET_1, FUNCT_1, CARD_1, ORDINAL1, ZF_MODEL,
TARSKI, BVFUNC_2, XBOOLEAN, FUNCT_4, ZFMISC_1, NAT_1, FINSEQ_1, ARYTM_3,
CLASSES2, XXREAL_0, MCART_1, RELAT_1, ZFMODEL1;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, SUBSET_1, XXREAL_0,
ORDINAL1, NUMBERS, RELAT_1, FUNCT_1, FINSEQ_1, ZF_LANG, RELSET_1,
FUNCT_2, FUNCT_7, NAT_1, ZF_MODEL, MCART_1;
constructors ENUMSET1, XXREAL_0, NAT_1, MEMBERED, ZF_MODEL, FUNCT_7, RELSET_1,
XTUPLE_0, NUMBERS;
registrations SUBSET_1, MEMBERED, ZF_LANG, RELAT_1, XXREAL_0, RELSET_1,
XTUPLE_0;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;
begin
reserve x,y,z for Variable,
H for ZF-formula,
E for non empty set,
a,b,c,X,Y,Z for set,
u,v,w for Element of E,
f,g,h,i,j for Function of VAR,E;
theorem :: ZFMODEL1:1
E is epsilon-transitive implies E |= the_axiom_of_extensionality;
theorem :: ZFMODEL1:2
E is epsilon-transitive implies (E |= the_axiom_of_pairs iff for
u,v holds { u,v } in E);
theorem :: ZFMODEL1:3
E is epsilon-transitive implies (E |= the_axiom_of_pairs iff for X,Y
st X in E & Y in E holds { X,Y } in E);
theorem :: ZFMODEL1:4
E is epsilon-transitive implies (E |= the_axiom_of_unions iff for
u holds union u in E);
theorem :: ZFMODEL1:5
E is epsilon-transitive implies (E |= the_axiom_of_unions iff for X st
X in E holds union X in E);
theorem :: ZFMODEL1:6
E is epsilon-transitive implies (E |= the_axiom_of_infinity iff
ex u st u <> {} & for v st v in u ex w st v c< w & w in u);
theorem :: ZFMODEL1:7
E is epsilon-transitive implies (E |= the_axiom_of_infinity iff ex X
st X in E & X <> {} & for Y st Y in X ex Z st Y c< Z & Z in X);
theorem :: ZFMODEL1:8
E is epsilon-transitive implies (E |= the_axiom_of_power_sets iff
for u holds E /\ bool u in E);
theorem :: ZFMODEL1:9
E is epsilon-transitive implies (E |= the_axiom_of_power_sets iff for
X st X in E holds E /\ bool X in E);
theorem :: ZFMODEL1:10
not x in Free H & E,f |= H implies E,f |= All(x,H);
theorem :: ZFMODEL1:11
{ x,y } misses Free H & E,f |= H implies E,f |= All(x,y,H);
theorem :: ZFMODEL1:12
{ x,y,z } misses Free H & E,f |= H implies E,f |= All(x,y,z,H);
definition
let H,E;
let val be Function of VAR,E;
assume that
not x.0 in Free H and
E,val |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0)));
func def_func'(H,val) -> Function of E,E means
:: ZFMODEL1:def 1
for g st for y st g.y
<> val.y holds x.0 = y or x.3 = y or x.4 = y holds E,g |= H iff it.(g.x.3) = g.
x.4;
end;
theorem :: ZFMODEL1:13
for H,f,g st (for x st f.x <> g.x holds not x in Free H) & E,f
|= H holds E,g |= H;
definition
let H,E;
assume that
Free H c= { x.3,x.4 } and
E |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0)));
func def_func(H,E) -> Function of E,E means
:: ZFMODEL1:def 2
for g holds E,g |= H iff it.(g.x.3) = g.x.4;
end;
definition
let F be Function;
let E;
pred F is_definable_in E means
:: ZFMODEL1:def 3
ex H st Free H c= { x.3,x.4 } & E |= All(x.3,
Ex(x.0,All(x.4,H <=> x.4 '=' x.0))) & F = def_func(H,E);
pred F is_parametrically_definable_in E means
:: ZFMODEL1:def 4
ex H,f st { x.0,x.1,x.2
} misses Free H & E,f |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0))) & F =
def_func'(H,f);
end;
theorem :: ZFMODEL1:14
for F being Function st F is_definable_in E holds F
is_parametrically_definable_in E;
theorem :: ZFMODEL1:15
E is epsilon-transitive implies ((for H st { x.0,x.1,x.2 }
misses Free H holds E |= the_axiom_of_substitution_for H) iff for H,f st { x.0,
x.1,x.2 } misses Free H & E,f |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0)))
for u holds def_func'(H,f).:u in E );
theorem :: ZFMODEL1:16
E is epsilon-transitive implies ((for H st { x.0,x.1,x.2 } misses Free
H holds E |= the_axiom_of_substitution_for H) iff for F being Function st F
is_parametrically_definable_in E for X st X in E holds F.:X in E );
theorem :: ZFMODEL1:17
E is being_a_model_of_ZF implies E is epsilon-transitive & (for u,v st
for w holds w in u iff w in v holds u = v) & (for u,v holds { u,v } in E) & (
for u holds union u in E) & (ex u st u <> {} & for v st v in u ex w st v c< w &
w in u) & (for u holds E /\ bool u in E) & for H,f st { x.0,x.1,x.2 } misses
Free H & E,f |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0))) for u holds
def_func'(H,f).:u in E;
theorem :: ZFMODEL1:18
E is epsilon-transitive & (for u,v holds { u,v } in E) & (for u holds
union u in E) & (ex u st u <> {} & for v st v in u ex w st v c< w & w in u) & (
for u holds E /\ bool u in E) & (for H,f st { x.0,x.1,x.2 } misses Free H & E,f
|= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0))) for u holds def_func'(H,f).:u in
E ) implies E is being_a_model_of_ZF;