let M1, M2 be non empty set ; ( M1 is_elementary_subsystem_of M2 implies M1 <==> M2 )
assume that
M1 c= M2
and
A1:
for H being ZF-formula
for v being Function of VAR,M1 holds
( M1,v |= H iff M2,M2 ! v |= H )
; ZFREFLE1:def 3 M1 <==> M2
let H be ZF-formula; ZFREFLE1:def 2 ( Free H = {} implies ( M1 |= H iff M2 |= H ) )
assume A2:
Free H = {}
; ( M1 |= H iff M2 |= H )
thus
( M1 |= H implies M2 |= H )
( M2 |= H implies M1 |= H )proof
assume A3:
for
v1 being
Function of
VAR,
M1 holds
M1,
v1 |= H
;
ZF_MODEL:def 5 M2 |= H
set v1 = the
Function of
VAR,
M1;
M1, the
Function of
VAR,
M1 |= H
by A3;
then A4:
M2,
M2 ! the
Function of
VAR,
M1 |= H
by A1;
let v2 be
Function of
VAR,
M2;
ZF_MODEL:def 5 M2,v2 |= H
for
x being
Variable st
x in Free H holds
v2 . x = (M2 ! the Function of VAR,M1) . x
by A2;
hence
M2,
v2 |= H
by A4, ZF_LANG1:75;
verum
end;
assume A5:
for v2 being Function of VAR,M2 holds M2,v2 |= H
; ZF_MODEL:def 5 M1 |= H
let v1 be Function of VAR,M1; ZF_MODEL:def 5 M1,v1 |= H
M2,M2 ! v1 |= H
by A5;
hence
M1,v1 |= H
by A1; verum