defpred S1[ object , object ] means ex S being non empty non void strict ManySortedSign st
( S = $2 & $1 = [ the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S] );
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 )
assume
(
S1[
x,
y] &
S1[
x,
z] )
;
y = z
then consider S1,
S2 being non
empty non
void strict ManySortedSign such that A2:
S1 = y
and A3:
x = [ the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1]
and A4:
S2 = z
and A5:
x = [ the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2]
and
(
S2 is
empty implies
S2 is
void )
;
A6:
the
Arity of
S1 = the
Arity of
S2
by A3, A5, XTUPLE_0:5;
( the
carrier of
S1 = the
carrier of
S2 & the
carrier' of
S1 = the
carrier' of
S2 )
by A3, A5, XTUPLE_0:5;
hence
y = z
by A2, A3, A4, A5, A6, XTUPLE_0:5;
verum
end;
consider X being set such that
A7:
for x being object holds
( x in X iff ex y being object st
( y in [:(bool A),(bool A),(PFuncs (A,(A *))),(PFuncs (A,A)):] & S1[y,x] ) )
from TARSKI:sch 1(A1);
take
X
; for x being object holds
( x in X iff ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A ) )
let x be object ; ( x in X iff ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A ) )
thus
( x in X iff ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A ) )
verumproof
thus
(
x in X implies ex
S being non
empty non
void strict ManySortedSign st
(
x = S & the
carrier of
S c= A & the
carrier' of
S c= A ) )
( ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A ) implies x in X )proof
assume
x in X
;
ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A )
then consider y being
object such that A8:
y in [:(bool A),(bool A),(PFuncs (A,(A *))),(PFuncs (A,A)):]
and A9:
S1[
y,
x]
by A7;
consider S being non
empty non
void strict ManySortedSign such that A10:
S = x
and
y = [ the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S]
by A9;
take
S
;
( x = S & the carrier of S c= A & the carrier' of S c= A )
( the
carrier of
S in bool A & the
carrier' of
S in bool A )
by A8, A9, A10, MCART_1:80;
hence
(
x = S & the
carrier of
S c= A & the
carrier' of
S c= A )
by A10;
verum
end;
given S being non
empty non
void strict ManySortedSign such that A11:
x = S
and A12:
the
carrier of
S c= A
and A13:
the
carrier' of
S c= A
;
x in X
(
dom the
ResultSort of
S = the
carrier' of
S &
rng the
ResultSort of
S c= A )
by A12, FUNCT_2:def 1;
then A14:
the
ResultSort of
S in PFuncs (
A,
A)
by A13, PARTFUN1:def 3;
reconsider C = the
carrier of
S as
Subset of
A by A12;
consider y being
set such that A15:
y = [ the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S]
;
C * c= A *
by MSUHOM_1:2;
then A16:
rng the
Arity of
S c= A *
;
dom the
Arity of
S c= A
by A13;
then
the
Arity of
S in PFuncs (
A,
(A *))
by A16, PARTFUN1:def 3;
then
y in [:(bool A),(bool A),(PFuncs (A,(A *))),(PFuncs (A,A)):]
by A12, A13, A15, A14, MCART_1:80;
hence
x in X
by A7, A11, A15;
verum
end;