defpred S1[ set , set ] means ex R being strict RelStr st
( $1 = [the carrier of R,the InternalRel of R] & $2 = R );
A1:
for x, y, z being set st S1[x,y] & S1[x,z] holds
y = z
proof
let x,
y,
z be
set ;
:: thesis: ( 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
;
:: thesis: ( 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
;
:: thesis: y = z
( the
carrier of
R1 = the
carrier of
R2 & the
InternalRel of
R1 = the
InternalRel of
R2 )
by A2, A4, ZFMISC_1:33;
hence
y = z
by A3, A5;
:: thesis: verum
end;
consider X being set such that
A6:
for x being set holds
( x in X iff ex y being set st
( y in FinSETS & S1[y,x] ) )
from TARSKI:sch 1(A1);
take
X
; :: thesis: for X being set holds
( X in X iff ex R being strict RelStr st
( X = R & the carrier of R in FinSETS ) )
for x being set holds
( x in X iff ex R being strict RelStr st
( x = R & the carrier of R in FinSETS ) )
proof
let x be
set ;
:: thesis: ( 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 ) )
:: thesis: ( ex R being strict RelStr st
( x = R & the carrier of R in FinSETS ) implies x in X )proof
assume
x in X
;
:: thesis: ex R being strict RelStr st
( x = R & the carrier of R in FinSETS )
then consider y being
set such that A7:
(
y in FinSETS & 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 A8:
(
y = [the carrier of R,the InternalRel of R] &
x = R )
by A7;
A9:
{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, A8, ORDINAL1:def 2;
then A10:
{the carrier of R} c= FinSETS
by A9, 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 A8, A10;
:: thesis: verum
end;
given R being
strict RelStr such that A11:
(
x = R & the
carrier of
R in FinSETS )
;
:: thesis: x in X
consider R being
strict RelStr such that A12:
(
x = R & the
carrier of
R in FinSETS )
by A11;
the
InternalRel of
R in FinSETS
by A12, Th1;
then
[the carrier of R,the InternalRel of R] in FinSETS
by A12, CLASSES2:64;
hence
x in X
by A6, A12;
:: thesis: verum
end;
hence
for X being set holds
( X in X iff ex R being strict RelStr st
( X = R & the carrier of R in FinSETS ) )
; :: thesis: verum