Copyright (c) 1990 Association of Mizar Users
environ
constructors XBOOLE_0;
clusters XBOOLE_0;
begin
reserve a,b,d for set;
scheme Schemat0 {P[set]} :
ex a st P[a]
provided
A1: for a holds P[a]
proof
consider a;
P[a] by A1;
hence thesis;
end;
scheme Schemat1a {P[set],T[]} :
(for a holds P[a]) & T[]
provided
A1: for a holds (P[a] & T[]) by A1;
scheme Schemat1b {P[set],T[]} :
for a holds (P[a] & T[])
provided
A1: (for a holds P[a]) & T[] by A1;
scheme Schemat2a {P[set], T[]} :
(ex a st P[a]) or T[]
provided
A1: ex a st (P[a] or T[]) by A1;
scheme Schemat2b {P[set], T[]} :
ex a st (P[a] or T[])
provided
A1: (ex a st P[a]) or T[] by A1;
scheme Schemat3 {S[set,set]} :
for b ex a st S[a,b]
provided
A1: ex a st for b holds S[a,b]
proof
consider a such that A2:for b holds S[a,b] by A1;
now
let b;
S[a,b] by A2;
hence ex a st S[a,b];
end;
hence thesis;
end;
scheme Schemat4a {P[set],Q[set]} :
(ex a st P[a]) or (ex a st Q[a])
provided
A1: ex a st (P[a] or Q[a]) by A1;
scheme Schemat4b {P[set],Q[set]} :
ex a st (P[a] or Q[a])
provided
A1: (ex a st P[a]) or (ex a st Q[a]) by A1;
scheme Schemat5 {P[set],Q[set]} :
(ex a st P[a]) & (ex a st Q[a])
provided
A1: ex a st (P[a] & Q[a]) by A1;
scheme Schemat6a {P[set],Q[set]} :
(for a holds P[a]) & (for a holds Q[a])
provided
A1: for a holds (P[a] & Q[a]) by A1;
scheme Schemat6b {P[set],Q[set]} :
for a holds (P[a] & Q[a])
provided
A1: (for a holds P[a]) & (for a holds Q[a]) by A1;
scheme Schemat7 {P[set],Q[set]} :
for a holds (P[a] or Q[a])
provided
A1: (for a holds P[a]) or (for a holds Q[a]) by A1;
scheme Schemat8 {P[set],Q[set]} :
(for a holds P[a]) implies (for a holds Q[a])
provided
A1: for a holds P[a] implies Q[a]
proof
assume A2:for a holds P[a];
now
let a;
(P[a] implies Q[a]) & P[a] by A1,A2;
hence Q[a];
end;
hence thesis;
end;
scheme Schemat9 {P[set],Q[set]} :
(for a holds P[a]) iff (for a holds Q[a])
provided
A1: for a holds (P[a] iff Q[a])
proof
thus (for a holds P[a]) implies (for a holds Q[a])
proof
assume A2:for a holds P[a];
now
let a;
(P[a] iff Q[a]) & P[a] by A1,A2;
hence Q[a];
end;
hence thesis;
end;
assume A3:for a holds Q[a];
now
let a;
(P[a] iff Q[a]) & Q[a] by A1,A3;
hence P[a];
end;
hence thesis;
end;
scheme Schemat10b {T[]} :
for a holds T[]
provided
A1: T[] by A1;
scheme Schemat11a {P[set],T[]} :
(for a holds P[a]) or T[]
provided
A1: for a holds (P[a] or T[]) by A1;
scheme Schemat11b {P[set],T[]} :
for a holds (P[a] or T[])
provided
A1: (for a holds P[a]) or T[] by A1;
scheme Schemat12a {P[set],T[]} :
ex a st (T[] & P[a])
provided
A1: T[] & (ex a st P[a]) by A1;
scheme Schemat12b {P[set],T[]} :
T[] & (ex a st P[a])
provided
A1: ex a st (T[] & P[a]) by A1;
scheme Schemat13a {P[set],T[]} :
for a holds (T[] implies P[a])
provided
A1: T[] implies (for a holds P[a]) by A1;
scheme Schemat13b {P[set],T[]} :
T[] implies (for a holds P[a])
provided
A1: for a holds (T[] implies P[a]) by A1;
scheme Schemat14 {P[set],T[]} :
ex a st (T[] implies P[a])
provided
A1: T[] implies (ex a st P[a]) by A1;
scheme Schemat17 {P[set],T[]} :
(for a holds P[a]) implies T[]
provided
A1: for a holds (P[a] implies T[])
proof
assume A2:for a holds P[a];
now
let a; P[a] by A2;
hence T[] by A1;
end;
hence thesis;
end;
scheme Schemat18a {P[set],Q[set]} :
ex a st (for b holds (P[a] or Q[b]))
provided
A1: (ex a st P[a]) or (for b holds Q[b])
proof
now
A2:now
given a such that A3:P[a];
for b holds (P[a] or Q[b]) by A3;
hence thesis;
end;
now
assume A4:for b holds Q[b];
consider a;
for b holds (P[a] or Q[b]) by A4;
hence thesis;
end;
hence thesis by A1,A2;
end;
hence thesis;
end;
scheme Schemat18b {P[set],Q[set]} :
(ex a st P[a]) or (for b holds Q[b])
provided
A1: ex a st for b holds (P[a] or Q[b])
proof
consider a such that A2:for b holds (P[a] or Q[b]) by A1;
(ex b st not Q[b]) implies P[a] by A2;
hence thesis;
end;
scheme Schemat19a {P[set],Q[set]} :
for b holds (ex a st (P[a] or Q[b]))
provided
A1: (ex a st P[a]) or (for b holds Q[b]) by A1;
scheme Schemat19b {P[set],Q[set]} :
(ex a st P[a]) or (for b holds Q[b])
provided
A1: for b holds (ex a st (P[a] or Q[b])) by A1;
scheme Schemat20b {P[set],Q[set]} :
ex a st (for b holds (P[a] or Q[b]))
provided
A1: for b ex a st (P[a] or Q[b])
proof
defpred X[set] means P[$1];
defpred Y[set] means Q[$1];
A2: for b ex a st (X[a] or Y[b]) by A1;
A3:(ex a st X[a]) or (for b holds Y[b]) from Schemat19b(A2);
ex a st (for b holds (X[a] or Y[b])) from Schemat18a(A3);
hence thesis;
end;
scheme Schemat21a {P[set],Q[set]} :
ex a st for b holds P[a] & Q[b]
provided
A1: (ex a st P[a]) & (for b holds Q[b]) by A1;
scheme Schemat21b {P[set],Q[set]} :
(ex a st P[a]) & (for b holds Q[b])
provided
A1: ex a st for b holds P[a] & Q[b] by A1;
scheme Schemat22a {P[set],Q[set]} :
for b ex a st (P[a] & Q[b])
provided
A1: (ex a st P[a]) & (for b holds Q[b])
proof
now
let b;
A2:Q[b] by A1;
consider a such that A3:P[a] by A1;
thus ex a st P[a] & Q[b] by A2,A3;
end;
hence thesis;
end;
scheme Schemat22b {P[set],Q[set]} :
(ex a st P[a]) & (for b holds Q[b])
provided
A1: for b ex a st P[a] & Q[b]
proof
assume A2:(for a holds not P[a]) or (ex b st not Q[b]);
A3:now
given b such that A4:not Q[b];
now
let d;
assume d = b;
ex a st P[a] & Q[b] by A1;
hence contradiction by A4;
end;
hence thesis;
end;
now
assume A5:for a holds not P[a];
now
let b;
consider a such that A6:P[a] & Q[b] by A1;
thus thesis by A5,A6;
end;
hence thesis;
end;
hence thesis by A2,A3;
end;
scheme Schemat23b {P[set],Q[set]} :
ex a st for b holds P[a] & Q[b]
provided
A1: for b ex a st P[a] & Q[b]
proof
defpred X[set] means P[$1];
defpred Y[set] means Q[$1];
A2: for b ex a st X[a] & Y[b] by A1;
A3: (ex a st X[a]) & (for b holds Y[b]) from Schemat22b(A2);
ex a st for b holds (X[a] & Y[b]) from Schemat21a(A3);
hence thesis;
end;
scheme Schemat24a {S[set,set],Q[set]} :
for a ex b st (S[a,b] implies Q[a])
provided
A1: for a holds ((for b holds S[a,b]) implies Q[a]) by A1;
scheme Schemat24b {S[set,set],Q[set]} :
for a holds ((for b holds S[a,b]) implies Q[a])
provided
A1: for a ex b st (S[a,b] implies Q[a]) by A1;
scheme Schemat25a {S[set,set],Q[set]} :
for a,b holds (S[a,b] implies Q[a])
provided
A1: for a holds ((ex b st S[a,b]) implies Q[a]) by A1;
scheme Schemat25b {S[set,set],Q[set]} :
for a holds ((ex b st S[a,b]) implies Q[a])
provided
A1: for a,b holds (S[a,b] implies Q[a]) by A1;
scheme Schemat27 {S[set,set]} :
for a holds S[a,a]
provided
A1: for a,b holds S[a,b] by A1;
scheme Schemat28 {S[set,set]} :
ex b st for a holds S[a,b]
provided
A1: for a,b holds S[a,b]
proof
now
let b;
for a holds S[a,b] by A1;
hence thesis;
end;
hence thesis;
end;
scheme Schemat30 {S[set,set]} :
ex a st S[a,a]
provided
A1: ex a st for b holds S[a,b]
proof
consider a such that A2:for b holds S[a,b] by A1;
S[a,a] by A2;
hence thesis;
end;
scheme Schemat31 {S[set,set]} :
for a ex b st S[b,a]
provided
A1: for a holds S[a,a]
proof
let a;
S[a,a] by A1;
hence thesis;
end;
scheme Schemat33 {S[set,set]} :
for a ex b st S[a,b]
provided
A1: for a holds S[a,a]
proof
let a;
S[a,a] by A1;
hence thesis;
end;
scheme Schemat36 {S[set,set]} :
ex a,b st S[a,b]
provided
A1: for b ex a st S[a,b]
proof
consider b;
ex a st S[a,b] by A1;
hence thesis;
end;
scheme Schemat37 {S[set,set]} :
ex a,b st S[a,b]
provided
A1: ex a st S[a,a] by A1;