The abstract of the Mizar article:

A Model of ZF Set Theory Language

by

Grzegorz Bancerek

Received April 4, 1989

MML identifier: ZF_LANG

[ Mizar article, MML identifier index ]

environ

 vocabulary FINSEQ_1, FUNCT_1, BOOLE, RELAT_1, ARYTM_1, ZF_LANG;
 notation TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XREAL_0, RELAT_1, FUNCT_1,
      NAT_1, NUMBERS, FINSEQ_1;
 constructors NAT_1, FINSEQ_1, XREAL_0, MEMBERED, XBOOLE_0;
 clusters RELSET_1, XREAL_0, FINSEQ_1, SUBSET_1, ARYTM_3, MEMBERED, ZFMISC_1,
      XBOOLE_0, NUMBERS, ORDINAL2;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;


begin

 reserve k,m,n for Nat,
         a,X,Y for set,
         D,D1,D2 for non empty set;

 reserve p,q for FinSequence of NAT;

::
::       The Construction of ZF Set Theory Language
::

:: The set and the mode of ZF-language variables

 definition
  func VAR -> Subset of NAT equals
:: ZF_LANG:def 1
   { k : 5 <= k };
 end;

 definition
  cluster VAR -> non empty;
 end;

 definition mode Variable is Element of VAR;
 end;

 definition let n;
  func x.n -> Variable equals
:: ZF_LANG:def 2
     5 + n;
 end;

 reserve x,y,z,t for Variable;

:: The operations to make ZF-formulae

 definition let x;
 redefine func <*x*> -> FinSequence of NAT;
 end;

 definition let x,y;
  func x '=' y -> FinSequence of NAT equals
:: ZF_LANG:def 3
   <*0*>^<*x*>^<*y*>;
  func x 'in' y -> FinSequence of NAT equals
:: ZF_LANG:def 4
   <*1*>^<*x*>^<*y*>;
 end;

canceled 5;

theorem :: ZF_LANG:6
    x '=' y = z '=' t implies x = z & y = t;

theorem :: ZF_LANG:7
    x 'in' y = z 'in' t implies x = z & y = t;

 definition let p;
  func 'not' p -> FinSequence of NAT equals
:: ZF_LANG:def 5
   <*2*>^p;
  let q;
  func p '&' q -> FinSequence of NAT equals
:: ZF_LANG:def 6
   <*3*>^p^q;
 end;

canceled 2;

theorem :: ZF_LANG:10
  'not' p = 'not' q implies p = q;

 definition let x,p;
  func All(x,p)-> FinSequence of NAT equals
:: ZF_LANG:def 7
   <*4*>^<*x*>^p;
 end;

canceled;

theorem :: ZF_LANG:12
  All(x,p) = All(y,q) implies x = y & p = q;

:: The set of all well formed formulae of ZF-language

 definition
  func WFF -> non empty set means
:: ZF_LANG:def 8
 (for a st a in it holds a is FinSequence of NAT ) &
       (for x,y holds x '=' y in it & x 'in' y in it ) &
        (for p st p in it holds 'not' p in it ) &
         (for p,q st p in it & q in it holds p '&' q in it ) &
          (for x,p st p in it holds All(x,p) in it ) &
      for D st
       (for a st a in D holds a is FinSequence of NAT ) &
        (for x,y holds x '=' y in D & x 'in' y in D ) &
         (for p st p in D holds 'not' p in D ) &
          (for p,q st p in D & q in D holds p '&' q in D ) &
           (for x,p st p in D holds All(x,p) in D )
       holds it c= D;
 end;

 definition let IT be FinSequence of NAT;
  attr IT is ZF-formula-like means
:: ZF_LANG:def 9
  IT is Element of WFF;
 end;

 definition
  cluster ZF-formula-like FinSequence of NAT;
 end;

definition
  mode ZF-formula is ZF-formula-like FinSequence of NAT;
end;

canceled;

theorem :: ZF_LANG:14
    a is ZF-formula iff a in WFF;

 reserve F,F1,G,G1,H,H1 for ZF-formula;

 definition let x,y;
  cluster x '=' y -> ZF-formula-like;
  cluster x 'in' y -> ZF-formula-like;
 end;

 definition let H;
  cluster 'not' H -> ZF-formula-like;
  let G;
  cluster H '&' G -> ZF-formula-like;
 end;

 definition let x,H;
  cluster All(x,H) -> ZF-formula-like;
 end;

