defpred S1[ object , object ] means ex R being strict RelStr st
( $1 = [ the carrier of R, the InternalRel of R] & $2 = R );
A1:
for x, y, z being object st S1[x,y] & S1[x,z] holds
y = z
proof
let x,
y,
z be
object ;
( S1[x,y] & S1[x,z] implies y = z )
given R1 being
strict RelStr such that A2:
x = [ the carrier of R1, the InternalRel of R1]
and A3:
y = R1
;
( not S1[x,z] or y = z )
given R2 being
strict RelStr such that A4:
x = [ the carrier of R2, the InternalRel of R2]
and A5:
z = R2
;
y = z
the
carrier of
R1 = the
carrier of
R2
by A2, A4, XTUPLE_0:1;
hence
y = z
by A2, A3, A4, A5, XTUPLE_0:1;
verum
end;
consider X being set such that
A6:
for x being object holds
( x in X iff ex y being object st
( y in FinSETS & S1[y,x] ) )
from TARSKI:sch 1(A1);
take
X
; for X being object holds
( X in X iff ex R being strict RelStr st
( X = R & the carrier of R in FinSETS ) )
for x being object holds
( x in X iff ex R being strict RelStr st
( x = R & the carrier of R in FinSETS ) )
proof
let x be
object ;
( x in X iff ex R being strict RelStr st
( x = R & the carrier of R in FinSETS ) )
thus
(
x in X implies ex
R being
strict RelStr st
(
x = R & the
carrier of
R in FinSETS ) )
( ex R being strict RelStr st
( x = R & the carrier of R in FinSETS ) implies x in X )proof
assume
x in X
;
ex R being strict RelStr st
( x = R & the carrier of R in FinSETS )
then consider y being
object such that A7:
y in FinSETS
and A8:
ex
R being
strict RelStr st
(
y = [ the carrier of R, the InternalRel of R] &
x = R )
by A6;
consider R being
strict RelStr such that A9:
y = [ the carrier of R, the InternalRel of R]
and A10:
x = R
by A8;
A11:
{ the carrier of R} in {{ the carrier of R, the InternalRel of R},{ the carrier of R}}
by TARSKI:def 2;
{{ the carrier of R, the InternalRel of R},{ the carrier of R}} c= FinSETS
by A7, A9, ORDINAL1:def 2;
then A12:
{ the carrier of R} c= FinSETS
by A11, ORDINAL1:def 2;
the
carrier of
R in { the carrier of R}
by TARSKI:def 1;
hence
ex
R being
strict RelStr st
(
x = R & the
carrier of
R in FinSETS )
by A10, A12;
verum
end;
given R being
strict RelStr such that A13:
x = R
and A14:
the
carrier of
R in FinSETS
;
x in X
consider R being
strict RelStr such that A15:
x = R
and A16:
the
carrier of
R in FinSETS
by A13, A14;
the
InternalRel of
R in FinSETS
by A16, Th1;
then
[ the carrier of R, the InternalRel of R] in FinSETS
by A16, CLASSES2:58;
hence
x in X
by A6, A15;
verum
end;
hence
for X being object holds
( X in X iff ex R being strict RelStr st
( X = R & the carrier of R in FinSETS ) )
; verum