begin
theorem Th1:
theorem Th2:
theorem
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
for
x,
y,
z being
Variable for
M being non
empty set for
m1,
m2,
m3 being
Element of
M for
v being
Function of
VAR ,
M st
x <> y &
y <> z &
z <> x holds
(
((v / x,m1) / y,m2) / z,
m3 = ((v / z,m3) / y,m2) / x,
m1 &
((v / x,m1) / y,m2) / z,
m3 = ((v / y,m2) / z,m3) / x,
m1 )
theorem Th8:
for
x1,
x2,
x3,
x4 being
Variable for
M being non
empty set for
m1,
m2,
m3,
m4 being
Element of
M for
v being
Function of
VAR ,
M st
x1 <> x2 &
x1 <> x3 &
x1 <> x4 &
x2 <> x3 &
x2 <> x4 &
x3 <> x4 holds
(
(((v / x1,m1) / x2,m2) / x3,m3) / x4,
m4 = (((v / x2,m2) / x3,m3) / x4,m4) / x1,
m1 &
(((v / x1,m1) / x2,m2) / x3,m3) / x4,
m4 = (((v / x3,m3) / x4,m4) / x1,m1) / x2,
m2 &
(((v / x1,m1) / x2,m2) / x3,m3) / x4,
m4 = (((v / x4,m4) / x2,m2) / x3,m3) / x1,
m1 )
theorem Th9:
for
x1,
x2,
x3,
x4 being
Variable for
M being non
empty set for
m1,
m2,
m,
m3,
m4 being
Element of
M for
v being
Function of
VAR ,
M holds
(
((v / x1,m1) / x2,m2) / x1,
m = (v / x2,m2) / x1,
m &
(((v / x1,m1) / x2,m2) / x3,m3) / x1,
m = ((v / x2,m2) / x3,m3) / x1,
m &
((((v / x1,m1) / x2,m2) / x3,m3) / x4,m4) / x1,
m = (((v / x2,m2) / x3,m3) / x4,m4) / x1,
m )
theorem Th10:
theorem Th11:
for
M being non
empty set for
H being
ZF-formula for
v being
Function of
VAR ,
M st not
x. 0 in Free H &
M,
v |= All (x. 3),
(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) holds
for
m1,
m2 being
Element of
M holds
(
(def_func' H,v) . m1 = m2 iff
M,
(v / (x. 3),m1) / (x. 4),
m2 |= H )
Lm1:
x. 0 <> x. 3
by ZF_LANG1:86;
Lm2:
x. 0 <> x. 4
by ZF_LANG1:86;
Lm3:
x. 3 <> x. 4
by ZF_LANG1:86;
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
for
x,
y being
Variable for
M being non
empty set for
H being
ZF-formula for
v being
Function of
VAR ,
M st not
x. 0 in Free H &
M,
v |= All (x. 3),
(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) & not
x in variables_in H & not
y in Free H &
x <> x. 0 &
x <> x. 3 &
x <> x. 4 holds
( not
x. 0 in Free (H / y,x) &
M,
v / x,
(v . y) |= All (x. 3),
(Ex (x. 0 ),(All (x. 4),((H / y,x) <=> ((x. 4) '=' (x. 0 ))))) &
def_func' H,
v = def_func' (H / y,x),
(v / x,(v . y)) )
theorem
theorem Th17:
for
M being non
empty set for
i being
Element of
NAT for
H1 being
ZF-formula for
v1 being
Function of
VAR ,
M st not
x. 0 in Free H1 &
M,
v1 |= All (x. 3),
(Ex (x. 0 ),(All (x. 4),(H1 <=> ((x. 4) '=' (x. 0 ))))) holds
ex
H2 being
ZF-formula ex
v2 being
Function of
VAR ,
M st
( ( for
j being
Element of
NAT st
j < i &
x. j in variables_in H2 & not
j = 3 holds
j = 4 ) & not
x. 0 in Free H2 &
M,
v2 |= All (x. 3),
(Ex (x. 0 ),(All (x. 4),(H2 <=> ((x. 4) '=' (x. 0 ))))) &
def_func' H1,
v1 = def_func' H2,
v2 )
theorem
for
M being non
empty set for
H1 being
ZF-formula for
v1 being
Function of
VAR ,
M st not
x. 0 in Free H1 &
M,
v1 |= All (x. 3),
(Ex (x. 0 ),(All (x. 4),(H1 <=> ((x. 4) '=' (x. 0 ))))) holds
ex
H2 being
ZF-formula ex
v2 being
Function of
VAR ,
M st
(
(Free H1) /\ (Free H2) c= {(x. 3),(x. 4)} & not
x. 0 in Free H2 &
M,
v2 |= All (x. 3),
(Ex (x. 0 ),(All (x. 4),(H2 <=> ((x. 4) '=' (x. 0 ))))) &
def_func' H1,
v1 = def_func' H2,
v2 )
theorem
theorem Th20:
theorem
theorem
theorem
for
M being non
empty set for
H1,
H2,
H being
ZF-formula for
v being
Function of
VAR ,
M st
{(x. 0 ),(x. 1),(x. 2)} misses Free H1 &
M,
v |= All (x. 3),
(Ex (x. 0 ),(All (x. 4),(H1 <=> ((x. 4) '=' (x. 0 ))))) &
{(x. 0 ),(x. 1),(x. 2)} misses Free H2 &
M,
v |= All (x. 3),
(Ex (x. 0 ),(All (x. 4),(H2 <=> ((x. 4) '=' (x. 0 ))))) &
{(x. 0 ),(x. 1),(x. 2)} misses Free H & not
x. 4
in Free H holds
for
FG being
Function st
dom FG = M & ( for
m being
Element of
M holds
( (
M,
v / (x. 3),
m |= H implies
FG . m = (def_func' H1,v) . m ) & (
M,
v / (x. 3),
m |= 'not' H implies
FG . m = (def_func' H2,v) . m ) ) ) holds
FG is_parametrically_definable_in M
theorem Th24:
theorem