::
::                   The Properties of ZF-formulae
::

 definition let H;
  attr H is being_equality means
:: ZF_LANG:def 10
  ex x,y st H = x '=' y;
  synonym H is_equality;
  attr H is being_membership means
:: ZF_LANG:def 11
  ex x,y st H = x 'in' y;
  synonym H is_membership;
  attr H is negative means
:: ZF_LANG:def 12
  ex H1 st H = 'not' H1;
  attr H is conjunctive means
:: ZF_LANG:def 13
  ex F,G st H = F '&' G;
  attr H is universal means
:: ZF_LANG:def 14
  ex x,H1 st H = All(x,H1);
 end;

canceled;

theorem :: ZF_LANG:16
    (H is_equality iff ex x,y st H = x '=' y) &
   (H is_membership iff ex x,y st H = x 'in' y) &
    (H is negative iff ex H1 st H = 'not' H1) &
     (H is conjunctive iff ex F,G st H = F '&' G) &
      (H is universal iff ex x,H1 st H = All(x,H1) );

 definition let H;
  attr H is atomic means
:: ZF_LANG:def 15
  H is_equality or H is_membership;
 end;

 definition let F,G;
  func F 'or' G -> ZF-formula equals
:: ZF_LANG:def 16
   'not'('not' F '&' 'not' G);

  func F => G -> ZF-formula equals
:: ZF_LANG:def 17
   'not' (F '&' 'not' G);

 end;

 definition let F,G;
  func F <=> G -> ZF-formula equals
:: ZF_LANG:def 18
   (F => G) '&' (G => F);

 end;

 definition let x,H;
  func Ex(x,H) -> ZF-formula equals
:: ZF_LANG:def 19
   'not' All(x,'not' H);

 end;

 definition let H;
  attr H is disjunctive means
:: ZF_LANG:def 20
  ex F,G st H = F 'or' G;
  attr H is conditional means
:: ZF_LANG:def 21
  ex F,G st H = F => G;
  attr H is biconditional means
:: ZF_LANG:def 22
  ex F,G st H = F <=> G;
  attr H is existential means
:: ZF_LANG:def 23
  ex x,H1 st H = Ex(x,H1);
 end;

canceled 5;

theorem :: ZF_LANG:22
    (H is disjunctive iff ex F,G st H = F 'or' G) &
   (H is conditional iff ex F,G st H = F => G) &
    (H is biconditional iff ex F,G st H = F <=> G) &
     (H is existential iff ex x,H1 st H = Ex(x,H1) );

 definition let x,y,H;
  func All(x,y,H) -> ZF-formula equals
:: ZF_LANG:def 24
   All(x,All(y,H));

  func Ex(x,y,H) -> ZF-formula equals
:: ZF_LANG:def 25
   Ex(x,Ex(y,H));

 end;

theorem :: ZF_LANG:23
   All(x,y,H) = All(x,All(y,H)) & Ex(x,y,H) = Ex(x,Ex(y,H));

 definition let x,y,z,H;
  func All(x,y,z,H) -> ZF-formula equals
:: ZF_LANG:def 26
   All(x,All(y,z,H));

  func Ex(x,y,z,H) -> ZF-formula equals
:: ZF_LANG:def 27
   Ex(x,Ex(y,z,H));

 end;

theorem :: ZF_LANG:24
   All(x,y,z,H) = All(x,All(y,z,H)) & Ex(x,y,z,H) = Ex(x,Ex(y,z,H));

theorem :: ZF_LANG:25
  H is_equality or H is_membership or H is negative or H is conjunctive or
       H is universal;

theorem :: ZF_LANG:26
  H is atomic or H is negative or H is conjunctive or
   H is universal;

theorem :: ZF_LANG:27
  H is atomic implies len H = 3;

theorem :: ZF_LANG:28
  H is atomic or ex H1 st len H1 + 1 <= len H;

theorem :: ZF_LANG:29
  3 <= len H;

theorem :: ZF_LANG:30
    len H = 3 implies H is atomic;

theorem :: ZF_LANG:31
  for x,y holds (x '=' y).1 = 0 & (x 'in' y ).1 = 1;

