:: by Grzegorz Bancerek

::

:: Received September 26, 1990

:: Copyright (c) 1990-2021 Association of Mizar Users

theorem Th2: :: ZFMODEL2:2

for x, y being Variable

for H being ZF-formula st not y in variables_in H holds

( ( x in Free H implies Free (H / (x,y)) = ((Free H) \ {x}) \/ {y} ) & ( not x in Free H implies Free (H / (x,y)) = Free H ) )

for H being ZF-formula st not y in variables_in H holds

( ( x in Free H implies Free (H / (x,y)) = ((Free H) \ {x}) \/ {y} ) & ( not x in Free H implies Free (H / (x,y)) = Free H ) )

proof end;

theorem Th3: :: ZFMODEL2:3

for H being ZF-formula holds

( ex i being Element of NAT st

for j being Element of NAT st x. j in variables_in H holds

j < i & not for x being Variable holds x in variables_in H )

( ex i being Element of NAT st

for j being Element of NAT st x. j in variables_in H holds

j < i & not for x being Variable holds x in variables_in H )

proof end;

theorem Th4: :: ZFMODEL2:4

for x being Variable

for M being non empty set

for H being ZF-formula

for v being Function of VAR,M st not x in variables_in H holds

( M,v |= H iff M,v |= All (x,H) )

for M being non empty set

for H being ZF-formula

for v being Function of VAR,M st not x in variables_in H holds

( M,v |= H iff M,v |= All (x,H) )

proof end;

theorem Th5: :: ZFMODEL2:5

for x being Variable

for M being non empty set

for m being Element of M

for H being ZF-formula

for v being Function of VAR,M st not x in variables_in H holds

( M,v |= H iff M,v / (x,m) |= H )

for M being non empty set

for m being Element of M

for H being ZF-formula

for v being Function of VAR,M st not x in variables_in H holds

( M,v |= H iff M,v / (x,m) |= H )

proof end;

theorem Th6: :: ZFMODEL2:6

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) )

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) )

proof end;

theorem Th7: :: ZFMODEL2:7

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) )

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) )

proof end;

theorem Th8: :: ZFMODEL2:8

for x1, x2, x3, x4 being Variable

for M being non empty set

for m, m1, m2, 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) )

for M being non empty set

for m, m1, m2, 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) )

proof end;

theorem Th9: :: ZFMODEL2:9

for x being Variable

for M being non empty set

for m being Element of M

for H being ZF-formula

for v being Function of VAR,M st not x in Free H holds

( M,v |= H iff M,v / (x,m) |= H )

for M being non empty set

for m being Element of M

for H being ZF-formula

for v being Function of VAR,M st not x in Free H holds

( M,v |= H iff M,v / (x,m) |= H )

proof end;

theorem Th10: :: ZFMODEL2:10

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 )

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 )

proof end;

Lm1: x. 0 <> x. 3

by ZF_LANG1:76;

Lm2: x. 0 <> x. 4

by ZF_LANG1:76;

Lm3: x. 3 <> x. 4

by ZF_LANG1:76;

theorem Th11: :: ZFMODEL2:11

for M being non empty set

for H being ZF-formula

for v being Function of VAR,M st Free H c= {(x. 3),(x. 4)} & M |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds

def_func' (H,v) = def_func (H,M)

for H being ZF-formula

for v being Function of VAR,M st Free H c= {(x. 3),(x. 4)} & M |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds

def_func' (H,v) = def_func (H,M)

proof end;

theorem Th12: :: ZFMODEL2:12

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 in variables_in H holds

( M,v |= H / (y,x) iff M,v / (y,(v . x)) |= H )

for M being non empty set

for H being ZF-formula

for v being Function of VAR,M st not x in variables_in H holds

( M,v |= H / (y,x) iff M,v / (y,(v . x)) |= H )

proof end;

theorem Th13: :: ZFMODEL2:13

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 in variables_in H & M,v |= H holds

M,v / (x,(v . y)) |= H / (y,x)

for M being non empty set

for H being ZF-formula

for v being Function of VAR,M st not x in variables_in H & M,v |= H holds

M,v / (x,(v . y)) |= H / (y,x)

proof end;

theorem Th14: :: ZFMODEL2:14

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)))) )

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)))) )

proof end;

theorem :: ZFMODEL2:15

for x, y being Variable

for M being non empty set

for H being ZF-formula st not x in variables_in H holds

( M |= H / (y,x) iff M |= H )

for M being non empty set

for H being ZF-formula st not x in variables_in H holds

( M |= H / (y,x) iff M |= H )

proof end;

theorem Th16: :: ZFMODEL2:16

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) )

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) )

proof end;

theorem :: ZFMODEL2:17

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) )

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) )

proof end;

theorem :: ZFMODEL2:18

for M being non empty set

for F, G being Function st F is_definable_in M & G is_definable_in M holds

F * G is_definable_in M

for F, G being Function st F is_definable_in M & G is_definable_in M holds

F * G is_definable_in M

proof end;

theorem Th19: :: ZFMODEL2:19

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 holds

( M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) iff for m1 being Element of M ex m2 being Element of M st

for m3 being Element of M holds

( M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H iff m3 = m2 ) )

for H being ZF-formula

for v being Function of VAR,M st not x. 0 in Free H holds

( M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) iff for m1 being Element of M ex m2 being Element of M st

for m3 being Element of M holds

( M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H iff m3 = m2 ) )

proof end;

theorem :: ZFMODEL2:20

for M being non empty set

for H being ZF-formula

for F, G being Function st F is_definable_in M & G is_definable_in M & Free H c= {(x. 3)} holds

for FG being Function st dom FG = M & ( for v being Function of VAR,M holds

( ( M,v |= H implies FG . (v . (x. 3)) = F . (v . (x. 3)) ) & ( M,v |= 'not' H implies FG . (v . (x. 3)) = G . (v . (x. 3)) ) ) ) holds

FG is_definable_in M

for H being ZF-formula

for F, G being Function st F is_definable_in M & G is_definable_in M & Free H c= {(x. 3)} holds

for FG being Function st dom FG = M & ( for v being Function of VAR,M holds

( ( M,v |= H implies FG . (v . (x. 3)) = F . (v . (x. 3)) ) & ( M,v |= 'not' H implies FG . (v . (x. 3)) = G . (v . (x. 3)) ) ) ) holds

FG is_definable_in M

proof end;

theorem :: ZFMODEL2:21

for M being non empty set

for F, G being Function st F is_parametrically_definable_in M & G is_parametrically_definable_in M holds

G * F is_parametrically_definable_in M

for F, G being Function st F is_parametrically_definable_in M & G is_parametrically_definable_in M holds

G * F is_parametrically_definable_in M

proof end;

theorem :: ZFMODEL2:22

for M being non empty set

for H, H1, H2 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

for H, H1, H2 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

proof end;

theorem :: ZFMODEL2:24