Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

### A Model of ZF Set Theory Language

by
Grzegorz Bancerek

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];
```