defpred S3[ object , object , object ] means for p, q being PartialPredicate of D st $1 = p & $2 = q holds
for f being Function st f = $3 holds
( dom f = H1(p,q) & ( for d being object holds
( ( ( S1[d,p] or S1[d,q] ) implies f . d = TRUE ) & ( S2[d,p,q] implies f . d = FALSE ) ) ) );
A1:
for x1, x2 being object st x1 in Pr D & x2 in Pr D holds
ex y being object st
( y in Pr D & S3[x1,x2,y] )
proof
let x1,
x2 be
object ;
( x1 in Pr D & x2 in Pr D implies ex y being object st
( y in Pr D & S3[x1,x2,y] ) )
assume
(
x1 in Pr D &
x2 in Pr D )
;
ex y being object st
( y in Pr D & S3[x1,x2,y] )
then reconsider X1 =
x1,
X2 =
x2 as
PartFunc of
D,
BOOLEAN by PARTFUN1:46;
defpred S4[
object ,
object ]
means for
d being
Element of
D st
d = $1 holds
( ( (
S1[
d,
X1] or
S1[
d,
X2] ) implies $2
= TRUE ) & (
S2[
d,
X1,
X2] implies $2
= FALSE ) );
A2:
for
a being
object st
a in H1(
X1,
X2) holds
ex
b being
object st
(
b in BOOLEAN &
S4[
a,
b] )
proof
let a be
object ;
( a in H1(X1,X2) implies ex b being object st
( b in BOOLEAN & S4[a,b] ) )
assume
a in H1(
X1,
X2)
;
ex b being object st
( b in BOOLEAN & S4[a,b] )
then consider d being
Element of
D such that A3:
d = a
and A4:
(
S1[
d,
X1] or
S1[
d,
X2] or
S2[
d,
X1,
X2] )
;
per cases
( S1[d,X1] or S1[d,X2] or S2[d,X1,X2] )
by A4;
end;
end;
consider g being
Function such that A7:
dom g = H1(
X1,
X2)
and A8:
rng g c= BOOLEAN
and A9:
for
x being
object st
x in H1(
X1,
X2) holds
S4[
x,
g . x]
from FUNCT_1:sch 6(A2);
take
g
;
( g in Pr D & S3[x1,x2,g] )
H1(
X1,
X2)
c= D
proof
let x be
object ;
TARSKI:def 3 ( not x in H1(X1,X2) or x in D )
assume
x in H1(
X1,
X2)
;
x in D
then
ex
d being
Element of
D st
(
d = x & (
S1[
d,
X1] or
S1[
d,
X2] or
S2[
d,
X1,
X2] ) )
;
hence
x in D
;
verum
end;
then
g is
PartFunc of
D,
BOOLEAN
by A7, A8, RELSET_1:4;
hence
g in Pr D
by PARTFUN1:45;
S3[x1,x2,g]
let p,
q be
PartialPredicate of
D;
( x1 = p & x2 = q implies for f being Function st f = g holds
( dom f = H1(p,q) & ( for d being object holds
( ( ( S1[d,p] or S1[d,q] ) implies f . d = TRUE ) & ( S2[d,p,q] implies f . d = FALSE ) ) ) ) )
assume A10:
(
x1 = p &
x2 = q )
;
for f being Function st f = g holds
( dom f = H1(p,q) & ( for d being object holds
( ( ( S1[d,p] or S1[d,q] ) implies f . d = TRUE ) & ( S2[d,p,q] implies f . d = FALSE ) ) ) )
let f be
Function;
( f = g implies ( dom f = H1(p,q) & ( for d being object holds
( ( ( S1[d,p] or S1[d,q] ) implies f . d = TRUE ) & ( S2[d,p,q] implies f . d = FALSE ) ) ) ) )
assume A11:
f = g
;
( dom f = H1(p,q) & ( for d being object holds
( ( ( S1[d,p] or S1[d,q] ) implies f . d = TRUE ) & ( S2[d,p,q] implies f . d = FALSE ) ) ) )
thus
dom f = H1(
p,
q)
by A7, A10, A11;
for d being object holds
( ( ( S1[d,p] or S1[d,q] ) implies f . d = TRUE ) & ( S2[d,p,q] implies f . d = FALSE ) )
let d be
object ;
( ( ( S1[d,p] or S1[d,q] ) implies f . d = TRUE ) & ( S2[d,p,q] implies f . d = FALSE ) )
hereby ( S2[d,p,q] implies f . d = FALSE )
end;
assume A14:
S2[
d,
p,
q]
;
f . d = FALSE
then
d in dom p
;
then A15:
d is
Element of
D
;
then
d in H1(
X1,
X2)
by A10, A14;
hence
f . d = FALSE
by A9, A10, A11, A14, A15;
verum
end;
consider F being Function of [:(Pr D),(Pr D):],(Pr D) such that
A16:
for x, y being object st x in Pr D & y in Pr D holds
S3[x,y,F . (x,y)]
from BINOP_1:sch 1(A1);
take
F
; for p, q being PartialPredicate of D holds
( dom (F . (p,q)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE ) ) } & ( for d being object holds
( ( ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) ) implies (F . (p,q)) . d = TRUE ) & ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE implies (F . (p,q)) . d = FALSE ) ) ) )
let p, q be PartialPredicate of D; ( dom (F . (p,q)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE ) ) } & ( for d being object holds
( ( ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) ) implies (F . (p,q)) . d = TRUE ) & ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE implies (F . (p,q)) . d = FALSE ) ) ) )
( p in Pr D & q in Pr D )
by PARTFUN1:45;
hence
( dom (F . (p,q)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE ) ) } & ( for d being object holds
( ( ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) ) implies (F . (p,q)) . d = TRUE ) & ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE implies (F . (p,q)) . d = FALSE ) ) ) )
by A16; verum