Volume 3, 1991

University of Bialystok

Copyright (c) 1991 Association of Mizar Users

### The abstract of the Mizar article:

### Mostowski's Fundamental Operations --- Part II

**by****Grzegorz Bancerek, and****Andrzej Kondracki**- Received February 15, 1991
- MML identifier: ZF_FUND2

- [ Mizar article, MML identifier index ]

environ vocabulary ZF_LANG, FUNCT_1, ARYTM_3, ZF_MODEL, BOOLE, ORDINAL1, CLASSES2, ZF_REFLE, PROB_1, RELAT_1, TARSKI, ORDINAL2, CARD_1, CLASSES1, QC_LANG3, ZFMODEL1, QC_LANG1, ZF_FUND1, FUNCT_2, ORDINAL4, ZF_FUND2; notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, ORDINAL1, ZF_LANG, ZF_MODEL, ZFMODEL1, ORDINAL2, CARD_1, PROB_1, ZF_LANG1, CLASSES1, CLASSES2, ORDINAL4, ZF_REFLE, ZF_FUND1, FINSUB_1; constructors ENUMSET1, NAT_1, ZFMODEL1, ZF_LANG1, CLASSES1, ZF_REFLE, ZF_FUND1, WELLORD2, MEMBERED, XBOOLE_0; clusters SUBSET_1, FUNCT_1, ZF_LANG, ORDINAL1, CLASSES2, RELSET_1, CARD_1, FINSUB_1, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; begin reserve H for ZF-formula, M,E for non empty set, e for Element of E, m,m0,m3,m4 for Element of M, v,v1,v2 for Function of VAR,M, f,f1 for Function of VAR,E, g for Function, u,u1,u2 for set, x,y for Variable, i,n for Nat, X for set; definition let H,M,v; func Section(H,v) -> Subset of M equals :: ZF_FUND2:def 1 { m : M,v/(x.0,m) |= H } if x.0 in Free H otherwise {}; end; definition let M; attr M is predicatively_closed means :: ZF_FUND2:def 2 for H, E, f st E in M holds Section(H,f) in M; end; theorem :: ZF_FUND2:1 E is epsilon-transitive implies Section(All(x.2,x.2 'in' x.0 => x.2 'in' x.1),f/(x.1,e)) = E /\ bool e; reserve W for Universe, w for Element of W, Y for Subclass of W, a,a1,b,c for Ordinal of W, L for DOMAIN-Sequence of W; theorem :: ZF_FUND2:2 (for a,b st a in b holds L.a c= L.b) & (for a holds L.a in Union L & L.a is epsilon-transitive) & Union L is predicatively_closed implies Union L |= the_axiom_of_power_sets; theorem :: ZF_FUND2:3 omega in W & (for a,b st a in b holds L.a c= L.b) & (for a st a <> {} & a is_limit_ordinal holds L.a = Union (L|a)) & (for a holds L.a in Union L & L.a is epsilon-transitive) & Union L is predicatively_closed implies for H st {x.0,x.1,x.2} misses Free H holds Union L |= the_axiom_of_substitution_for H; theorem :: ZF_FUND2:4 Section(H,v)= {m : {[{},m]} \/ (v*decode)|((code Free H)\{{}}) in Diagram(H,M)}; theorem :: ZF_FUND2:5 Y is closed_wrt_A1-A7 & Y is epsilon-transitive implies Y is predicatively_closed; theorem :: ZF_FUND2:6 (omega in W) & (for a,b st a in b holds L.a c= L.b) & (for a st a <> {} & a is_limit_ordinal holds L.a = Union (L|a)) & (for a holds L.a in Union L & L.a is epsilon-transitive) & (Union L is closed_wrt_A1-A7) implies Union L is_a_model_of_ZF;

Back to top