defpred S1[ set , set ] means ex M being strict feasible MSAlgebra of S st
( M = $2 & $1 = [ the Sorts of M, the Charact of M] );
A1:
for x, y, z being set st S1[x,y] & S1[x,z] holds
y = z
proof
let x,
y,
z be
set ;
( S1[x,y] & S1[x,z] implies y = z )
given M being
strict feasible MSAlgebra of
S such that A2:
M = y
and A3:
x = [ the Sorts of M, the Charact of M]
;
( not S1[x,z] or y = z )
given N being
strict feasible MSAlgebra of
S such that A4:
N = z
and A5:
x = [ the Sorts of N, the Charact of N]
;
y = z
the
Sorts of
M = the
Sorts of
N
by A3, A5, ZFMISC_1:33;
hence
y = z
by A2, A3, A4, A5, ZFMISC_1:33;
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 [:(Funcs ( the carrier of S,(bool A))),(Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A)))):] & S1[y,x] ) )
from TARSKI:sch 1(A1);
take
X
; for x being set holds
( x in X iff ex M being strict feasible MSAlgebra of S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) )
thus
for x being set holds
( x in X iff ex M being strict feasible MSAlgebra of S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) )
verumproof
let x be
set ;
( x in X iff ex M being strict feasible MSAlgebra of S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) )
given M being
strict feasible MSAlgebra of
S such that A13:
x = M
and A14:
for
C being
Component of the
Sorts of
M holds
C c= A
;
x in X
A15:
dom the
Sorts of
M = the
carrier of
S
by PARTFUN1:def 4;
then reconsider SM = the
Sorts of
M as
Function of the
carrier of
S,
(rng the Sorts of M) by FUNCT_2:3;
A16:
rng the
Sorts of
M c= bool A
then reconsider SM9 =
SM as
Function of the
carrier of
S,
(bool A) by FUNCT_2:8;
consider y being
set such that A17:
y = [ the Sorts of M, the Charact of M]
;
A18:
dom the
Charact of
M = the
carrier' of
S
by PARTFUN1:def 4;
rng the
Charact of
M c= PFuncs (
(PFuncs (NAT,A)),
A)
proof
reconsider SA =
( the Sorts of M #) * the
Arity of
S,
SR = the
Sorts of
M * the
ResultSort of
S as
ManySortedSet of the
carrier' of
S ;
let x be
set ;
TARSKI:def 3 ( not x in rng the Charact of M or x in PFuncs ((PFuncs (NAT,A)),A) )
reconsider CM = the
Charact of
M as
ManySortedFunction of
SA,
SR ;
assume
x in rng the
Charact of
M
;
x in PFuncs ((PFuncs (NAT,A)),A)
then consider x1 being
set such that A19:
x1 in dom the
Charact of
M
and A20:
x = the
Charact of
M . x1
by FUNCT_1:def 5;
reconsider Cm =
CM . x1 as
Function of
(SA . x1),
(SR . x1) by A18, A19, PBOOLE:def 18;
A21:
x1 in the
carrier' of
S
by A19, PARTFUN1:def 4;
A22:
x1 in dom SA
by A18, A19, PARTFUN1:def 4;
SA . x1 c= PFuncs (
NAT,
A)
then A30:
dom Cm c= PFuncs (
NAT,
A)
by XBOOLE_1:1;
x1 in dom SR
by A18, A19, PARTFUN1:def 4;
then A31:
SR . x1 = the
Sorts of
M . ( the ResultSort of S . x1)
by FUNCT_1:22;
the
ResultSort of
S . x1 in the
carrier of
S
by A18, A19, FUNCT_2:7;
then
SR . x1 in rng the
Sorts of
M
by A15, A31, FUNCT_1:def 5;
then
rng Cm c= A
by A16, XBOOLE_1:1;
hence
x in PFuncs (
(PFuncs (NAT,A)),
A)
by A20, A30, PARTFUN1:def 5;
verum
end;
then
(
SM9 in Funcs ( the
carrier of
S,
(bool A)) & the
Charact of
M in Funcs ( the
carrier' of
S,
(PFuncs ((PFuncs (NAT,A)),A))) )
by A18, FUNCT_2:11, FUNCT_2:def 2;
then
y in [:(Funcs ( the carrier of S,(bool A))),(Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A)))):]
by A17, ZFMISC_1:106;
hence
x in X
by A6, A13, A17;
verum
end;