:: ZFMODEL2 semantic presentation

theorem Th1: :: ZFMODEL2:1
for b1, b2 being Variable
for b3 being ZF-formula holds Free (b3 / b1,b2) c= ((Free b3) \ {b1}) \/ {b2}
proof end;

theorem Th2: :: ZFMODEL2:2
for b1, b2 being Variable
for b3 being ZF-formula st not b1 in variables_in b3 holds
( ( b2 in Free b3 implies Free (b3 / b2,b1) = ((Free b3) \ {b2}) \/ {b1} ) & ( not b2 in Free b3 implies Free (b3 / b2,b1) = Free b3 ) )
proof end;

theorem Th3: :: ZFMODEL2:3
for b1 being ZF-formula holds variables_in b1 is finite
proof end;

theorem Th4: :: ZFMODEL2:4
for b1 being ZF-formula holds
( ex b2 being Nat st
for b3 being Nat st x. b3 in variables_in b1 holds
b3 < b2 & not for b2 being Variable holds b2 in variables_in b1 )
proof end;

theorem Th5: :: ZFMODEL2:5
for b1 being Variable
for b2 being non empty set
for b3 being ZF-formula
for b4 being Function of VAR ,b2 st not b1 in variables_in b3 holds
( b2,b4 |= b3 iff b2,b4 |= All b1,b3 )
proof end;

theorem Th6: :: ZFMODEL2:6
for b1 being Variable
for b2 being non empty set
for b3 being Element of b2
for b4 being ZF-formula
for b5 being Function of VAR ,b2 st not b1 in variables_in b4 holds
( b2,b5 |= b4 iff b2,b5 / b1,b3 |= b4 )
proof end;

theorem Th7: :: ZFMODEL2:7
for b1, b2, b3 being Variable
for b4 being non empty set
for b5, b6, b7 being Element of b4
for b8 being Function of VAR ,b4 st b1 <> b2 & b2 <> b3 & b3 <> b1 holds
( ((b8 / b1,b5) / b2,b6) / b3,b7 = ((b8 / b3,b7) / b2,b6) / b1,b5 & ((b8 / b1,b5) / b2,b6) / b3,b7 = ((b8 / b2,b6) / b3,b7) / b1,b5 )
proof end;

theorem Th8: :: ZFMODEL2:8
for b1, b2, b3, b4 being Variable
for b5 being non empty set
for b6, b7, b8, b9 being Element of b5
for b10 being Function of VAR ,b5 st b1 <> b2 & b1 <> b3 & b1 <> b4 & b2 <> b3 & b2 <> b4 & b3 <> b4 holds
( (((b10 / b1,b6) / b2,b7) / b3,b8) / b4,b9 = (((b10 / b2,b7) / b3,b8) / b4,b9) / b1,b6 & (((b10 / b1,b6) / b2,b7) / b3,b8) / b4,b9 = (((b10 / b3,b8) / b4,b9) / b1,b6) / b2,b7 & (((b10 / b1,b6) / b2,b7) / b3,b8) / b4,b9 = (((b10 / b4,b9) / b2,b7) / b3,b8) / b1,b6 )
proof end;

theorem Th9: :: ZFMODEL2:9
for b1, b2, b3, b4 being Variable
for b5 being non empty set
for b6, b7, b8, b9, b10 being Element of b5
for b11 being Function of VAR ,b5 holds
( ((b11 / b1,b6) / b2,b7) / b1,b8 = (b11 / b2,b7) / b1,b8 & (((b11 / b1,b6) / b2,b7) / b3,b9) / b1,b8 = ((b11 / b2,b7) / b3,b9) / b1,b8 & ((((b11 / b1,b6) / b2,b7) / b3,b9) / b4,b10) / b1,b8 = (((b11 / b2,b7) / b3,b9) / b4,b10) / b1,b8 )
proof end;