theorem :: ZF_LANG:32
  for H holds ('not' H).1 = 2;

theorem :: ZF_LANG:33
  for F,G holds (F '&' G).1 = 3;

theorem :: ZF_LANG:34
  for x,H holds All(x,H).1 = 4;

theorem :: ZF_LANG:35
  H is_equality implies H.1 = 0;

theorem :: ZF_LANG:36
  H is_membership implies H.1 = 1;

theorem :: ZF_LANG:37
  H is negative implies H.1 = 2;

theorem :: ZF_LANG:38
  H is conjunctive implies H.1 = 3;

theorem :: ZF_LANG:39
  H is universal implies H.1 = 4;

theorem :: ZF_LANG:40
  H is_equality & H.1 = 0 or H is_membership & H.1 = 1 or
  H is negative & H.1 = 2 or H is conjunctive & H.1 = 3 or
   H is universal & H.1 = 4;

theorem :: ZF_LANG:41
    H.1 = 0 implies H is_equality;

theorem :: ZF_LANG:42
    H.1 = 1 implies H is_membership;

theorem :: ZF_LANG:43
   H.1 = 2 implies H is negative;

theorem :: ZF_LANG:44
   H.1 = 3 implies H is conjunctive;

theorem :: ZF_LANG:45
   H.1 = 4 implies H is universal;

 reserve sq,sq' for FinSequence;

theorem :: ZF_LANG:46
  H = F^sq implies H = F;

theorem :: ZF_LANG:47
  H '&' G = H1 '&' G1 implies H = H1 & G = G1;

theorem :: ZF_LANG:48
  F 'or' G = F1 'or' G1 implies F = F1 & G = G1;

theorem :: ZF_LANG:49
  F => G = F1 => G1 implies F = F1 & G = G1;

theorem :: ZF_LANG:50
  F <=> G = F1 <=> G1 implies F = F1 & G = G1;

theorem :: ZF_LANG:51
  Ex(x,H) = Ex(y,G) implies x = y & H = G;


::
::             The Select Function of ZF-fomrulae
::

 definition let H;
  assume
 H is atomic;
  func Var1 H -> Variable equals
:: ZF_LANG:def 28
   H.2;
  func Var2 H -> Variable equals
:: ZF_LANG:def 29
   H.3;
 end;

theorem :: ZF_LANG:52
    H is atomic implies Var1 H = H.2 & Var2 H = H.3;

theorem :: ZF_LANG:53
  H is_equality implies H = (Var1 H) '=' Var2 H;

theorem :: ZF_LANG:54
  H is_membership implies H = (Var1 H) 'in' Var2 H;

 definition let H;
  assume
 H is negative;
  func the_argument_of H -> ZF-formula means
:: ZF_LANG:def 30
  'not' it = H;
 end;

 definition let H;
  assume
 H is conjunctive or H is disjunctive;
  func the_left_argument_of H -> ZF-formula means
:: ZF_LANG:def 31
  ex H1 st it '&' H1 = H if H is conjunctive
     otherwise ex H1 st it 'or' H1 = H;
  func the_right_argument_of H -> ZF-formula means
:: ZF_LANG:def 32
  ex H1 st H1 '&' it = H if H is conjunctive
     otherwise ex H1 st H1 'or' it = H;
 end;

canceled;

theorem :: ZF_LANG:56
    H is conjunctive implies
   (F = the_left_argument_of H iff ex G st F '&' G = H) &
    (F = the_right_argument_of H iff ex G st G '&' F = H);

theorem :: ZF_LANG:57
  H is disjunctive implies
   (F = the_left_argument_of H iff ex G st F 'or' G = H) &
    (F = the_right_argument_of H iff ex G st G 'or' F = H);

theorem :: ZF_LANG:58
  H is conjunctive implies
   H = (the_left_argument_of H) '&' the_right_argument_of H;

theorem :: ZF_LANG:59
    H is disjunctive implies
   H = (the_left_argument_of H) 'or' the_right_argument_of H;

 definition let H;
  assume
 H is universal or H is existential;
  func bound_in H -> Variable means
:: ZF_LANG:def 33
  ex H1 st All(it,H1) = H if H is universal
     otherwise ex H1 st Ex(it,H1) = H;
  func the_scope_of H -> ZF-formula means
