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