Copyright (c) 1990 Association of Mizar Users
environ
vocabulary NAT_1, SEQ_1, SEQM_3, FUNCT_1, RELAT_1, ORDINAL2, ARYTM_3, ARYTM_1,
PARTFUN1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, NAT_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, SEQ_1,
SEQM_3;
constructors NAT_1, SEQ_1, SEQM_3, PARTFUN1, MEMBERED, XBOOLE_0;
clusters RELSET_1, XREAL_0, SEQM_3, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0,
NUMBERS, ORDINAL2;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0;
theorems ZFMISC_1, REAL_1, NAT_1, FUNCT_1, FUNCT_2, SEQM_3, PARTFUN1,
RELSET_1, XBOOLE_1, XCMPLX_1;
schemes NAT_1, FUNCT_2, RECDEF_1, SETWISEO, ZFREFLE1, XBOOLE_0;
begin
reserve x,y,z for set;
reserve n,m,k for Nat;
reserve r for Real;
theorem
for n ex m st n = 2*m or n = 2*m+1
proof let n;
A1: n = 2*(n div 2) + (n mod 2) by NAT_1:47;
take n div 2; set k = n mod 2;
k = 0 or k = 1
proof k < 1 + 1 by NAT_1:46; then A2: k <= 0 + 1 by NAT_1:38;
now per cases by A2,NAT_1:26;
suppose k <= 0; hence thesis by NAT_1:18;
suppose k = 0 + 1; hence thesis;
end; hence thesis;
end;
hence thesis by A1;
end;
theorem Th2:
for n ex m st n = 3*m or n = 3*m+1 or n = 3*m+2
proof let n;
A1: n = 3*(n div 3) + (n mod 3) by NAT_1:47;
take n div 3; set w = n mod 3;
A2: w = 0 or w = 1 or w = 2
proof w < 2 + 1 by NAT_1:46; then A3: w <= 1 + 1 by NAT_1:38;
now per cases by A3,NAT_1:26;
suppose A4: w <= 1;
now per cases by A4,NAT_1:26;
suppose w <= 0; hence thesis by NAT_1:18;
suppose w = 0 + 1; hence thesis;
end; hence thesis;
suppose w = 1 + 1; hence thesis;
end; hence thesis;
end;
now per cases by A2;
suppose w = 0; hence thesis by A1;
suppose w = 1; hence thesis by NAT_1:47;
suppose w = 2; hence thesis by NAT_1:47;
end; hence thesis;
end;
theorem Th3:
for n ex m st n = 4*m or n = 4*m+1 or n = 4*m+2 or n = 4*m+3
proof let n;
A1: n = 4*(n div 4) + (n mod 4) by NAT_1:47;
take n div 4; set o = n mod 4;
o = 0 or o = 1 or o = 2 or o = 3
proof o < 3 + 1 by NAT_1:46; then A2: o <= 2 + 1 by NAT_1:38;
now per cases by A2,NAT_1:26;
suppose A3: o <= 2;
now per cases by A3,NAT_1:26;
suppose A4: o <= 1;
now per cases by A4,NAT_1:26;
suppose o <= 0; hence thesis by NAT_1:18;
suppose o = 0 + 1; hence thesis;
end; hence thesis;
suppose o = 1 + 1; hence thesis;
end; hence thesis;
suppose o = 2 + 1; hence thesis;
end; hence thesis;
end;
hence thesis by A1;
end;
theorem Th4:
for n ex m st n = 5*m or n = 5*m+1 or n = 5*m+2 or n = 5*m+3 or n = 5*m+4
proof let n;
A1: n = 5*(n div 5) + (n mod 5) by NAT_1:47;
take n div 5; set l = n mod 5;
l = 0 or l = 1 or l = 2 or l = 3 or l = 4
proof l < 4 + 1 by NAT_1:46; then A2: l <= 3 + 1 by NAT_1:38;
now per cases by A2,NAT_1:26;
suppose A3: l <= 3;
now per cases by A3,NAT_1:26;
suppose A4: l <= 2;
now per cases by A4,NAT_1:26;
suppose A5: l <= 1;
now per cases by A5,NAT_1:26;
suppose l <= 0; hence thesis by NAT_1:18;
suppose l = 0 + 1; hence thesis;
end; hence thesis;
suppose l = 1 + 1; hence thesis;
end; hence thesis;
suppose l = 2 + 1; hence thesis;
end; hence thesis;
suppose l = 3 + 1; hence thesis;
end; hence thesis;
end;
hence thesis by A1;
end;
scheme ExRealSubseq{s()->Real_Sequence,P[set]}:
ex q being Real_Sequence st
q is_subsequence_of s() & (for n holds P[q.n]) &
for n st (for r st r = s().n holds P[r]) ex m st s().n = q.m
provided
A1: for n ex m st n <= m & P[s().m]
proof defpred X[set] means P[s().$1];
consider m1 be Nat such that
A2: 0 <= m1 & P[s().m1] by A1;
A3: ex m st X[m] by A2;
consider M be Nat such that
A4: X[M] & for n st X[n] holds M <= n from Min(A3);
A5: now let n; consider m such that
A6: n + 1 <= m & P[s().m] by A1;
take m; thus n < m & P[s().m] by A6,NAT_1:38;
end;
defpred P[set,set] means for n,m st $1 = n & $2 = m holds
n < m & P[s().m] & for k st n < k & P[s().k] holds m <= k;
defpred X[set,set,set] means P[$2,$3];
A7: for n for x be Element of NAT ex y be Element of NAT st X[n,x,y]
proof let n; let x be Element of NAT;
defpred X[Element of NAT] means x < $1 & P[s().$1];
A8: ex m st X[m] by A5; consider l be Nat such that
A9: X[l] & for k st X[k] holds l <= k from Min(A8);
take l; thus thesis by A9;
end;
reconsider M' = M as Element of NAT qua non empty set;
consider F be Function of NAT,NAT such that
A10: F.0 = M' &
for n be Element of NAT holds X[n,F.n,F.(n+1)] from RecExD(A7);
A11: dom F = NAT & rng F c= NAT by FUNCT_2:def 1;
rng F c= REAL by XBOOLE_1:1;
then reconsider F as Real_Sequence by A11,FUNCT_2:def 1,RELSET_1:11;
A12: now let n; F.n in rng F by A11,FUNCT_1:def 5;hence F.n is Nat by A11;
end;
now let n;
F.n is Nat & F.(n+1) is Nat by A12;
hence F.n < F.(n+1) by A10;
end;
then reconsider F as increasing Seq_of_Nat by A11,SEQM_3:def 8,def 11;
take q = s()*F; thus q is_subsequence_of s() by SEQM_3:def 10;
defpred X[set] means P[q.$1];
A13: X[0] by A4,A10,SEQM_3:31;
A14: for k st X[k] holds X[k+1]
proof let k such that P[q.k]; P[F.k,F.(k+1)] by A10; then P[s().(F.(k+1))];
hence P[q.(k+1)] by SEQM_3:31;
end;
thus for n holds X[n] from Ind(A13,A14);
A15: for n st P[s().n] ex m st F.m = n
proof defpred X[set] means P[s().$1] & for m holds F.m <> $1;
assume A16: ex n st X[n];
consider M1 be Nat such that A17: X[M1] & for n st X[n] holds M1 <= n
from Min(A16);
defpred X[Element of NAT] means $1 < M1 & P[s().$1] & ex m st F.m = $1;
A18: ex n st X[n]
proof take M; A19: M <= M1 by A4,A17;
M <> M1 by A10,A17;
hence M < M1 by A19,REAL_1:def 5; thus P[s().M] by A4; take 0;
thus thesis by A10;
end;
A20: for n st X[n] holds n <= M1;
consider X be Nat such that
A21: X[X] & for n st X[n] holds n <= X from Max(A20,A18);
A22: for k st X < k & k < M1 holds not P[s().k]
proof given k such that A23: X < k & k < M1 & P[s().k];
now per cases;
suppose ex m st F.m = k; hence contradiction by A21,A23;
suppose for m holds F.m <> k;
hence contradiction by A17,A23;
end;
hence contradiction;
end;
consider m such that
A24: F.m = X by A21;
A25: X < F.(m+1) & P[s().(F.(m+1))] &
for k st X < k & P[s().k] holds F.(m+1) <= k by A10,A24;
A26: F.(m+1) <= M1 by A10,A17,A21,A24;
now assume F.(m+1) <> M1; then F.(m+1) < M1 by A26,REAL_1:def 5;
hence contradiction by A22,A25;
end;hence contradiction by A17;
end;
let n; assume for r st r = s().n holds P[r];
then P[s().n]; then consider m such that
A27: F.m = n by A15; take m;
thus s().n = q.m by A27,SEQM_3:31;
end;
scheme ExRealSeq2{F,G(set)->Real}:
ex s being Real_Sequence st for n holds s.(2*n) = F(n) & s.(2*n+1) = G(n)
proof defpred X[set] means ex m st $1 = 2*m;
consider N be Subset of NAT such that
A1: for n holds n in N iff X[n] from SubsetEx;
defpred X[set] means ex m st $1 = 2*m+1;
consider M be Subset of NAT such that
A2: for n holds n in M iff X[n] from SubsetEx;
defpred X[Element of NAT, set] means
($1 in N implies $2 = F($1/2)) & ($1 in M implies $2 = G(($1-1)/2));
A3: for n ex r st X[n,r]
proof let n;
now assume A4: n in N; take r = F(n/2);
now assume n in M; then A5: ex k st n = 2*k + 1 by A2;
consider m such that A6: n = 2*m by A1,A4;
n = 2*m + 0 by A6; hence contradiction by A5,NAT_1:43;
end; hence thesis;
end; hence thesis;
end;
consider f being Function of NAT,REAL such that
A7: for n holds X[n,f.n] from FuncExD(A3);
reconsider f as Real_Sequence;
take f;
let n; 2*n in N by A1;
hence f.(2*n) = F(2*n/2) by A7
.= F(n) by XCMPLX_1:90;
2*n + 1 in M by A2;
hence f.(2*n + 1) = G((2*n + 1 - 1)/2) by A7
.= G(2*n/2) by XCMPLX_1:26
.= G(n) by XCMPLX_1:90;
end;
scheme ExRealSeq3{F,G,H(set)->Real}:
ex s being Real_Sequence st
for n holds s.(3*n) = F(n) & s.(3*n+1) = G(n) & s.(3*n+2) = H(n)
proof defpred X[set] means ex m st $1 = 3*m;
consider E be Subset of NAT such that
A1: for n holds n in E iff X[n] from SubsetEx;
defpred X[set] means ex m st $1 = 3*m+1;
consider G be Subset of NAT such that
A2: for n holds n in G iff X[n] from SubsetEx;
defpred X[set] means ex m st $1 = 3*m+2;
consider K be Subset of NAT such that
A3: for n holds n in K iff X[n] from SubsetEx;
defpred X[Element of NAT, set] means
($1 in E implies $2 = F($1/3)) & ($1 in G implies $2 = G(($1-1)/3)) &
( $1 in K implies $2 = H(($1-2)/3));
A4: for n ex r st X[n,r]
proof let n; consider m such that
A5: n = 3*m or n = 3*m + 1 or n = 3*m + 2 by Th2;
now per cases by A5;
suppose A6: n = 3*m; take r = F(n/3); A7: n = 3*m + 0 by A6;
A8: now assume n in G;
then ex k st n = 3*k + 1 by A2; hence contradiction
by A7,NAT_1:43;
end;
now assume n in K; then ex k st n = 3*k + 2 by A3; hence
contradiction by A7,NAT_1:43;
end; hence thesis by A8;
suppose A9: n = 3*m + 1; take r = G((n-1)/3);
A10: now assume n in E; then consider k such that
A11: n = 3*k by A1; n = 3*k + 0 by A11; hence contradiction by A9,NAT_1:43
;
end;
now assume n in K; then ex k st n = 3*k + 2 by A3; hence
contradiction by A9,NAT_1:43;
end; hence thesis by A10;
suppose A12: n = 3*m + 2; take r = H((n-2)/3);
A13: now assume n in E; then consider k such that
A14: n = 3*k by A1; n = 3*k + 0 by A14; hence contradiction by A12,NAT_1:
43;
end;
now assume n in G; then ex k st n = 3*k + 1 by A2; hence
contradiction by A12,NAT_1:43;
end; hence thesis by A13;
end; hence thesis;
end;
consider f being Function of NAT,REAL such that
A15: for n holds X[n,f.n] from FuncExD(A4);
reconsider f as Real_Sequence; take f;
let n; 3*n in E by A1; hence f.(3*n) = F(3*n/3) by A15
.= F(n) by XCMPLX_1:90;
3*n+1 in G by A2; hence f.(3*n+1) = G((3*n + 1 - 1)/3) by A15
.= G(3*n/3) by XCMPLX_1:26
.= G(n) by XCMPLX_1:90;
3*n+2 in K by A3; hence f.(3*n+2) = H((3*n + 2 - 2)/3) by A15
.= H(3*n/3) by XCMPLX_1:26
.= H(n) by XCMPLX_1:90;
end;
scheme ExRealSeq4{F,G,H,I(set)->Real}:
ex s being Real_Sequence st for n holds
s.(4*n) = F(n) & s.(4*n+1) = G(n) & s.(4*n+2) = H(n) & s.(4*n+3) = I(n)
proof defpred X[set] means ex m st $1 = 4*m;
consider Q be Subset of NAT such that
A1: for n holds n in Q iff X[n] from SubsetEx;
defpred X[set] means ex m st $1 = 4*m+1;
consider R be Subset of NAT such that
A2: for n holds n in R iff X[n] from SubsetEx;
defpred X[set] means ex m st $1 = 4*m+2;
consider P be Subset of NAT such that
A3: for n holds n in P iff X[n] from SubsetEx;
defpred X[set] means ex m st $1 = 4*m+3;
consider L be Subset of NAT such that
A4: for n holds n in L iff X[n] from SubsetEx;
defpred X[Element of NAT, set] means
($1 in Q implies $2 = F($1/4)) & ($1 in R implies $2 = G(($1-1)/4)) &
( $1 in P implies $2 = H(($1-2)/4)) & ($1 in L implies $2 = I(($1-3)/4));
A5: for n ex r st X[n,r]
proof let n; consider m such that
A6: n = 4*m or n = 4*m + 1 or n = 4*m + 2 or n = 4*m + 3 by Th3;
now per cases by A6;
suppose A7: n = 4*m; take r=F(n/4); A8: n=4*m+0 by A7;
A9: now assume n in R; then ex k st n=4*k+1 by A2;
hence contradiction by A8,NAT_1:43;
end;
A10: now assume n in P; then ex k st n=4*k+2 by A3;
hence contradiction by A8,NAT_1:43;
end;
now assume n in L; then ex k st n=4*k+3 by A4;
hence contradiction by A8,NAT_1:43;
end; hence thesis by A9,A10;
suppose A11: n = 4*m + 1; take r=G((n-1)/4);
A12: now assume n in Q; then consider k such that A13: n=4*k by A1;
n=4*k+0 by A13; hence contradiction by A11,NAT_1:43;
end;
A14: now assume n in P; then ex k st n=4*k+2 by A3;
hence contradiction by A11,NAT_1:43;
end;
now assume n in L; then ex k st n=4*k+3 by A4;
hence contradiction by A11,NAT_1:43;
end; hence thesis by A12,A14;
suppose A15: n=4*m+2; take r=H((n-2)/4);
A16: now assume n in Q; then consider k such that A17: n=4*k by A1;
n=4*k+0 by A17; hence contradiction by A15,NAT_1:43;
end;
A18: now assume n in R; then ex k st n=4*k+1 by A2;
hence contradiction by A15,NAT_1:43;
end;
now assume n in L; then ex k st n=4*k+3 by A4;
hence contradiction by A15,NAT_1:43;
end; hence thesis by A16,A18;
suppose A19: n=4*m+3; take r=I((n-3)/4);
A20: now assume n in Q; then consider k such that A21: n=4*k by A1;
n=4*k+0 by A21; hence contradiction by A19,NAT_1:43;
end;
A22: now assume n in R; then ex k st n=4*k+1 by A2;
hence contradiction by A19,NAT_1:43;
end;
now assume n in P; then ex k st n=4*k+2 by A3;
hence contradiction by A19,NAT_1:43;
end; hence thesis by A20,A22;
end; hence thesis;
end;
consider f being Function of NAT,REAL such that
A23: for n holds X[n,f.n] from FuncExD(A5);
reconsider f as Real_Sequence; take f;
let n; 4*n in Q by A1; hence f.(4*n)=F(4*n/4) by A23
.= F(n) by XCMPLX_1:90;
4*n+1 in R by A2; hence f.(4*n+1)=G((4*n+1-1)/4) by A23
.= G(4*n/4) by XCMPLX_1:26
.= G(n) by XCMPLX_1:90;
4*n+2 in P by A3; hence f.(4*n+2)=H((4*n+2-2)/4) by A23
.= H(4*n/4) by XCMPLX_1:26
.= H(n) by XCMPLX_1:90;
4*n+3 in L by A4; hence f.(4*n+3)=I((4*n+3-3)/4) by A23
.= I(4*n/4) by XCMPLX_1:26
.= I(n) by XCMPLX_1:90;
end;
scheme ExRealSeq5{F,G,H,I,J(set)->Real}:
ex s being Real_Sequence st for n holds s.(5*n) = F(n) & s.(5*n+1) = G(n) &
s.(5*n+2) = H(n) & s.(5*n+3) = I(n) & s.(5*n+4) = J(n)
proof defpred X[set] means ex m st $1 = 5*m;
consider N be Subset of NAT such that
A1: for n holds n in N iff X[n] from SubsetEx;
defpred X[set] means ex m st $1 = 5*m+1;
consider M be Subset of NAT such that
A2: for n holds n in M iff X[n] from SubsetEx;
defpred X[set] means ex m st $1 = 5*m+2;
consider K be Subset of NAT such that
A3: for n holds n in K iff X[n] from SubsetEx;
defpred X[set] means ex m st $1 = 5*m+3;
consider L be Subset of NAT such that
A4: for n holds n in L iff X[n] from SubsetEx;
defpred X[set] means ex m st $1 = 5*m+4;
consider O be Subset of NAT such that
A5: for n holds n in O iff X[n] from SubsetEx;
defpred X[Element of NAT, set] means
($1 in N implies $2 = F($1/5)) & ($1 in M implies $2 = G(($1-1)/5)) &
( $1 in K implies $2 = H(($1-2)/5)) & ($1 in L implies $2 = I(($1-3)/5)) &
($1 in O implies $2=J(($1-4)/5));
A6: for n ex r st X[n,r]
proof let n; consider m such that
A7: n=5*m or n=5*m+1 or n=5*m+2 or n=5*m+3 or n=5*m+4 by Th4;
now per cases by A7;
suppose A8: n=5*m; take r=F(n/5); A9: n=5*m+0 by A8;
A10: now assume n in M; then ex k st n=5*k+1 by A2;
hence contradiction by A9,NAT_1:43;
end;
A11: now assume n in K; then ex k st n=5*k+2 by A3;
hence contradiction by A9,NAT_1:43;
end;
A12: now assume n in L; then ex k st n=5*k+3 by A4;
hence contradiction by A9,NAT_1:43;
end;
now assume n in O; then ex k st n=5*k+4 by A5;
hence contradiction by A9,NAT_1:43;
end; hence thesis by A10,A11,A12;
suppose A13: n=5*m+1; take r=G((n-1)/5);
A14: now assume n in N; then consider k such that A15: n=5*k by A1;
n=5*k+0 by A15; hence contradiction by A13,NAT_1:43;
end;
A16: now assume n in K; then ex k st n=5*k+2 by A3;
hence contradiction by A13,NAT_1:43;
end;
A17: now assume n in L; then ex k st n=5*k+3 by A4;
hence contradiction by A13,NAT_1:43;
end;
now assume n in O; then ex k st n=5*k+4 by A5;
hence contradiction by A13,NAT_1:43;
end; hence thesis by A14,A16,A17;
suppose A18: n=5*m+2; take r=H((n-2)/5);
A19: now assume n in N; then consider k such that A20: n=5*k by A1;
n=5*k+0 by A20; hence contradiction by A18,NAT_1:43;
end;
A21: now assume n in M; then ex k st n=5*k+1 by A2;
hence contradiction by A18,NAT_1:43;
end;
A22: now assume n in L; then ex k st n=5*k+3 by A4;
hence contradiction by A18,NAT_1:43;
end;
now assume n in O; then ex k st n=5*k+4 by A5;
hence contradiction by A18,NAT_1:43;
end; hence thesis by A19,A21,A22;
suppose A23: n=5*m+3; take r=I((n-3)/5);
A24: now assume n in N; then consider k such that A25: n=5*k by A1;
n=5*k+0 by A25; hence contradiction by A23,NAT_1:43;
end;
A26: now assume n in M; then ex k st n=5*k+1 by A2;
hence contradiction by A23,NAT_1:43;
end;
A27: now assume n in K; then ex k st n=5*k+2 by A3;
hence contradiction by A23,NAT_1:43;
end;
now assume n in O; then ex k st n=5*k+4 by A5;
hence contradiction by A23,NAT_1:43;
end; hence thesis by A24,A26,A27;
suppose A28: n=5*m+4; take r=J((n-4)/5);
A29: now assume n in N; then consider k such that A30: n=5*k by A1;
n=5*k+0 by A30; hence contradiction by A28,NAT_1:43;
end;
A31: now assume n in M; then ex k st n=5*k+1 by A2;
hence contradiction by A28,NAT_1:43;
end;
A32: now assume n in K; then ex k st n=5*k+2 by A3;
hence contradiction by A28,NAT_1:43;
end;
now assume n in L; then ex k st n=5*k+3 by A4;
hence contradiction by A28,NAT_1:43;
end; hence thesis by A29,A31,A32;
end; hence thesis;
end;
consider f being Function of NAT,REAL such that
A33: for n holds X[n,f.n] from FuncExD(A6);
reconsider f as Real_Sequence; take f;
let n; 5*n in N by A1;
hence f.(5*n) = F(5*n/5) by A33
.= F(n) by XCMPLX_1:90;
5*n+1 in M by A2;
hence f.(5*n+1) = G((5*n+1-1)/5) by A33
.= G(5*n/5) by XCMPLX_1:26
.= G(n) by XCMPLX_1:90;
5*n+2 in K by A3;
hence f.(5*n+2) = H((5*n+2-2)/5) by A33
.= H(5*n/5) by XCMPLX_1:26
.= H(n) by XCMPLX_1:90;
5*n+3 in L by A4;
hence f.(5*n+3) = I((5*n+3-3)/5) by A33
.= I(5*n/5) by XCMPLX_1:26
.= I(n) by XCMPLX_1:90;
5*n+4 in O by A5;
hence f.(5*n+4) = J((5*n+4-4)/5) by A33
.= J(5*n/5) by XCMPLX_1:26
.= J(n) by XCMPLX_1:90;
end;
scheme PartFuncExD2{C, D()->non empty set, P,Q[set],
F,G(set)->Element of D()}:
ex f being PartFunc of C(),D() st
(for c be Element of C() holds c in dom f iff P[c] or Q[c]) &
(for c be Element of C() st c in dom f holds
(P[c] implies f.c = F(c)) & (Q[c] implies f.c = G(c)))
provided
A1: for c be Element of C() st P[c] holds not Q[c]
proof defpred X[set] means P[$1] or Q[$1];
consider X be set such that
A2: for x holds x in X iff x in C() & X[x] from Separation;
A3: X c= C()
proof let x; assume x in X; hence x in C() by A2; end;
defpred X[set,set] means
(P[$1] implies $2 = F($1)) & (Q[$1] implies $2 = G($1));
A4: for x st x in X ex y st X[x,y]
proof let x; assume A5: x in X;
then reconsider x' = x as Element of C() by A2;
now per cases by A2,A5;
suppose A6: P[x]; take y = F(x); not Q[x'] by A1,A6; hence thesis;
suppose A7: Q[x]; take y = G(x); not P[x'] by A1,A7; hence thesis;
end; hence thesis;
end;
consider f being Function such that
A8: dom f = X & for x st x in X holds X[x,f.x] from NonUniqFuncEx(A4);
rng f c= D()
proof let x; assume x in rng f; then consider y such that
A9: y in dom f & x = f.y by FUNCT_1:def 5;
now per cases by A2,A8,A9;
suppose P[y]; then f.y = F(y) by A8,A9;
hence x in D() by A9;
suppose Q[y]; then f.y = G(y) by A8,A9;
hence x in D() by A9;
end; hence x in D();
end;
then reconsider q = f as PartFunc of C(),D() by A3,A8,RELSET_1:11; take q;
thus for c be Element of C() holds c in dom q iff P[c] or Q[c] by A2,A8;
let b be Element of C(); assume b in dom q;
hence thesis by A8;
end;
scheme PartFuncExD2'{C, D()->non empty set,P,Q[set],
F,G(set)->Element of D()}:
ex f being PartFunc of C(),D() st
(for c be Element of C() holds c in dom f iff P[c] or Q[c]) &
(for c be Element of C() st c in dom f holds
(P[c] implies f.c = F(c)) & (Q[c] implies f.c = G(c)))
provided
A1: for c be Element of C() st P[c] & Q[c] holds F(c)=G(c)
proof defpred X[set] means P[$1] or Q[$1];
consider Y be set such that
A2: for x holds x in Y iff x in C() & X[x] from Separation;
A3: Y c= C()
proof let x; assume x in Y; hence x in C() by A2; end;
defpred X[set,set] means
(P[$1] implies $2 = F($1)) & (Q[$1] implies $2 = G($1));
A4: for x st x in Y ex y st X[x,y]
proof let x; assume A5: x in Y;
then reconsider a' = x as Element of C() by A2;
now per cases by A2,A5;
suppose A6: P[a']; take y = F(a');
now per cases;
suppose Q[a']; then F(a') = G(a') by A1,A6; hence thesis;
suppose not Q[a']; hence thesis;
end; hence thesis;
suppose A7: Q[a']; take y = G(a');
now per cases;
suppose P[a']; then F(a') = G(a') by A1,A7; hence thesis;
suppose not P[a']; hence thesis;
end; hence thesis;
end; hence thesis;
end;
consider f being Function such that
A8: dom f = Y & for x st x in Y holds X[x,f.x] from NonUniqFuncEx(A4);
rng f c= D()
proof let x; assume x in rng f; then consider y such that
A9: y in dom f & x = f.y by FUNCT_1:def 5;
now per cases by A2,A8,A9;
suppose P[y]; then f.y = F(y) by A8,A9;
hence x in D() by A9;
suppose Q[y]; then f.y = G(y) by A8,A9;
hence x in D() by A9;
end; hence x in D();
end;
then reconsider q = f as PartFunc of C(),D() by A3,A8,RELSET_1:11; take q;
thus for c be Element of C() holds c in dom q iff P[c] or Q[c] by A2,A8;
let e be Element of C(); assume e in dom q;
hence thesis by A8;
end;
scheme PartFuncExD2''{C, D()->non empty set,P[set],
F,G(set)->Element of D()}:
ex f being PartFunc of C(),D() st f is total &
(for c be Element of C() st c in dom f holds
(P[c] implies f.c = F(c)) & (not P[c] implies f.c = G(c)))
proof
defpred X[set] means P[$1];
defpred Y[set] means not P[$1];
deffunc U(set) = F($1);
deffunc V(set) = G($1);
A1: for c be Element of C() st X[c] holds not Y[c];
consider f being PartFunc of C(),D() such that
A2: (for c be Element of C() holds c in dom f iff X[c] or Y[c]) &
(for c be Element of C() st c in dom f holds (X[c] implies f.c = U(c)) &
(Y[c] implies f.c = V(c))) from PartFuncExD2(A1); take f;
dom f = C()
proof thus dom f c= C();
let x; assume x in C();
then reconsider b' = x as Element of C();
P[b'] or not P[b']; hence thesis by A2;
end;
hence f is total by PARTFUN1:def 4; thus thesis by A2;
end;
scheme PartFuncExD3{C, D()->non empty set,P,Q,R[set],
F,G,H(set)->Element of D()}:
ex f being PartFunc of C(),D() st
(for c be Element of C() holds c in dom f iff P[c] or Q[c] or R[c]) &
(for c be Element of C() st c in dom f holds (P[c] implies f.c = F(c)) &
(Q[c] implies f.c = G(c)) & (R[c] implies f.c = H(c)))
provided
A1: for c be Element of C() holds (P[c] implies not Q[c]) &
(P[c] implies not R[c]) & (Q[c] implies not R[c])
proof defpred X[set] means P[$1] or Q[$1] or R[$1];
consider Z be set such that
A2: for x holds x in Z iff x in C() & X[x] from Separation;
A3: Z c= C()
proof let x; assume x in Z; hence x in C() by A2; end;
defpred X[set,set] means
(P[$1] implies $2 = F($1)) & (Q[$1] implies $2 = G($1)) &
(R[$1] implies $2 = H($1));
A4: for x st x in Z ex y st X[x,y]
proof let x; assume A5: x in Z;
then reconsider c' = x as Element of C() by A2;
now per cases by A2,A5;
suppose
A6: P[x]; take y = F(x); not Q[c'] & not R[c'] by A1,A6; hence thesis;
suppose
A7: Q[x]; take y = G(x); not P[c'] & not R[c'] by A1,A7; hence thesis;
suppose
A8: R[x]; take y = H(x); not P[c'] & not Q[c'] by A1,A8; hence thesis;
end; hence thesis;
end;
consider f being Function such that
A9: dom f = Z & for x st x in Z holds X[x,f.x] from NonUniqFuncEx(A4);
rng f c= D()
proof let x; assume x in rng f; then consider y such that
A10: y in dom f & x = f.y by FUNCT_1:def 5;
now per cases by A2,A9,A10;
suppose P[y]; then f.y = F(y) by A9,A10;
hence x in D() by A10;
suppose Q[y]; then f.y = G(y) by A9,A10;
hence x in D() by A10;
suppose R[y]; then f.y = H(y) by A9,A10;
hence x in D() by A10;
end; hence x in D();
end;
then reconsider q = f as PartFunc of C(),D() by A3,A9,RELSET_1:11; take q;
thus for c be Element of C() holds c in dom q iff P[c] or Q[c] or R[c] by A2,
A9;
let g be Element of C(); assume g in dom q;
hence thesis by A9;
end;
scheme PartFuncExD3'{C, D()->non empty set,P,Q,R[set],
F,G,H(set)->Element of D()}:
ex f being PartFunc of C(),D() st
(for c be Element of C() holds c in dom f iff P[c] or Q[c] or R[c]) &
(for c be Element of C() st c in dom f holds (P[c] implies f.c = F(c)) &
(Q[c] implies f.c = G(c)) & (R[c] implies f.c = H(c)))
provided
A1: for c be Element of C() holds (P[c] & Q[c] implies F(c)=G(c)) &
(P[c] & R[c] implies F(c)=H(c)) & (Q[c] & R[c] implies G(c)=H(c))
proof defpred X[set] means P[$1] or Q[$1] or R[$1];
consider V be set such that
A2: for x holds x in V iff x in C() & X[x] from Separation;
A3: V c= C()
proof let x; assume x in V; hence x in C() by A2; end;
defpred X[set,set] means
(P[$1] implies $2 = F($1)) & (Q[$1] implies $2 = G($1)) &
(R[$1] implies $2 = H($1));
A4: for x st x in V ex y st X[x,y]
proof let x; assume A5: x in V;
then reconsider d' = x as Element of C() by A2;
now per cases by A2,A5;
suppose A6: P[d']; take y = F(d');
now per cases;
suppose A7: Q[d']; then A8: F(d') = G(d') by A1,A6;
now per cases;
suppose R[d']; then G(d') = H(d') by A1,A7; hence thesis by A8;
suppose not R[d']; hence thesis by A8;
end; hence thesis;
suppose A9: not Q[d'];
now per cases;
suppose R[d']; then F(d') = H(d') by A1,A6; hence thesis by A9;
suppose not R[d']; hence thesis by A9;
end; hence thesis;
end; hence thesis;
suppose A10: Q[d']; take y = G(x);
now per cases;
suppose P[d']; then A11: F(d') = G(d') by A1,A10;
now per cases;
suppose R[d']; then G(d') = H(d') by A1,A10; hence thesis by A11;
suppose not R[d']; hence thesis by A11;
end; hence thesis;
suppose A12: not P[d'];
now per cases;
suppose R[d']; then G(d') = H(d') by A1,A10; hence thesis by A12;
suppose not R[d']; hence thesis by A12;
end; hence thesis;
end; hence thesis;
suppose A13: R[d']; take y = H(x);
now per cases;
suppose P[d']; then A14: F(d') = H(d') by A1,A13;
now per cases;
suppose Q[d']; then G(d') = H(d') by A1,A13; hence thesis by A14;
suppose not Q[d']; hence thesis by A14;
end; hence thesis;
suppose A15: not P[d'];
now per cases;
suppose Q[d']; then G(d') = H(d') by A1,A13; hence thesis by A15;
suppose not Q[d']; hence thesis by A15;
end; hence thesis;
end; hence thesis;
end; hence thesis;
end;
consider f being Function such that
A16: dom f = V & for x st x in V holds X[x,f.x] from NonUniqFuncEx(A4);
rng f c= D()
proof let x; assume x in rng f; then consider y such that
A17: y in dom f & x = f.y by FUNCT_1:def 5;
now per cases by A2,A16,A17;
suppose P[y]; then f.y = F(y) by A16,A17;
hence x in D() by A17;
suppose Q[y]; then f.y = G(y) by A16,A17;
hence x in D() by A17;
suppose R[y]; then f.y = H(y) by A16,A17;
hence x in D() by A17;
end; hence x in D();
end;
then reconsider q = f as PartFunc of C(),D() by A3,A16,RELSET_1:11; take q;
thus for c be Element of C() holds c in dom q iff P[c] or Q[c] or R[c] by A2,
A16;
let i be Element of C(); assume i in dom q;
hence thesis by A16;
end;
scheme PartFuncExD4{C, D()->non empty set,P,Q,R,S[set],
F,G,H,I(set)->Element of D()}:
ex f being PartFunc of C(),D() st
(for c be Element of C() holds c in dom f iff P[c] or Q[c] or R[c] or S[c]) &
(for c be Element of C() st c in dom f holds (P[c] implies f.c = F(c)) &
(Q[c] implies f.c = G(c)) & (R[c] implies f.c = H(c)) &
(S[c] implies f.c = I(c)))
provided
A1: for c be Element of C() holds (P[c] implies not Q[c]) &
(P[c] implies not R[c]) & (P[c] implies not S[c]) &
(Q[c] implies not R[c]) & (Q[c] implies not S[c]) & (R[c] implies not S[c])
proof defpred X[set] means P[$1] or Q[$1] or R[$1] or S[$1];
consider B be set such that
A2: for x holds x in B iff x in C() & X[x] from Separation;
A3: B c= C()
proof let x; assume x in B; hence x in C() by A2; end;
defpred X[set,set] means
(P[$1] implies $2 = F($1)) & (Q[$1] implies $2 = G($1)) &
(R[$1] implies $2 = H($1)) & (S[$1] implies $2 = I($1));
A4: for x st x in B ex y st X[x,y]
proof let x; assume A5: x in B;
then reconsider e' = x as Element of C() by A2;
now per cases by A2,A5;
suppose A6: P[x]; take y = F(x); not Q[e'] & not R[e'] & not S[e'] by A1,A6
;
hence thesis;
suppose A7: Q[x]; take y = G(x); not P[e'] & not R[e'] & not S[e'] by A1,A7
;
hence thesis;
suppose A8: R[x]; take y = H(x); not P[e'] & not Q[e'] & not S[e'] by A1,A8
;
hence thesis;
suppose A9: S[x]; take y = I(x); not P[e'] & not Q[e'] & not R[e'] by A1,A9
;
hence thesis;
end; hence thesis;
end;
consider f being Function such that
A10: dom f = B & for y st y in B holds X[y,f.y] from NonUniqFuncEx(A4);
rng f c= D()
proof let x; assume x in rng f; then consider y such that
A11: y in dom f & x = f.y by FUNCT_1:def 5;
now per cases by A2,A10,A11;
suppose P[y]; then f.y = F(y) by A10,A11;
hence x in D() by A11;
suppose Q[y]; then f.y = G(y) by A10,A11;
hence x in D() by A11;
suppose R[y]; then f.y = H(y) by A10,A11;
hence x in D() by A11;
suppose S[y]; then f.y = I(y) by A10,A11;
hence x in D() by A11;
end; hence x in D();
end;
then reconsider q = f as PartFunc of C(),D() by A3,A10,RELSET_1:11; take q;
thus for c be Element of C() holds c in dom q iff P[c] or Q[c] or R[c] or S[c
]
by A2,A10;
let o be Element of C(); assume o in dom q;
hence thesis by A10;
end;
scheme PartFuncExS2{X, Y()->set,P,Q[set],F,G(set)->set}:
ex f being PartFunc of X(),Y() st
(for x holds x in dom f iff x in X() & (P[x] or Q[x])) &
(for x st x in dom f holds (P[x] implies f.x=F(x)) & (Q[x] implies f.x=G(x)))
provided
A1: for x st x in X() holds P[x] implies not Q[x] and
A2: for x st x in X() & P[x] holds F(x) in Y() and
A3: for x st x in X() & Q[x] holds G(x) in Y()
proof defpred X[set] means P[$1] or Q[$1];
consider A be set such that
A4: for x holds x in A iff x in X() & X[x] from Separation;
A5: A c= X()
proof let x; assume x in A; hence x in X() by A4; end;
defpred X[set,set] means
(P[$1] implies $2 = F($1)) & (Q[$1] implies $2 = G($1));
A6: for x st x in A ex y st X[x,y]
proof let x; assume A7: x in A; then A8: x in X() by A4;
now per cases by A4,A7;
suppose A9: P[x]; take y = F(x); not Q[x] by A1,A8,A9; hence thesis;
suppose A10: Q[x]; take y = G(x); not P[x] by A1,A8,A10; hence thesis;
end; hence thesis;
end;
consider f being Function such that
A11: dom f = A & for x st x in A holds X[x,f.x] from NonUniqFuncEx(A6);
rng f c= Y()
proof let x; assume x in rng f; then consider y such that
A12: y in dom f & x = f.y by FUNCT_1:def 5;
now per cases by A4,A11,A12;
suppose A13: P[y]; then f.y = F(y) by A11,A12;
hence x in Y() by A2,A5,A11,A12,A13;
suppose A14: Q[y]; then f.y = G(y) by A11,A12;
hence x in Y() by A3,A5,A11,A12,A14;
end; hence x in Y();
end;
then reconsider f as PartFunc of X(),Y() by A5,A11,RELSET_1:11; take f;
thus for x holds x in dom f iff x in X() & (P[x] or Q[x]) by A4,A11;
let x; assume x in dom f; hence thesis by A11;
end;
scheme PartFuncExS3{X, Y()->set,P,Q,R[set],
F,G,H(set)->set}:
ex f being PartFunc of X(),Y() st
(for x holds x in dom f iff x in X() & (P[x] or Q[x] or R[x])) &
(for x st x in dom f holds
(P[x] implies f.x=F(x)) & (Q[x] implies f.x=G(x)) &
(R[x] implies f.x=H(x)))
provided
A1: for x st x in X() holds (P[x] implies not Q[x]) & (P[x] implies not R[x]) &
(Q[x] implies not R[x]) and
A2: for x st x in X() & P[x] holds F(x) in Y() and
A3: for x st x in X() & Q[x] holds G(x) in Y() and
A4: for x st x in X() & R[x] holds H(x) in Y()
proof defpred X[set] means P[$1] or Q[$1] or R[$1];
consider S be set such that
A5: for x holds x in S iff x in X() & X[x] from Separation;
A6: S c= X()
proof let x; assume x in S; hence x in X() by A5; end;
defpred X[set,set] means
(P[$1] implies $2 = F($1)) & (Q[$1] implies $2 = G($1)) &
(R[$1] implies $2 = H($1));
A7: for x st x in S ex y st X[x,y]
proof let x; assume A8: x in S; then A9: x in X() by A5;
now per cases by A5,A8;
suppose
A10: P[x]; take y = F(x); not Q[x] & not R[x] by A1,A9,A10; hence thesis;
suppose
A11: Q[x]; take y = G(x); not P[x] & not R[x] by A1,A9,A11; hence thesis;
suppose
A12: R[x]; take y = H(x); not P[x] & not Q[x] by A1,A9,A12; hence thesis;
end; hence thesis;
end;
consider f being Function such that
A13: dom f = S & for x st x in S holds X[x,f.x] from NonUniqFuncEx(A7);
rng f c= Y()
proof let x; assume x in rng f; then consider y such that
A14: y in dom f & x = f.y by FUNCT_1:def 5;
now per cases by A5,A13,A14;
suppose A15: P[y]; then f.y = F(y) by A13,A14;
hence x in Y() by A2,A6,A13,A14,A15;
suppose A16: Q[y]; then f.y = G(y) by A13,A14;
hence x in Y() by A3,A6,A13,A14,A16;
suppose A17: R[y]; then f.y = H(y) by A13,A14;
hence x in Y() by A4,A6,A13,A14,A17;
end; hence x in Y();
end;
then reconsider f as PartFunc of X(),Y() by A6,A13,RELSET_1:11; take f;
thus for x holds x in dom f iff x in X() & (P[x] or Q[x] or R[x]) by A5,A13;
let x; assume x in dom f; hence thesis by A13;
end;
scheme PartFuncExS4{X, Y()->set,P,Q,R,S[set],
F,G,H,I(set)->set}:
ex f being PartFunc of X(),Y() st
(for x holds x in dom f iff x in X() & (P[x] or Q[x] or R[x] or S[x])) &
(for x st x in dom f holds
(P[x] implies f.x=F(x)) & (Q[x] implies f.x=G(x)) &
(R[x] implies f.x=H(x)) & (S[x] implies f.x=I(x)))
provided
A1: for x st x in X() holds (P[x] implies not Q[x]) & (P[x] implies not R[x]) &
(P[x] implies not S[x]) & (Q[x] implies not R[x]) &
(Q[x] implies not S[x]) & (R[x] implies not S[x]) and
A2: for x st x in X() & P[x] holds F(x) in Y() and
A3: for x st x in X() & Q[x] holds G(x) in Y() and
A4: for x st x in X() & R[x] holds H(x) in Y() and
A5: for x st x in X() & S[x] holds I(x) in Y()
proof defpred X[set] means P[$1] or Q[$1] or R[$1] or S[$1];
consider D be set such that
A6:for x holds x in D iff x in X() & X[x] from Separation;
A7: D c= X()
proof let x; assume x in D; hence x in X() by A6; end;
defpred X[set,set] means
(P[$1] implies $2 = F($1)) & (Q[$1] implies $2 = G($1)) &
(R[$1] implies $2 = H($1)) & (S[$1] implies $2 = I($1));
A8: for x st x in D ex y st X[x,y]
proof let x; assume A9: x in D; then A10: x in X() by A6;
now per cases by A6,A9;
suppose
A11: P[x]; take y = F(x); not Q[x] & not R[x] & not S[x] by A1,A10,A11;
hence thesis;
suppose
A12: Q[x]; take y = G(x); not P[x] & not R[x] & not S[x] by A1,A10,A12;
hence thesis;
suppose
A13: R[x]; take y = H(x); not P[x] & not Q[x] & not S[x] by A1,A10,A13;
hence thesis;
suppose
A14: S[x]; take y = I(x); not P[x] & not Q[x] & not R[x] by A1,A10,A14;
hence thesis;
end; hence thesis;
end;
consider f being Function such that
A15: dom f = D & for x st x in D holds X[x,f.x] from NonUniqFuncEx(A8);
rng f c= Y()
proof let x; assume x in rng f; then consider y such that
A16: y in dom f & x = f.y by FUNCT_1:def 5;
now per cases by A6,A15,A16;
suppose A17: P[y]; then f.y = F(y) by A15,A16;
hence x in Y() by A2,A7,A15,A16,A17;
suppose A18: Q[y]; then f.y = G(y) by A15,A16;
hence x in Y() by A3,A7,A15,A16,A18;
suppose A19: R[y]; then f.y = H(y) by A15,A16;
hence x in Y() by A4,A7,A15,A16,A19;
suppose A20: S[y]; then f.y = I(y) by A15,A16;
hence x in Y() by A5,A7,A15,A16,A20;
end; hence x in Y();
end;
then reconsider f as PartFunc of X(),Y() by A7,A15,RELSET_1:11; take f;
thus for x holds
x in dom f iff x in X() & (P[x] or Q[x] or R[x] or S[x]) by A6,A15;
let x; assume x in dom f; hence thesis by A15;
end;
scheme PartFuncExC_D2{C, D, E()->non empty set, P,Q[set,set],
F,G(set,set)->Element of E()}:
ex f being PartFunc of [:C(),D():],E() st
(for c be Element of C() ,d be Element of D() holds
[c,d] in dom f iff P[c,d] or Q[c,d]) &
for c be Element of C() ,d be Element of D() st [c,d] in dom f holds
(P[c,d] implies f.[c,d]=F(c,d)) & (Q[c,d] implies f.[c,d]=G(c,d))
provided
A1: for c be Element of C() ,d be Element of D() st P[c,d] holds not Q[c,d]
proof defpred X[set] means
for c be Element of C() ,d be Element of D() st $1 = [c,d] holds
P[c,d] or Q[c,d];
consider F be set such that
A2: for z holds z in F iff z in [:C(),D():] & X[z] from Separation;
A3: F c= [:C(),D():]
proof let z; assume z in F; hence z in [:C(),D():] by A2; end;
defpred X[set,set] means
for c be Element of C() ,t be Element of D() st $1 = [c,t] holds
(P[c,t] implies $2 = F(c,t)) & (Q[c,t] implies $2 = G(c,t));
A4: for x1 be set st x1 in F ex z st X[x1,z]
proof let x1 be set; assume A5: x1 in F; then x1 in [:C(),D():] by A2;
then consider f',g' be set such that
A6: f' in C() & g' in D() & x1 = [f',g'] by ZFMISC_1:def 2;
reconsider f' as Element of C() by A6;
reconsider g' as Element of D() by A6;
now per cases by A2,A5,A6;
suppose A7: P[f',g']; take z = F(f',g');
let p be Element of C() ,d be Element of D(); assume x1 = [p,d];
then f' = p & g' = d by A6,ZFMISC_1:33;
hence (P[p,d] implies z = F(p,d)) & (Q[p,d] implies z = G(p,d)) by A1,A7;
suppose A8: Q[f',g']; take z = G(f',g');
let r be Element of C() ,d be Element of D(); assume x1 = [r,d];
then f' = r & g' = d by A6,ZFMISC_1:33;
hence (P[r,d] implies z = F(r,d)) & (Q[r,d] implies z = G(r,d)) by A1,A8;
end;
hence thesis;
end;
consider f being Function such that
A9: dom f = F & for z st z in F holds X[z,f.z] from NonUniqFuncEx(A4);
rng f c= E()
proof let z; assume z in rng f; then consider x1 be set such that
A10: x1 in dom f & z = f.x1 by FUNCT_1:def 5; x1 in [:C(),D():] by A2,A9,A10
;
then consider x,y such that A11: x in C() & y in D() & x1 = [x,y] by
ZFMISC_1:def 2;
reconsider x as Element of C() by A11;
reconsider y as Element of D() by A11;
now per cases by A2,A9,A10,A11;
suppose P[x,y]; then f.[x,y] = F(x,y) by A9,A10,A11;
hence z in E() by A10,A11;
suppose Q[x,y]; then f.[x,y] = G(x,y) by A9,A10,A11;
hence z in E() by A10,A11;
end; hence z in E();
end;
then reconsider f as PartFunc of [:C(),D():],E() by A3,A9,RELSET_1:11;
take f;
thus for c be Element of C() ,h be Element of D() holds
[c,h] in dom f iff P[c,h] or Q[c,h]
proof let c be Element of C() ,g be Element of D();
thus [c,g] in dom f implies P[c,g] or Q[c,g] by A2,A9;
assume A12: P[c,g] or Q[c,g];
A13: [c,g] in [:C(),D():] by ZFMISC_1:106;
now let h' be Element of C() ,j' be Element of D(); assume [c,g] = [h',j'
]
;
then c = h' & g = j' by ZFMISC_1:33; hence P[h',j'] or Q[h',j'] by A12;
end; hence thesis by A2,A9,A13;
end;
let c be Element of C() ,d be Element of D(); assume [c,d] in dom f;
hence thesis by A9;
end;
scheme PartFuncExC_D3{C, D, E()->non empty set,
P,Q,R[set,set],
F,G,H(set,set)->Element of E()}:
ex f being PartFunc of [:C(),D():],E() st
(for c be Element of C() ,d be Element of D() holds
[c,d] in dom f iff P[c,d] or Q[c,d] or R[c,d]) &
for c be Element of C() ,r be Element of D() st [c,r] in dom f holds
(P[c,r] implies f.[c,r]=F(c,r)) & (Q[c,r] implies f.[c,r]=G(c,r)) &
(R[c,r] implies f.[c,r]=H(c,r))
provided
A1: for c be Element of C() ,s be Element of D() holds
(P[c,s] implies not Q[c,s]) & (P[c,s] implies not R[c,s]) &
(Q[c,s] implies not R[c,s])
proof
defpred X[set] means
for c be Element of C() ,d be Element of D() st $1 = [c,d] holds
P[c,d] or Q[c,d] or R[c,d];
consider T be set such that
A2: for z holds z in T iff z in [:C(),D():] & X[z] from Separation;
A3: T c= [:C(),D():]
proof let z; assume z in T; hence z in [:C(),D():] by A2; end;
defpred X[set,set] means
for c be Element of C() ,t be Element of D() st $1 = [c,t] holds
(P[c,t] implies $2 = F(c,t)) & (Q[c,t] implies $2 = G(c,t)) &
(R[c,t] implies $2 = H(c,t));
A4: for x1 be set st x1 in T ex z st X[x1,z]
proof let x1 be set; assume A5: x1 in T; then x1 in [:C(),D():] by A2;
then consider q',w' be set such that
A6: q' in C() & w' in D() & x1 = [q',w'] by ZFMISC_1:def 2;
reconsider q' as Element of C() by A6;
reconsider w' as Element of D() by A6;
now per cases by A2,A5,A6;
suppose A7: P[q',w']; take z = F(q',w');
let c be Element of C() ,d be Element of D(); assume x1 = [c,d];
then q' = c & w' = d by A6,ZFMISC_1:33;
hence (P[c,d] implies z = F(c,d)) & (Q[c,d] implies z = G(c,d)) &
(R[c,d] implies z = H(c,d)) by A1,A7;
suppose A8: Q[q',w']; take z = G(q',w');
let c be Element of C() ,d be Element of D(); assume x1 = [c,d];
then q' = c & w' = d by A6,ZFMISC_1:33;
hence (P[c,d] implies z = F(c,d)) & (Q[c,d] implies z = G(c,d)) &
(R[c,d] implies z = H(c,d)) by A1,A8;
suppose A9: R[q',w']; take z = H(q',w');
let c be Element of C() ,d be Element of D(); assume x1 = [c,d];
then q' = c & w' = d by A6,ZFMISC_1:33;
hence (P[c,d] implies z = F(c,d)) & (Q[c,d] implies z = G(c,d)) &
(R[c,d] implies z = H(c,d)) by A1,A9;
end; hence thesis;
end;
consider f being Function such that
A10: dom f = T & for z st z in T holds X[z,f.z] from NonUniqFuncEx(A4);
rng f c= E()
proof let z; assume z in rng f; then consider x1 be set such that
A11: x1 in dom f & z = f.x1 by FUNCT_1:def 5
; x1 in [:C(),D():] by A2,A10,A11
;
then consider x,y such that A12: x in C() & y in D() & x1 = [x,y] by
ZFMISC_1:def 2;
reconsider x as Element of C() by A12;
reconsider y as Element of D() by A12;
now per cases by A2,A10,A11,A12;
suppose P[x,y]; then f.[x,y] = F(x,y) by A10,A11,A12;
hence z in E() by A11,A12;
suppose Q[x,y]; then f.[x,y] = G(x,y) by A10,A11,A12;
hence z in E() by A11,A12;
suppose R[x,y]; then f.[x,y] = H(x,y) by A10,A11,A12;
hence z in E() by A11,A12;
end; hence z in E();
end;
then reconsider f as PartFunc of [:C(),D():],E() by A3,A10,RELSET_1:11;
take f;
thus for c be Element of C() ,d be Element of D() holds
[c,d] in dom f iff P[c,d] or Q[c,d] or R[c,d]
proof let c be Element of C() ,d be Element of D();
thus [c,d] in dom f implies P[c,d] or Q[c,d] or R[c,d] by A2,A10;
assume A13: P[c,d] or Q[c,d] or R[c,d];
A14: [c,d] in [:C(),D():] by ZFMISC_1:106;
now let i' be Element of C() ,o' be Element of D(); assume [c,d] = [i',o'
]
;
then c = i' & d = o' by ZFMISC_1:33;
hence P[i',o'] or Q[i',o'] or R[i',o'] by A13;
end; hence thesis by A2,A10,A14;
end;
let c be Element of C() ,d be Element of D(); assume [c,d] in dom f;
hence thesis by A10;
end;
scheme PartFuncExC_S2{X, Y, Z()->set,P,Q[set,set],
F,G(set,set)->set}:
ex f being PartFunc of [:X(),Y():],Z() st
(for x,y holds [x,y] in dom f iff x in X() & y in Y() & (P[x,y] or Q[x,y])) &
(for x,y st [x,y] in dom f holds (P[x,y] implies f.[x,y]=F(x,y)) &
(Q[x,y] implies f.[x,y]=G(x,y)))
provided
A1: for x,y st x in X() & y in Y() holds P[x,y] implies not Q[x,y] and
A2: for x,y st x in X() & y in Y() & P[x,y] holds F(x,y) in Z() and
A3: for x,y st x in X() & y in Y() & Q[x,y] holds G(x,y) in Z()
proof
defpred X[set] means
for x,y st $1 = [x,y] holds P[x,y] or Q[x,y];
consider K be set such that
A4: for z holds z in K iff z in [:X(),Y():] & X[z] from Separation;
A5: K c= [:X(),Y():]
proof let z; assume z in K; hence z in [:X(),Y():] by A4; end;
defpred X[set,set] means
for x ,y st $1 = [x,y] holds
(P[x,y] implies $2 = F(x,y)) & (Q[x,y] implies $2 = G(x,y));
A6: for x1 be set st x1 in K ex z st X[x1,z]
proof let x1 be set; assume A7: x1 in K; then x1 in [:X(),Y():] by A4;
then consider n',m' be set such that
A8: n' in X() & m' in Y() & x1 = [n',m'] by ZFMISC_1:def 2;
now per cases by A4,A7,A8;
suppose A9: P[n',m']; take z = F(n',m');
let x,y; assume x1 = [x,y]; then n' = x & m' = y by A8,ZFMISC_1:33;
hence (P[x,y] implies z = F(x,y)) & (Q[x,y] implies z = G(x,y)) by A1,A8,A9
;
suppose A10: Q[n',m']; take z = G(n',m');
let x,y; assume x1 = [x,y]; then n' = x & m' = y by A8,ZFMISC_1:33;
hence (P[x,y] implies z = F(x,y)) & (Q[x,y] implies z = G(x,y)) by A1,A8,
A10;
end; hence thesis;
end;
consider f being Function such that
A11: dom f = K & for z st z in K holds X[z,f.z] from NonUniqFuncEx(A6);
rng f c= Z()
proof let z; assume z in rng f; then consider x1 be set such that
A12: x1 in dom f & z = f.x1 by FUNCT_1:def 5;
x1 in [:X(),Y():] by A4,A11,A12;
then consider x,y such that A13: x in X() & y in Y() & x1 = [x,y] by
ZFMISC_1:def 2;
now per cases by A4,A11,A12,A13;
suppose A14: P[x,y]; then f.[x,y] = F(x,y) by A11,A12,A13;
hence z in Z() by A2,A12,A13,A14;
suppose A15: Q[x,y]; then f.[x,y] = G(x,y) by A11,A12,A13;
hence z in Z() by A3,A12,A13,A15;
end; hence z in Z();
end;
then reconsider f as PartFunc of [:X(),Y():],Z() by A5,A11,RELSET_1:11;
take f;
thus for x,y holds [x,y] in dom f iff x in X() & y in Y() & (P[x,y] or Q[x,y]
)
proof let x,y;
thus [x,y] in dom f implies x in X() & y in Y() &
(P[x,y] or Q[x,y]) by A4,A11,ZFMISC_1:106;
assume A16: x in X() & y in Y() & (P[x,y] or Q[x,y]);
then A17: [x,y] in [:X(),Y():] by ZFMISC_1:106;
now let z',q' be set; assume [x,y] = [z',q'];
then x = z' & y = q' by ZFMISC_1:33;
hence P[z',q'] or Q[z',q'] by A16;
end; hence thesis by A4,A11,A17;
end;
let x,y; assume [x,y] in dom f;hence thesis by A11;
end;
scheme PartFuncExC_S3{X, Y, Z()->set, P,Q,R[set,set],
F,G,H(set,set)->set}:
ex f being PartFunc of [:X(),Y():],Z() st
(for x,y holds [x,y] in dom f iff x in X() & y in Y() &
(P[x,y] or Q[x,y] or R[x,y])) &
(for x,y st [x,y] in dom f holds (P[x,y] implies f.[x,y]=F(x,y)) &
(Q[x,y] implies f.[x,y]=G(x,y)) & (R[x,y] implies f.[x,y]=H(x,y)))
provided
A1: for x,y st x in X() & y in Y() holds (P[x,y] implies not Q[x,y]) &
(P[x,y] implies not R[x,y]) & (Q[x,y] implies not R[x,y]) and
A2: for x,y st x in X() & y in Y() holds P[x,y] implies F(x,y) in Z() and
A3: for x,y st x in X() & y in Y() holds Q[x,y] implies G(x,y) in Z() and
A4: for x,y st x in X() & y in Y() holds R[x,y] implies H(x,y) in Z()
proof
defpred X[set] means
for x,y st $1 = [x,y] holds P[x,y] or Q[x,y] or R[x,y];
consider L be set such that
A5: for z holds z in L iff z in [:X(),Y():] & X[z] from Separation;
A6: L c= [:X(),Y():]
proof let z; assume z in L; hence z in [:X(),Y():] by A5; end;
defpred X[set,set] means
for x ,y st $1 = [x,y] holds
(P[x,y] implies $2 = F(x,y)) & (Q[x,y] implies $2 = G(x,y)) &
(R[x,y] implies $2 = H(x,y));
A7: for x1 be set st x1 in L ex z st X[x1,z]
proof let x1 be set; assume A8: x1 in L; then x1 in [:X(),Y():] by A5;
then consider z',a' be set such that
A9: z' in X() & a' in Y() & x1 = [z',a'] by ZFMISC_1:def 2;
now per cases by A5,A8,A9;
suppose A10: P[z',a']; take z = F(z',a');
let x,y; assume x1 = [x,y]; then z' = x & a' = y by A9,ZFMISC_1:33;
hence (P[x,y] implies z = F(x,y)) & (Q[x,y] implies z = G(x,y)) &
(R[x,y] implies z = H(x,y)) by A1,A9,A10;
suppose A11: Q[z',a']; take z = G(z',a');
let x,y; assume x1 = [x,y]; then z' = x & a' = y by A9,ZFMISC_1:33;
hence (P[x,y] implies z = F(x,y)) & (Q[x,y] implies z = G(x,y)) &
(R[x,y] implies z = H(x,y)) by A1,A9,A11;
suppose A12: R[z',a']; take z=H(z',a');
let x,y; assume x1 = [x,y]; then z' = x & a' = y by A9,ZFMISC_1:33;
hence (P[x,y] implies z = F(x,y)) & (Q[x,y] implies z = G(x,y)) &
(R[x,y] implies z = H(x,y)) by A1,A9,A12;
end;
hence thesis;
end;
consider f being Function such that
A13: dom f = L & for z st z in L holds X[z,f.z] from NonUniqFuncEx(A7);
rng f c= Z()
proof let z; assume z in rng f; then consider x1 be set such that
A14: x1 in dom f & z = f.x1 by FUNCT_1:def 5
; x1 in [:X(),Y():] by A5,A13,A14
;
then consider x,y such that
A15: x in X() & y in Y() & x1 = [x,y] by ZFMISC_1:def 2;
now per cases by A5,A13,A14,A15;
suppose A16: P[x,y]; then f.[x,y] = F(x,y) by A13,A14,A15;
hence z in Z() by A2,A14,A15,A16;
suppose A17: Q[x,y]; then f.[x,y] = G(x,y) by A13,A14,A15;
hence z in Z() by A3,A14,A15,A17;
suppose A18: R[x,y]; then f.[x,y] = H(x,y) by A13,A14,A15;
hence z in Z() by A4,A14,A15,A18;
end; hence z in Z();
end;
then reconsider f as PartFunc of [:X(),Y():],Z() by A6,A13,RELSET_1:11;
take f;
thus for x,y holds
[x,y] in dom f iff x in X() & y in Y() & (P[x,y] or Q[x,y] or R[x,y])
proof let x,y;
thus [x,y] in dom f implies
x in X() & y in Y() & (P[x,y] or Q[x,y] or R[x,y])
by A5,A13,ZFMISC_1:106;
assume A19: x in X() & y in Y() & (P[x,y] or Q[x,y] or R[x,y]);
then A20: [x,y] in [:X(),Y():] by ZFMISC_1:106;
now let f',r' be set; assume [x,y]=[f',r'];
then x = f' & y = r' by ZFMISC_1:33;
hence P[f',r'] or Q[f',r'] or R[f',r'] by A19;
end;
hence thesis by A5,A13,A20;
end;
let x,y; assume [x,y] in dom f;
hence thesis by A13;
end;
scheme ExFuncD3{C, D()->non empty set,P,Q,R[set],
F,G,H(set)->Element of D()}:
ex f being Function of C(),D() st
for c be Element of C() holds (P[c] implies f.c = F(c)) &
(Q[c] implies f.c = G(c)) & (R[c] implies f.c = H(c))
provided
A1: for c be Element of C() holds (P[c] implies not Q[c]) &
(P[c] implies not R[c]) & (Q[c] implies not R[c]) and
A2: for c be Element of C() holds P[c] or Q[c] or R[c]
proof
defpred X[set] means P[$1];
defpred Y[set] means Q[$1];
defpred Z[set] means R[$1];
deffunc U(set) = F($1);
deffunc V(set) = G($1);
deffunc W(set) = H($1);
A3: for c be Element of C() holds (X[c] implies not Y[c]) &
(X[c] implies not Z[c]) & (Y[c] implies not Z[c]) by A1;
consider f being PartFunc of C(),D() such that
A4: for w be Element of C() holds w in dom f iff X[w] or Y[w] or Z[w] and
A5: for q be Element of C() st q in dom f holds (X[q] implies f.q = U(q)) &
(Y[q] implies f.q = V(q)) & (Z[q] implies f.q = W(q)) from PartFuncExD3(A3);
set q = f;
A6: dom q = C()
proof thus dom q c= C();
let x; assume x in C();
then reconsider t' = x as Element of C();
P[t'] or Q[t'] or R[t'] by A2; hence thesis by A4;
end;
then reconsider q as Function of C(),D() by FUNCT_2:def 1; take q;
let t be Element of C();
thus (P[t] implies q.t = F(t)) & (Q[t] implies q.t = G(t)) &
(R[t] implies q.t = H(t)) by A5,A6;
end;
scheme ExFuncD4{C, D()->non empty set, P,Q,R,S[set],
F,G,H,I(set)->Element of D()}:
ex f being Function of C(),D() st
for c be Element of C() holds (P[c] implies f.c = F(c)) &
(Q[c] implies f.c = G(c)) & (R[c] implies f.c = H(c)) &
(S[c] implies f.c = I(c))
provided
A1: for c be Element of C() holds (P[c] implies not Q[c]) &
(P[c] implies not R[c]) & (P[c] implies not S[c]) &
(Q[c] implies not R[c]) & (Q[c] implies not S[c]) &
(R[c] implies not S[c]) and
A2: for c be Element of C() holds P[c] or Q[c] or R[c] or S[c]
proof
defpred X[set] means P[$1];
defpred Y[set] means Q[$1];
defpred Z[set] means R[$1];
defpred O[set] means S[$1];
deffunc U(set) = F($1);
deffunc V(set) = G($1);
deffunc W(set) = H($1);
deffunc T(set) = I($1);
A3: for c be Element of C() holds (X[c] implies not Y[c]) &
(X[c] implies not Z[c]) & (X[c] implies not O[c]) &
(Y[c] implies not Z[c]) & (Y[c] implies not O[c]) &
(Z[c] implies not O[c]) by A1;
consider f being PartFunc of C(),D() such that
A4: for r be Element of C() holds
r in dom f iff X[r] or Y[r] or Z[r] or O[r] and
A5: for o be Element of C() st o in dom f holds (X[o] implies f.o = U(o)) &
(Y[o] implies f.o = V(o)) & (Z[o] implies f.o = W(o)) &
(O[o] implies f.o = T(o)) from PartFuncExD4(A3);
set q=f;
A6: dom q = C()
proof
thus dom q c= C();
let x; assume x in C();
then reconsider w' = x as Element of C();
P[w'] or Q[w'] or R[w'] or S[w'] by A2; hence thesis by A4;
end;
then reconsider q as Function of C(),D() by FUNCT_2:def 1;
take q;
let e be Element of C();
thus (P[e] implies q.e = F(e)) & (Q[e] implies q.e = G(e)) &
(R[e] implies q.e = H(e)) & (S[e] implies q.e = I(e)) by A5,A6;
end;
scheme FuncExC_D2{C, D, E()->non empty set,P[set,set],
F,G(set,set)->Element of E()}:
ex f being Function of [:C(),D():],E() st
for c be Element of C() ,d be Element of D() st [c,d] in dom f holds
(P[c,d] implies f.[c,d]=F(c,d)) & (not P[c,d] implies f.[c,d]=G(c,d))
proof
defpred X[set,set] means P[$1,$2];
defpred Y[set,set] means not P[$1,$2];
deffunc U(set,set) = F($1,$2);
deffunc V(set,set) = G($1,$2);
A1: for c be Element of C() ,f being Element of D() st X[c,f] holds
not Y[c,f];
consider f being PartFunc of [:C(),D():],E() such that
A2: (for c be Element of C() ,e be Element of D() holds
[c,e] in dom f iff X[c,e] or Y[c,e]) &
for c be Element of C() ,g being Element of D() st [c,g] in dom f holds
(X[c,g] implies f.[c,g] = U(c,g)) & (Y[c,g] implies f.[c,g] = V(c,g))
from PartFuncExC_D2(A1);
A3: dom f = [:C(),D():]
proof
thus dom f c= [:C(),D():];
let x; assume x in [:C(),D():]; then consider y,z such that
A4: y in C() & z in D() & x = [y,z] by ZFMISC_1:def 2;
reconsider y as Element of C() by A4;
reconsider z as Element of D() by A4;
P[y,z] or not P[y,z]; hence thesis by A2,A4;
end;
consider g be Function such that A5: g=f;
reconsider g as Function of [:C(),D():],E() by A3,A5,FUNCT_2:def 1;
take g; thus thesis by A2,A5;
end;
scheme FuncExC_D3{C, D, E()->non empty set, P,Q,R[set,set],
F,G,H(set,set)->Element of E()}:
ex f being Function of [:C(),D():],E() st
(for c be Element of C() ,d be Element of D() holds
[c,d] in dom f iff P[c,d] or Q[c,d] or R[c,d]) &
for c be Element of C() ,d be Element of D() st [c,d] in dom f holds
(P[c,d] implies f.[c,d]=F(c,d)) & (Q[c,d] implies f.[c,d]=G(c,d)) &
(R[c,d] implies f.[c,d]=H(c,d))
provided
A1: for c be Element of C() ,d be Element of D() holds
(P[c,d] implies not Q[c,d]) & (P[c,d] implies not R[c,d]) &
(Q[c,d] implies not R[c,d]) and
A2: for c be Element of C() ,d be Element of D() holds
P[c,d] or Q[c,d] or R[c,d]
proof
defpred X[set,set] means P[$1,$2];
defpred Y[set,set] means Q[$1,$2];
defpred Z[set,set] means R[$1,$2];
deffunc U(set,set) = F($1,$2);
deffunc V(set,set) = G($1,$2);
deffunc W(set,set) = H($1,$2);
A3: for c be Element of C() ,d be Element of D() holds
(X[c,d] implies not Y[c,d]) & (X[c,d] implies not Z[c,d]) &
(Y[c,d] implies not Z[c,d]) by A1;
consider f being PartFunc of [:C(),D():],E() such that
A4: (for c be Element of C() ,b be Element of D() holds
[c,b] in dom f iff X[c,b] or Y[c,b] or Z[c,b]) &
for a being Element of C() ,b be Element of D() st [a,b] in dom f holds
(X[a,b] implies f.[a,b] = U(a,b)) & (Y[a,b] implies f.[a,b] = V(a,b)) &
(Z[a,b] implies f.[a,b] = W(a,b)) from PartFuncExC_D3(A3);
A5: dom f = [:C(),D():]
proof
thus dom f c= [:C(),D():];
let x; assume x in [:C(),D():]; then consider y,z such that
A6: y in C() & z in D() & x = [y,z] by ZFMISC_1:def 2;
reconsider y as Element of C() by A6;
reconsider z as Element of D() by A6;
P[y,z] or Q[y,z] or R[y,z] by A2; hence thesis by A4,A6;
end;
consider v be Function such that A7: v = f;
reconsider v as Function of [:C(),D():],E() by A5,A7,FUNCT_2:def 1;
take v; thus thesis by A4,A7;
end;