:: ZF_LANG:def 34
  ex x st All(x,it) = H if H is universal
     otherwise ex x st Ex(x,it) = H;
 end;

theorem :: ZF_LANG:60
    H is universal implies
   (x = bound_in H iff ex H1 st All(x,H1) = H) &
    (H1 = the_scope_of H iff ex x st All(x,H1) = H);

theorem :: ZF_LANG:61
  H is existential implies
   (x = bound_in H iff ex H1 st Ex(x,H1) = H) &
    (H1 = the_scope_of H iff ex x st Ex(x,H1) = H);

theorem :: ZF_LANG:62
  H is universal implies H = All(bound_in H,the_scope_of H);

theorem :: ZF_LANG:63
    H is existential implies H = Ex(bound_in H,the_scope_of H);

 definition let H;
  assume
 H is conditional;
  func the_antecedent_of H -> ZF-formula means
:: ZF_LANG:def 35
  ex H1 st H = it => H1;
  func the_consequent_of H -> ZF-formula means
:: ZF_LANG:def 36
  ex H1 st H = H1 => it;
 end;

theorem :: ZF_LANG:64
    H is conditional implies
   (F = the_antecedent_of H iff ex G st H = F => G) &
    (F = the_consequent_of H iff ex G st H = G => F);

theorem :: ZF_LANG:65
    H is conditional implies
   H = (the_antecedent_of H) => the_consequent_of H;

 definition let H;
  assume
 H is biconditional;
  func the_left_side_of H -> ZF-formula means
:: ZF_LANG:def 37
  ex H1 st H = it <=> H1;
  func the_right_side_of H -> ZF-formula means
:: ZF_LANG:def 38
  ex H1 st H = H1 <=> it;
 end;

theorem :: ZF_LANG:66
    H is biconditional implies
   (F = the_left_side_of H iff ex G st H = F <=> G) &
    (F = the_right_side_of H iff ex G st H = G <=> F);

theorem :: ZF_LANG:67
    H is biconditional implies
   H = (the_left_side_of H) <=> the_right_side_of H;

::
::         The Immediate Constituents of ZF-formulae
::

 definition let H,F;
  pred H is_immediate_constituent_of F means
:: ZF_LANG:def 39
  F = 'not' H or ( ex H1 st F = H '&' H1 or F = H1 '&' H ) or
      ex x st F = All(x,H);
 end;

canceled;

theorem :: ZF_LANG:69
  not H is_immediate_constituent_of x '=' y;

theorem :: ZF_LANG:70
  not H is_immediate_constituent_of x 'in' y;

theorem :: ZF_LANG:71
  F is_immediate_constituent_of 'not' H iff F = H;

theorem :: ZF_LANG:72
  F is_immediate_constituent_of G '&' H iff F = G or F = H;

theorem :: ZF_LANG:73
  F is_immediate_constituent_of All(x,H) iff F = H;

theorem :: ZF_LANG:74
    H is atomic implies not F is_immediate_constituent_of H;

theorem :: ZF_LANG:75
  H is negative implies
   (F is_immediate_constituent_of H iff F = the_argument_of H);

theorem :: ZF_LANG:76
  H is conjunctive implies
   (F is_immediate_constituent_of H iff
     F = the_left_argument_of H or F = the_right_argument_of H);

theorem :: ZF_LANG:77
  H is universal implies
   (F is_immediate_constituent_of H iff F = the_scope_of H);

::
::    The Subformulae and The Proper Subformulae of ZF-formulae
::

 reserve L,L' for FinSequence;

 definition let H,F;
  pred H is_subformula_of F means
:: ZF_LANG:def 40
  ex n,L st 1 <= n & len L = n & L.1 = H & L.n = F &
        for k st 1 <= k & k < n
         ex H1,F1 st L.k = H1 & L.(k + 1) = F1 &
          H1 is_immediate_constituent_of F1;
 end;

canceled;

theorem :: ZF_LANG:79
  H is_subformula_of H;

 definition let H,F;
  pred H is_proper_subformula_of F means
:: ZF_LANG:def 41
  H is_subformula_of F & H <> F;
 end;

canceled;

theorem :: ZF_LANG:81
  H is_immediate_constituent_of F implies len H < len F;