theorem Th10: :: ZFMODEL2:10
for b1 being Variable
for b2 being non empty set
for b3 being Element of b2
for b4 being ZF-formula
for b5 being Function of VAR ,b2 st not b1 in Free b4 holds
( b2,b5 |= b4 iff b2,b5 / b1,b3 |= b4 )
proof end;

theorem Th11: :: ZFMODEL2:11
for b1 being non empty set
for b2 being ZF-formula
for b3 being Function of VAR ,b1 st not x. 0 in Free b2 & b1,b3 |= All (x. 3),(Ex (x. 0),(All (x. 4),(b2 <=> ((x. 4) '=' (x. 0))))) holds
for b4, b5 being Element of b1 holds
( (def_func' b2,b3) . b4 = b5 iff b1,(b3 / (x. 3),b4) / (x. 4),b5 |= b2 )
proof end;

Lemma11: ( x. 0 <> x. 3 & x. 0 <> x. 4 & x. 3 <> x. 4 )
by ZF_LANG1:86;

theorem Th12: :: ZFMODEL2:12
for b1 being non empty set
for b2 being ZF-formula
for b3 being Function of VAR ,b1 st Free b2 c= {(x. 3),(x. 4)} & b1 |= All (x. 3),(Ex (x. 0),(All (x. 4),(b2 <=> ((x. 4) '=' (x. 0))))) holds
def_func' b2,b3 = def_func b2,b1
proof end;

theorem Th13: :: ZFMODEL2:13
for b1, b2 being Variable
for b3 being non empty set
for b4 being ZF-formula
for b5 being Function of VAR ,b3 st not b1 in variables_in b4 holds
( b3,b5 |= b4 / b2,b1 iff b3,b5 / b2,(b5 . b1) |= b4 )
proof end;

theorem Th14: :: ZFMODEL2:14
for b1, b2 being Variable
for b3 being non empty set
for b4 being ZF-formula
for b5 being Function of VAR ,b3 st not b1 in variables_in b4 & b3,b5 |= b4 holds
b3,b5 / b1,(b5 . b2) |= b4 / b2,b1
proof end;

theorem Th15: :: ZFMODEL2:15
for b1, b2 being Variable
for b3 being non empty set
for b4 being ZF-formula
for b5 being Function of VAR ,b3 st not x. 0 in Free b4 & b3,b5 |= All (x. 3),(Ex (x. 0),(All (x. 4),(b4 <=> ((x. 4) '=' (x. 0))))) & not b1 in variables_in b4 & b2 <> x. 3 & b2 <> x. 4 & not b2 in Free b4 & b1 <> x. 0 & b1 <> x. 3 & b1 <> x. 4 holds
( not x. 0 in Free (b4 / b2,b1) & b3,b5 / b1,(b5 . b2) |= All (x. 3),(Ex (x. 0),(All (x. 4),((b4 / b2,b1) <=> ((x. 4) '=' (x. 0))))) & def_func' b4,b5 = def_func' (b4 / b2,b1),(b5 / b1,(b5 . b2)) )
proof end;

theorem Th16: :: ZFMODEL2:16
for b1, b2 being Variable
for b3 being non empty set
for b4 being ZF-formula st not b1 in variables_in b4 holds
( b3 |= b4 / b2,b1 iff b3 |= b4 )
proof end;

theorem Th17: :: ZFMODEL2:17
for b1 being non empty set
for b2 being Nat
for b3 being ZF-formula
for b4 being Function of VAR ,b1 st not x. 0 in Free b3 & b1,b4 |= All (x. 3),(Ex (x. 0),(All (x. 4),(b3 <=> ((x. 4) '=' (x. 0))))) holds
ex b5 being ZF-formulaex b6 being Function of VAR ,b1 st
( ( for b7 being Nat st b7 < b2 & x. b7 in variables_in b5 & not b7 = 3 holds
b7 = 4 ) & not x. 0 in Free b5 & b1,b6 |= All (x. 3),(Ex (x. 0),(All (x. 4),(b5 <=> ((x. 4) '=' (x. 0))))) & def_func' b3,b4 = def_func' b5,b6 )
proof end;

theorem Th18: :: ZFMODEL2:18
for b1 being non empty set
for b2 being ZF-formula
for b3 being Function of VAR ,b1 st not x. 0 in Free b2 & b1,b3 |= All (x. 3),(Ex (x. 0),(All (x. 4),(b2 <=> ((x. 4) '=' (x. 0))))) holds
ex b4 being ZF-formulaex b5 being Function of VAR ,b1 st
( (Free b2) /\ (Free b4) c= {(x. 3),(x. 4)} & not x. 0 in Free b4 & b1,b5 |= All (x. 3),(Ex (x. 0),(All (x. 4),(b4 <=> ((x. 4) '=' (x. 0))))) & def_func' b2,b3 = def_func' b4,b5 )
proof end;

theorem Th19: :: ZFMODEL2:19
for b1 being non empty set
for b2, b3 being Function st b2 is_definable_in b1 & b3 is_definable_in b1 holds
b2 * b3 is_definable_in b1
proof end;

theorem Th20: :: ZFMODEL2:20
for b1 being non empty set
for b2 being ZF-formula
for b3 being Function of VAR ,b1 st not x. 0 in Free b2 holds
( b1,b3 |= All (x. 3),(Ex (x. 0),(All (x. 4),(b2 <=> ((x. 4) '=' (x. 0))))) iff for b4 being Element of b1 ex b5 being Element of b1 st
for b6 being Element of b1 holds
( b1,(b3 / (x. 3),b4) / (x. 4),b6 |= b2 iff b6 = b5 ) )
proof end;

theorem Th21: :: ZFMODEL2:21
for b1 being non empty set
for b2 being ZF-formula
for b3, b4 being Function st b3 is_definable_in b1 & b4 is_definable_in b1 & Free b2 c= {(x. 3)} holds
for b5 being Function st dom b5 = b1 & ( for b6 being Function of VAR ,b1 holds
( ( b1,b6 |= b2 implies b5 . (b6 . (x. 3)) = b3 . (b6 . (x. 3)) ) & ( b1,b6 |= 'not' b2 implies b5 . (b6 . (x. 3)) = b4 . (b6 . (x. 3)) ) ) ) holds
b5 is_definable_in b1
proof end;

theorem Th22: :: ZFMODEL2:22
for b1 being non empty set
for b2, b3 being Function st b2 is_parametrically_definable_in b1 & b3 is_parametrically_definable_in b1 holds
b3 * b2 is_parametrically_definable_in b1
proof end;

theorem Th23: :: ZFMODEL2:23
for b1 being non empty set
for b2, b3, b4 being ZF-formula
for b5 being Function of VAR ,b1 st {(x. 0),(x. 1),(x. 2)} misses Free b2 & b1,b5 |= All (x. 3),(Ex (x. 0),(All (x. 4),(b2 <=> ((x. 4) '=' (x. 0))))) & {(x. 0),(x. 1),(x. 2)} misses Free b3 & b1,b5 |= All (x. 3),(Ex (x. 0),(All (x. 4),(b3 <=> ((x. 4) '=' (x. 0))))) & {(x. 0),(x. 1),(x. 2)} misses Free b4 & not x. 4 in Free b4 holds
for b6 being Function st dom b6 = b1 & ( for b7 being Element of b1 holds
( ( b1,b5 / (x. 3),b7 |= b4 implies b6 . b7 = (def_func' b2,b5) . b7 ) & ( b1,b5 / (x. 3),b7 |= 'not' b4 implies b6 . b7 = (def_func' b3,b5) . b7 ) ) ) holds
b6 is_parametrically_definable_in b1
proof end;

theorem Th24: :: ZFMODEL2:24
for b1 being non empty set holds id b1 is_definable_in b1
proof end;

theorem Th25: :: ZFMODEL2:25
for b1 being non empty set holds id b1 is_parametrically_definable_in b1
proof end;