:: A Model of ZF Set Theory Language
:: by Grzegorz Bancerek
::
:: Received April 4, 1989
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem defines VAR ZF_LANG:def 1 :
:: deftheorem defines x. ZF_LANG:def 2 :
:: deftheorem defines '=' ZF_LANG:def 3 :
:: deftheorem defines 'in' ZF_LANG:def 4 :
theorem :: ZF_LANG:1
canceled;
theorem :: ZF_LANG:2
canceled;
theorem :: ZF_LANG:3
canceled;
theorem :: ZF_LANG:4
canceled;
theorem :: ZF_LANG:5
canceled;
theorem :: ZF_LANG:6
theorem :: ZF_LANG:7
:: deftheorem defines 'not' ZF_LANG:def 5 :
:: deftheorem defines '&' ZF_LANG:def 6 :
:: deftheorem defines All ZF_LANG:def 7 :
theorem :: ZF_LANG:8
canceled;
theorem :: ZF_LANG:9
canceled;
theorem :: ZF_LANG:10
canceled;
theorem :: ZF_LANG:11
canceled;
theorem Th12: :: ZF_LANG:12
definition
func WFF -> non
empty set means :
Def8:
:: ZF_LANG:def 8
( ( for
a being
set st
a in it holds
a is
FinSequence of
NAT ) & ( for
x,
y being
Variable holds
(
x '=' y in it &
x 'in' y in it ) ) & ( for
p being
FinSequence of
NAT st
p in it holds
'not' p in it ) & ( for
p,
q being
FinSequence of
NAT st
p in it &
q in it holds
p '&' q in it ) & ( for
x being
Variable for
p being
FinSequence of
NAT st
p in it holds
All x,
p in it ) & ( for
D being non
empty set st ( for
a being
set st
a in D holds
a is
FinSequence of
NAT ) & ( for
x,
y being
Variable holds
(
x '=' y in D &
x 'in' y in D ) ) & ( for
p being
FinSequence of
NAT st
p in D holds
'not' p in D ) & ( for
p,
q being
FinSequence of
NAT st
p in D &
q in D holds
p '&' q in D ) & ( for
x being
Variable for
p being
FinSequence of
NAT st
p in D holds
All x,
p in D ) holds
it c= D ) );
existence
ex b1 being non empty set st
( ( for a being set st a in b1 holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in b1 & x 'in' y in b1 ) ) & ( for p being FinSequence of NAT st p in b1 holds
'not' p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p '&' q in b1 ) & ( for x being Variable
for p being FinSequence of NAT st p in b1 holds
All x,p in b1 ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for x being Variable
for p being FinSequence of NAT st p in D holds
All x,p in D ) holds
b1 c= D ) )
uniqueness
for b1, b2 being non empty set st ( for a being set st a in b1 holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in b1 & x 'in' y in b1 ) ) & ( for p being FinSequence of NAT st p in b1 holds
'not' p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p '&' q in b1 ) & ( for x being Variable
for p being FinSequence of NAT st p in b1 holds
All x,p in b1 ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for x being Variable
for p being FinSequence of NAT st p in D holds
All x,p in D ) holds
b1 c= D ) & ( for a being set st a in b2 holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in b2 & x 'in' y in b2 ) ) & ( for p being FinSequence of NAT st p in b2 holds
'not' p in b2 ) & ( for p, q being FinSequence of NAT st p in b2 & q in b2 holds
p '&' q in b2 ) & ( for x being Variable
for p being FinSequence of NAT st p in b2 holds
All x,p in b2 ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for x being Variable
for p being FinSequence of NAT st p in D holds
All x,p in D ) holds
b2 c= D ) holds
b1 = b2
end;
:: deftheorem Def8 defines WFF ZF_LANG:def 8 :
:: deftheorem Def9 defines ZF-formula-like ZF_LANG:def 9 :
theorem :: ZF_LANG:13
canceled;
theorem :: ZF_LANG:14
:: deftheorem Def10 defines being_equality ZF_LANG:def 10 :
:: deftheorem Def11 defines being_membership ZF_LANG:def 11 :
:: deftheorem Def12 defines negative ZF_LANG:def 12 :
:: deftheorem Def13 defines conjunctive ZF_LANG:def 13 :
:: deftheorem Def14 defines universal ZF_LANG:def 14 :
theorem :: ZF_LANG:15
canceled;
theorem :: ZF_LANG:16
for
H being
ZF-formula holds
( (
H is
being_equality implies ex
x,
y being
Variable st
H = x '=' y ) & ( ex
x,
y being
Variable st
H = x '=' y implies
H is
being_equality ) & (
H is
being_membership implies ex
x,
y being
Variable st
H = x 'in' y ) & ( ex
x,
y being
Variable st
H = x 'in' y implies
H is
being_membership ) & (
H is
negative implies ex
H1 being
ZF-formula st
H = 'not' H1 ) & ( ex
H1 being
ZF-formula st
H = 'not' H1 implies
H is
negative ) & (
H is
conjunctive implies ex
F,
G being
ZF-formula st
H = F '&' G ) & ( ex
F,
G being
ZF-formula st
H = F '&' G implies
H is
conjunctive ) & (
H is
universal implies ex
x being
Variable ex
H1 being
ZF-formula st
H = All x,
H1 ) & ( ex
x being
Variable ex
H1 being
ZF-formula st
H = All x,
H1 implies
H is
universal ) )
by Def10, Def11, Def12, Def13, Def14;
:: deftheorem Def15 defines atomic ZF_LANG:def 15 :
:: deftheorem defines 'or' ZF_LANG:def 16 :
:: deftheorem defines => ZF_LANG:def 17 :
:: deftheorem defines <=> ZF_LANG:def 18 :
:: deftheorem defines Ex ZF_LANG:def 19 :
:: deftheorem Def20 defines disjunctive ZF_LANG:def 20 :
:: deftheorem Def21 defines conditional ZF_LANG:def 21 :
:: deftheorem Def22 defines biconditional ZF_LANG:def 22 :
:: deftheorem Def23 defines existential ZF_LANG:def 23 :
theorem :: ZF_LANG:17
canceled;
theorem :: ZF_LANG:18
canceled;
theorem :: ZF_LANG:19
canceled;
theorem :: ZF_LANG:20
canceled;
theorem :: ZF_LANG:21
canceled;
theorem :: ZF_LANG:22
for
H being
ZF-formula holds
( (
H is
disjunctive implies ex
F,
G being
ZF-formula st
H = F 'or' G ) & ( ex
F,
G being
ZF-formula st
H = F 'or' G implies
H is
disjunctive ) & (
H is
conditional implies ex
F,
G being
ZF-formula st
H = F => G ) & ( ex
F,
G being
ZF-formula st
H = F => G implies
H is
conditional ) & (
H is
biconditional implies ex
F,
G being
ZF-formula st
H = F <=> G ) & ( ex
F,
G being
ZF-formula st
H = F <=> G implies
H is
biconditional ) & (
H is
existential implies ex
x being
Variable ex
H1 being
ZF-formula st
H = Ex x,
H1 ) & ( ex
x being
Variable ex
H1 being
ZF-formula st
H = Ex x,
H1 implies
H is
existential ) )
by Def20, Def21, Def22, Def23;
definition
let x,
y be
Variable;
let H be
ZF-formula;
func All x,
y,
H -> ZF-formula equals :: ZF_LANG:def 24
All x,
(All y,H);
coherence
All x,(All y,H) is ZF-formula
;
func Ex x,
y,
H -> ZF-formula equals :: ZF_LANG:def 25
Ex x,
(Ex y,H);
coherence
Ex x,(Ex y,H) is ZF-formula
;
end;
:: deftheorem defines All ZF_LANG:def 24 :
:: deftheorem defines Ex ZF_LANG:def 25 :
theorem :: ZF_LANG:23
definition
let x,
y,
z be
Variable;
let H be
ZF-formula;
func All x,
y,
z,
H -> ZF-formula equals :: ZF_LANG:def 26
All x,
(All y,z,H);
coherence
All x,(All y,z,H) is ZF-formula
;
func Ex x,
y,
z,
H -> ZF-formula equals :: ZF_LANG:def 27
Ex x,
(Ex y,z,H);
coherence
Ex x,(Ex y,z,H) is ZF-formula
;
end;
:: deftheorem defines All ZF_LANG:def 26 :
:: deftheorem defines Ex ZF_LANG:def 27 :
theorem :: ZF_LANG:24
for
x,
y,
z being
Variable for
H being
ZF-formula holds
(
All x,
y,
z,
H = All x,
(All y,z,H) &
Ex x,
y,
z,
H = Ex x,
(Ex y,z,H) ) ;
theorem Th25: :: ZF_LANG:25
theorem Th26: :: ZF_LANG:26
theorem Th27: :: ZF_LANG:27
theorem Th28: :: ZF_LANG:28
theorem Th29: :: ZF_LANG:29
theorem :: ZF_LANG:30
theorem Th31: :: ZF_LANG:31
theorem :: ZF_LANG:32
canceled;
theorem Th33: :: ZF_LANG:33
theorem Th34: :: ZF_LANG:34
theorem Th35: :: ZF_LANG:35
theorem Th36: :: ZF_LANG:36
theorem Th37: :: ZF_LANG:37
theorem Th38: :: ZF_LANG:38
theorem Th39: :: ZF_LANG:39
theorem Th40: :: ZF_LANG:40
theorem :: ZF_LANG:41
theorem :: ZF_LANG:42
theorem :: ZF_LANG:43
theorem :: ZF_LANG:44
theorem :: ZF_LANG:45
theorem Th46: :: ZF_LANG:46
theorem Th47: :: ZF_LANG:47
theorem Th48: :: ZF_LANG:48
theorem Th49: :: ZF_LANG:49
theorem Th50: :: ZF_LANG:50
theorem Th51: :: ZF_LANG:51
:: deftheorem Def28 defines Var1 ZF_LANG:def 28 :
:: deftheorem Def29 defines Var2 ZF_LANG:def 29 :
theorem :: ZF_LANG:52
theorem Th53: :: ZF_LANG:53
theorem Th54: :: ZF_LANG:54
:: deftheorem Def30 defines the_argument_of ZF_LANG:def 30 :
definition
let H be
ZF-formula;
assume A1:
(
H is
conjunctive or
H is
disjunctive )
;
func the_left_argument_of H -> ZF-formula means :
Def31:
:: ZF_LANG:def 31
ex
H1 being
ZF-formula st
it '&' H1 = H if H is
conjunctive otherwise ex
H1 being
ZF-formula st
it 'or' H1 = H;
existence
( ( H is conjunctive implies ex b1, H1 being ZF-formula st b1 '&' H1 = H ) & ( not H is conjunctive implies ex b1, H1 being ZF-formula st b1 'or' H1 = H ) )
by A1, Def13, Def20;
uniqueness
for b1, b2 being ZF-formula holds
( ( H is conjunctive & ex H1 being ZF-formula st b1 '&' H1 = H & ex H1 being ZF-formula st b2 '&' H1 = H implies b1 = b2 ) & ( not H is conjunctive & ex H1 being ZF-formula st b1 'or' H1 = H & ex H1 being ZF-formula st b2 'or' H1 = H implies b1 = b2 ) )
by Th47, Th48;
consistency
for b1 being ZF-formula holds verum
;
func the_right_argument_of H -> ZF-formula means :
Def32:
:: ZF_LANG:def 32
ex
H1 being
ZF-formula st
H1 '&' it = H if H is
conjunctive otherwise ex
H1 being
ZF-formula st
H1 'or' it = H;
existence
( ( H is conjunctive implies ex b1, H1 being ZF-formula st H1 '&' b1 = H ) & ( not H is conjunctive implies ex b1, H1 being ZF-formula st H1 'or' b1 = H ) )
uniqueness
for b1, b2 being ZF-formula holds
( ( H is conjunctive & ex H1 being ZF-formula st H1 '&' b1 = H & ex H1 being ZF-formula st H1 '&' b2 = H implies b1 = b2 ) & ( not H is conjunctive & ex H1 being ZF-formula st H1 'or' b1 = H & ex H1 being ZF-formula st H1 'or' b2 = H implies b1 = b2 ) )
by Th47, Th48;
consistency
for b1 being ZF-formula holds verum
;
end;
:: deftheorem Def31 defines the_left_argument_of ZF_LANG:def 31 :
:: deftheorem Def32 defines the_right_argument_of ZF_LANG:def 32 :
theorem :: ZF_LANG:55
canceled;
theorem :: ZF_LANG:56
theorem Th57: :: ZF_LANG:57
theorem Th58: :: ZF_LANG:58
theorem :: ZF_LANG:59
definition
let H be
ZF-formula;
assume A1:
(
H is
universal or
H is
existential )
;
func bound_in H -> Variable means :
Def33:
:: ZF_LANG:def 33
ex
H1 being
ZF-formula st
All it,
H1 = H if H is
universal otherwise ex
H1 being
ZF-formula st
Ex it,
H1 = H;
existence
( ( H is universal implies ex b1 being Variable ex H1 being ZF-formula st All b1,H1 = H ) & ( not H is universal implies ex b1 being Variable ex H1 being ZF-formula st Ex b1,H1 = H ) )
by A1, Def14, Def23;
uniqueness
for b1, b2 being Variable holds
( ( H is universal & ex H1 being ZF-formula st All b1,H1 = H & ex H1 being ZF-formula st All b2,H1 = H implies b1 = b2 ) & ( not H is universal & ex H1 being ZF-formula st Ex b1,H1 = H & ex H1 being ZF-formula st Ex b2,H1 = H implies b1 = b2 ) )
by Th12, Th51;
consistency
for b1 being Variable holds verum
;
func the_scope_of H -> ZF-formula means :
Def34:
:: ZF_LANG:def 34
ex
x being
Variable st
All x,
it = H if H is
universal otherwise ex
x being
Variable st
Ex x,
it = H;
existence
( ( H is universal implies ex b1 being ZF-formula ex x being Variable st All x,b1 = H ) & ( not H is universal implies ex b1 being ZF-formula ex x being Variable st Ex x,b1 = H ) )
uniqueness
for b1, b2 being ZF-formula holds
( ( H is universal & ex x being Variable st All x,b1 = H & ex x being Variable st All x,b2 = H implies b1 = b2 ) & ( not H is universal & ex x being Variable st Ex x,b1 = H & ex x being Variable st Ex x,b2 = H implies b1 = b2 ) )
by Th12, Th51;
consistency
for b1 being ZF-formula holds verum
;
end;
:: deftheorem Def33 defines bound_in ZF_LANG:def 33 :
:: deftheorem Def34 defines the_scope_of ZF_LANG:def 34 :
theorem :: ZF_LANG:60
theorem Th61: :: ZF_LANG:61
theorem Th62: :: ZF_LANG:62
theorem :: ZF_LANG:63
:: deftheorem Def35 defines the_antecedent_of ZF_LANG:def 35 :
:: deftheorem Def36 defines the_consequent_of ZF_LANG:def 36 :
theorem :: ZF_LANG:64
theorem :: ZF_LANG:65
:: deftheorem Def37 defines the_left_side_of ZF_LANG:def 37 :
:: deftheorem Def38 defines the_right_side_of ZF_LANG:def 38 :
theorem :: ZF_LANG:66
theorem :: ZF_LANG:67
:: deftheorem Def39 defines is_immediate_constituent_of ZF_LANG:def 39 :
theorem :: ZF_LANG:68
canceled;
theorem Th69: :: ZF_LANG:69
theorem Th70: :: ZF_LANG:70
theorem Th71: :: ZF_LANG:71
theorem Th72: :: ZF_LANG:72
theorem Th73: :: ZF_LANG:73
theorem :: ZF_LANG:74
theorem Th75: :: ZF_LANG:75
theorem Th76: :: ZF_LANG:76
theorem Th77: :: ZF_LANG:77
:: deftheorem Def40 defines is_subformula_of ZF_LANG:def 40 :
theorem :: ZF_LANG:78
canceled;
theorem Th79: :: ZF_LANG:79
:: deftheorem Def41 defines is_proper_subformula_of ZF_LANG:def 41 :
theorem :: ZF_LANG:80
canceled;
theorem Th81: :: ZF_LANG:81
theorem Th82: :: ZF_LANG:82
theorem Th83: :: ZF_LANG:83
theorem Th84: :: ZF_LANG:84
theorem Th85: :: ZF_LANG:85
theorem Th86: :: ZF_LANG:86
theorem :: ZF_LANG:87
theorem Th88: :: ZF_LANG:88
theorem Th89: :: ZF_LANG:89
theorem Th90: :: ZF_LANG:90
theorem Th91: :: ZF_LANG:91
theorem Th92: :: ZF_LANG:92
theorem :: ZF_LANG:93
theorem :: ZF_LANG:94
theorem :: ZF_LANG:95
theorem :: ZF_LANG:96
theorem Th97: :: ZF_LANG:97
theorem Th98: :: ZF_LANG:98
:: deftheorem Def42 defines Subformulae ZF_LANG:def 42 :
theorem :: ZF_LANG:99
canceled;
theorem Th100: :: ZF_LANG:100
theorem :: ZF_LANG:101
theorem Th102: :: ZF_LANG:102
theorem Th103: :: ZF_LANG:103
theorem Th104: :: ZF_LANG:104
theorem Th105: :: ZF_LANG:105
theorem Th106: :: ZF_LANG:106
theorem :: ZF_LANG:107
theorem :: ZF_LANG:108
theorem :: ZF_LANG:109
theorem :: ZF_LANG:110
theorem :: ZF_LANG:111