defpred S1[ object , object ] means for c being Element of F1()
for t being Element of F2() st $1 = [c,t] holds
( ( P1[c,t] implies $2 = F4(c,t) ) & ( P2[c,t] implies $2 = F5(c,t) ) & ( P3[c,t] implies $2 = F6(c,t) ) );
defpred S2[ object ] means for c being Element of F1()
for d being Element of F2() holds
( not $1 = [c,d] or P1[c,d] or P2[c,d] or P3[c,d] );
consider T being set such that
A2:
for z being object holds
( z in T iff ( z in [:F1(),F2():] & S2[z] ) )
from XBOOLE_0:sch 1();
A3:
for x1 being object st x1 in T holds
ex z being object st S1[x1,z]
proof
let x1 be
object ;
( x1 in T implies ex z being object st S1[x1,z] )
assume A4:
x1 in T
;
ex z being object st S1[x1,z]
then
x1 in [:F1(),F2():]
by A2;
then consider q9,
w9 being
object such that A5:
q9 in F1()
and A6:
w9 in F2()
and A7:
x1 = [q9,w9]
by ZFMISC_1:def 2;
reconsider w9 =
w9 as
Element of
F2()
by A6;
reconsider q9 =
q9 as
Element of
F1()
by A5;
now ex z being Element of F3() st
for c being Element of F1()
for d being Element of F2() st x1 = [c,d] holds
( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) )per cases
( P1[q9,w9] or P2[q9,w9] or P3[q9,w9] )
by A2, A4, A7;
suppose A8:
P1[
q9,
w9]
;
ex z being Element of F3() st
for c being Element of F1()
for d being Element of F2() st x1 = [c,d] holds
( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) )take z =
F4(
q9,
w9);
for c being Element of F1()
for d being Element of F2() st x1 = [c,d] holds
( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) )let c be
Element of
F1();
for d being Element of F2() st x1 = [c,d] holds
( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) )let d be
Element of
F2();
( x1 = [c,d] implies ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) ) )assume
x1 = [c,d]
;
( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) )then
(
q9 = c &
w9 = d )
by A7, XTUPLE_0:1;
hence
( (
P1[
c,
d] implies
z = F4(
c,
d) ) & (
P2[
c,
d] implies
z = F5(
c,
d) ) & (
P3[
c,
d] implies
z = F6(
c,
d) ) )
by A1, A8;
verum end; suppose A9:
P2[
q9,
w9]
;
ex z being Element of F3() st
for c being Element of F1()
for d being Element of F2() st x1 = [c,d] holds
( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) )take z =
F5(
q9,
w9);
for c being Element of F1()
for d being Element of F2() st x1 = [c,d] holds
( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) )let c be
Element of
F1();
for d being Element of F2() st x1 = [c,d] holds
( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) )let d be
Element of
F2();
( x1 = [c,d] implies ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) ) )assume
x1 = [c,d]
;
( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) )then
(
q9 = c &
w9 = d )
by A7, XTUPLE_0:1;
hence
( (
P1[
c,
d] implies
z = F4(
c,
d) ) & (
P2[
c,
d] implies
z = F5(
c,
d) ) & (
P3[
c,
d] implies
z = F6(
c,
d) ) )
by A1, A9;
verum end; suppose A10:
P3[
q9,
w9]
;
ex z being Element of F3() st
for c being Element of F1()
for d being Element of F2() st x1 = [c,d] holds
( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) )take z =
F6(
q9,
w9);
for c being Element of F1()
for d being Element of F2() st x1 = [c,d] holds
( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) )let c be
Element of
F1();
for d being Element of F2() st x1 = [c,d] holds
( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) )let d be
Element of
F2();
( x1 = [c,d] implies ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) ) )assume
x1 = [c,d]
;
( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) )then
(
q9 = c &
w9 = d )
by A7, XTUPLE_0:1;
hence
( (
P1[
c,
d] implies
z = F4(
c,
d) ) & (
P2[
c,
d] implies
z = F5(
c,
d) ) & (
P3[
c,
d] implies
z = F6(
c,
d) ) )
by A1, A10;
verum end; end; end;
hence
ex
z being
object st
S1[
x1,
z]
;
verum
end;
consider f being Function such that
A11:
( dom f = T & ( for z being object st z in T holds
S1[z,f . z] ) )
from CLASSES1:sch 1(A3);
A12:
rng f c= F3()
T c= [:F1(),F2():]
by A2;
then reconsider f = f as PartFunc of [:F1(),F2():],F3() by A11, A12, RELSET_1:4;
take
f
; ( ( for c being Element of F1()
for d being Element of F2() holds
( [c,d] in dom f iff ( P1[c,d] or P2[c,d] or P3[c,d] ) ) ) & ( for c being Element of F1()
for r being Element of F2() st [c,r] in dom f holds
( ( P1[c,r] implies f . [c,r] = F4(c,r) ) & ( P2[c,r] implies f . [c,r] = F5(c,r) ) & ( P3[c,r] implies f . [c,r] = F6(c,r) ) ) ) )
thus
for c being Element of F1()
for d being Element of F2() holds
( [c,d] in dom f iff ( P1[c,d] or P2[c,d] or P3[c,d] ) )
for c being Element of F1()
for r being Element of F2() st [c,r] in dom f holds
( ( P1[c,r] implies f . [c,r] = F4(c,r) ) & ( P2[c,r] implies f . [c,r] = F5(c,r) ) & ( P3[c,r] implies f . [c,r] = F6(c,r) ) )proof
let c be
Element of
F1();
for d being Element of F2() holds
( [c,d] in dom f iff ( P1[c,d] or P2[c,d] or P3[c,d] ) )let d be
Element of
F2();
( [c,d] in dom f iff ( P1[c,d] or P2[c,d] or P3[c,d] ) )
thus
( not
[c,d] in dom f or
P1[
c,
d] or
P2[
c,
d] or
P3[
c,
d] )
by A2, A11;
( ( P1[c,d] or P2[c,d] or P3[c,d] ) implies [c,d] in dom f )
assume A18:
(
P1[
c,
d] or
P2[
c,
d] or
P3[
c,
d] )
;
[c,d] in dom f
A19:
now for i9 being Element of F1()
for o9 being Element of F2() holds
( not [c,d] = [i9,o9] or P1[i9,o9] or P2[i9,o9] or P3[i9,o9] )let i9 be
Element of
F1();
for o9 being Element of F2() holds
( not [c,d] = [i9,o9] or P1[i9,o9] or P2[i9,o9] or P3[i9,o9] )let o9 be
Element of
F2();
( not [c,d] = [i9,o9] or P1[i9,o9] or P2[i9,o9] or P3[i9,o9] )assume A20:
[c,d] = [i9,o9]
;
( P1[i9,o9] or P2[i9,o9] or P3[i9,o9] )then
c = i9
by XTUPLE_0:1;
hence
(
P1[
i9,
o9] or
P2[
i9,
o9] or
P3[
i9,
o9] )
by A18, A20, XTUPLE_0:1;
verum end;
[c,d] in [:F1(),F2():]
by ZFMISC_1:87;
hence
[c,d] in dom f
by A2, A11, A19;
verum
end;
let c be Element of F1(); for r being Element of F2() st [c,r] in dom f holds
( ( P1[c,r] implies f . [c,r] = F4(c,r) ) & ( P2[c,r] implies f . [c,r] = F5(c,r) ) & ( P3[c,r] implies f . [c,r] = F6(c,r) ) )
let d be Element of F2(); ( [c,d] in dom f implies ( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) & ( P3[c,d] implies f . [c,d] = F6(c,d) ) ) )
assume
[c,d] in dom f
; ( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) & ( P3[c,d] implies f . [c,d] = F6(c,d) ) )
hence
( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) & ( P3[c,d] implies f . [c,d] = F6(c,d) ) )
by A11; verum