xfamily.miz
begin
scheme ::
XFAMILY:sch1
Separation { A() ->
set , P[
object] } :
ex X be
set st for x be
set holds x
in X iff x
in A() & P[x];
defpred
Q[
object,
object] means $1
= $2 & P[$2];
A1: for x,y,z be
object st
Q[x, y] &
Q[x, z] holds y
= z;
consider X be
set such that
A2: for x be
object holds x
in X iff ex y be
object st y
in A() &
Q[y, x] from
TARSKI:sch 1(
A1);
take X;
let x be
set;
thus x
in X implies x
in A() & P[x]
proof
assume x
in X;
then ex y be
object st y
in A() &
Q[y, x] by
A2;
hence thesis;
end;
assume x
in A() & P[x];
then ex y be
object st y
in A() &
Q[y, x];
hence x
in X by
A2;
end;
scheme ::
XFAMILY:sch2
Extensionality { X,Y() ->
set , P[
set] } :
X()
= Y()
provided
A1: for x be
set holds x
in X() iff P[x]
and
A2: for x be
set holds x
in Y() iff P[x];
A3: for x be
object holds x
in Y() implies x
in X()
proof
let x be
object;
reconsider x as
set by
TARSKI: 1;
x
in Y() implies x
in X() by
A1,
A2;
hence thesis;
end;
for x be
object holds x
in X() implies x
in Y()
proof
let x be
object;
reconsider x as
set by
TARSKI: 1;
x
in X() implies x
in Y() by
A1,
A2;
hence thesis;
end;
hence thesis by
A3,
TARSKI: 2;
end;
scheme ::
XFAMILY:sch3
SetEq { P[
set] } :
for X1,X2 be
set st (for x be
set holds x
in X1 iff P[x]) & (for x be
set holds x
in X2 iff P[x]) holds X1
= X2;
let X1,X2 be
set such that
A1: for x be
set holds x
in X1 iff P[x] and
A2: for x be
set holds x
in X2 iff P[x];
thus thesis from
Extensionality(
A1,
A2);
end;
definition
let x be
object;
:: original:
`1
redefine
func x
`1 ->
set ;
coherence by
TARSKI: 1;
:: original:
`2
redefine
func x
`2 ->
set ;
coherence by
TARSKI: 1;
end
definition
let x be
object;
:: original:
`1_3
redefine
func x
`1_3 ->
set ;
coherence by
TARSKI: 1;
:: original:
`2_3
redefine
func x
`2_3 ->
set ;
coherence by
TARSKI: 1;
end
definition
let x be
object;
:: original:
`1_4
redefine
func x
`1_4 ->
set ;
coherence by
TARSKI: 1;
:: original:
`2_4
redefine
func x
`2_4 ->
set ;
coherence by
TARSKI: 1;
end