defpred S1[ object , object ] means ex p being QC-formula of A ex Sub being CQC_Substitution of A st
( $1 = [p,Sub] & p,Sub PQSub $2 );
A1:
for a, b1, b2 being object st S1[a,b1] & S1[a,b2] holds
b1 = b2
proof
let a,
b1,
b2 be
object ;
( S1[a,b1] & S1[a,b2] implies b1 = b2 )
assume that A2:
ex
p being
QC-formula of
A ex
Sub being
CQC_Substitution of
A st
(
a = [p,Sub] &
p,
Sub PQSub b1 )
and A3:
ex
p being
QC-formula of
A ex
Sub being
CQC_Substitution of
A st
(
a = [p,Sub] &
p,
Sub PQSub b2 )
;
b1 = b2
consider p1 being
QC-formula of
A,
Sub1 being
CQC_Substitution of
A such that A4:
a = [p1,Sub1]
and A5:
p1,
Sub1 PQSub b1
by A2;
consider p2 being
QC-formula of
A,
Sub2 being
CQC_Substitution of
A such that A6:
a = [p2,Sub2]
and A7:
p2,
Sub2 PQSub b2
by A3;
A8:
p1 = p2
by A4, A6, XTUPLE_0:1;
A9:
Sub1 = Sub2
by A4, A6, XTUPLE_0:1;
end;
consider f being Function such that
A12:
for a, b being object holds
( [a,b] in f iff ( a in [:(QC-WFF A),(vSUB A):] & S1[a,b] ) )
from FUNCT_1:sch 1(A1);
take
f
; for a being object holds
( a in f iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being object st
( a = [[p,Sub],b] & p,Sub PQSub b ) )
for c being object holds
( c in f iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being object st
( c = [[p,Sub],b] & p,Sub PQSub b ) )
proof
let c be
object ;
( c in f iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being object st
( c = [[p,Sub],b] & p,Sub PQSub b ) )
thus
(
c in f implies ex
p being
QC-formula of
A ex
Sub being
CQC_Substitution of
A ex
b being
object st
(
c = [[p,Sub],b] &
p,
Sub PQSub b ) )
( ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being object st
( c = [[p,Sub],b] & p,Sub PQSub b ) implies c in f )proof
assume A13:
c in f
;
ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being object st
( c = [[p,Sub],b] & p,Sub PQSub b )
then consider a,
b being
object such that A14:
c = [a,b]
by RELAT_1:def 1;
ex
p being
QC-formula of
A ex
Sub being
CQC_Substitution of
A st
(
a = [p,Sub] &
p,
Sub PQSub b )
by A12, A13, A14;
hence
ex
p being
QC-formula of
A ex
Sub being
CQC_Substitution of
A ex
b being
object st
(
c = [[p,Sub],b] &
p,
Sub PQSub b )
by A14;
verum
end;
thus
( ex
p being
QC-formula of
A ex
Sub being
CQC_Substitution of
A ex
b being
object st
(
c = [[p,Sub],b] &
p,
Sub PQSub b ) implies
c in f )
by A12;
verum
end;
hence
for a being object holds
( a in f iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being object st
( a = [[p,Sub],b] & p,Sub PQSub b ) )
; verum