theorem :: ZF_LANG:82
  H is_immediate_constituent_of F implies H is_proper_subformula_of F;

theorem :: ZF_LANG:83
  H is_proper_subformula_of F implies len H < len F;

theorem :: ZF_LANG:84
  H is_proper_subformula_of F implies
   ex G st G is_immediate_constituent_of F;

 reserve j,j1 for Nat;

theorem :: ZF_LANG:85
  F is_proper_subformula_of G & G is_proper_subformula_of H implies
   F is_proper_subformula_of H;

theorem :: ZF_LANG:86
  F is_subformula_of G & G is_subformula_of H implies
   F is_subformula_of H;

theorem :: ZF_LANG:87
    G is_subformula_of H & H is_subformula_of G implies G = H;

theorem :: ZF_LANG:88
  not F is_proper_subformula_of x '=' y;

theorem :: ZF_LANG:89
  not F is_proper_subformula_of x 'in' y;

theorem :: ZF_LANG:90
  F is_proper_subformula_of 'not' H implies F is_subformula_of H;

theorem :: ZF_LANG:91
  F is_proper_subformula_of G '&' H implies
   F is_subformula_of G or F is_subformula_of H;

theorem :: ZF_LANG:92
  F is_proper_subformula_of All(x,H) implies F is_subformula_of H;

theorem :: ZF_LANG:93
    H is atomic implies not F is_proper_subformula_of H;

theorem :: ZF_LANG:94
    H is negative implies the_argument_of H is_proper_subformula_of H;

theorem :: ZF_LANG:95
    H is conjunctive implies
   the_left_argument_of H is_proper_subformula_of H &
    the_right_argument_of H is_proper_subformula_of H;

theorem :: ZF_LANG:96
    H is universal implies the_scope_of H is_proper_subformula_of H;

theorem :: ZF_LANG:97
  H is_subformula_of x '=' y iff H = x '=' y;

theorem :: ZF_LANG:98
  H is_subformula_of x 'in' y iff H = x 'in' y;

::
::           The Set of Subformulae of ZF-formulae
::

 definition let H;
  func Subformulae H -> set means
:: ZF_LANG:def 42
  a in it iff ex F st F = a & F is_subformula_of H;
 end;

canceled;

theorem :: ZF_LANG:100
  G in Subformulae H implies G is_subformula_of H;

theorem :: ZF_LANG:101
    F is_subformula_of H implies Subformulae F c= Subformulae H;

theorem :: ZF_LANG:102
  Subformulae x '=' y = { x '=' y };

theorem :: ZF_LANG:103
  Subformulae x 'in' y = { x 'in' y };

theorem :: ZF_LANG:104
  Subformulae 'not' H = Subformulae H \/ { 'not' H };

theorem :: ZF_LANG:105
  Subformulae (H '&' F) = Subformulae H \/ Subformulae F \/ { H '&' F };

theorem :: ZF_LANG:106
  Subformulae All(x,H) = Subformulae H \/ { All(x,H) };

theorem :: ZF_LANG:107
    H is atomic iff Subformulae H = { H };

theorem :: ZF_LANG:108
    H is negative implies
   Subformulae H = Subformulae the_argument_of H \/ { H };

theorem :: ZF_LANG:109
    H is conjunctive implies
   Subformulae H = Subformulae the_left_argument_of H \/
    Subformulae the_right_argument_of H \/ { H };

theorem :: ZF_LANG:110
    H is universal implies
   Subformulae H = Subformulae the_scope_of H \/ { H };

theorem :: ZF_LANG:111
    (H is_immediate_constituent_of G or H is_proper_subformula_of G or
   H is_subformula_of G) & G in Subformulae F implies H in Subformulae F;

::
::               The Structural Induction Schemes
::

scheme ZF_Ind { P[ZF-formula] } :
  for H holds P[H]
    provided
 for H st H is atomic holds P[H] and
 for H st H is negative & P[the_argument_of H] holds P[H] and
 for H st H is conjunctive &
    P[the_left_argument_of H] & P[the_right_argument_of H] holds P[H] and
 for H st H is universal & P[the_scope_of H] holds P[H];

scheme ZF_CompInd { P[ZF-formula] } :
  for H holds P[H]
    provided
 for H st for F st F is_proper_subformula_of H holds P[F] holds P[H];