:: Schemes
:: by Stanis\l aw T. Czuba
::
:: Received December 17, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
begin
reserve a,b,d for set;
scheme
Schemat0 {P[set]} : ex a st P[a]
provided
A1: for a holds P[a]
proof
set a = the set;
P[a] by A1;
hence thesis;
end;
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
thus thesis by A1;
end;
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
thus thesis by A1;
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] by A1;
assume
A2: for a holds Q[a];
for a holds P[a] by A1,A2;
hence thesis;
end;
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 thesis 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
set a = the set;
assume for b holds Q[b];
then for b holds P[a] or Q[b];
hence thesis;
end;
now
given a such that
A3: P[a];
for b holds P[a] or Q[b] by A3;
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
thus thesis by A1;
end;
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
A2: (ex a st P[a]) or for b holds Q[b] by A1;
ex a st for b holds P[a] or Q[b] from Schemat18a(A2);
hence thesis;
end;
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
thus thesis by A1;
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];
per cases by A2;
suppose
ex b st not Q[b];
then consider b such that
A3: not Q[b];
now
let d;
assume d = b;
ex a st P[a] & Q[b] by A1;
hence contradiction by A3;
end;
hence thesis;
end;
suppose
A4: for a holds not P[a];
now
let b;
ex a st ( P[a])& Q[b] by A1;
hence thesis by A4;
end;
hence thesis;
end;
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
A2: for b ex a st P[a] & Q[b] by A1;
(ex a st P[a]) & for b holds Q[b] from Schemat22b(A2);
hence thesis;
end;
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
thus thesis by A1;
end;
scheme
Schemat31 {S[set,set]} : for a ex b st S[b,a]
provided
A1: for a holds S[a,a]
proof
thus thesis by A1;
end;
scheme
Schemat33 {S[set,set]} : for a ex b st S[a,b]
provided
A1: for a holds S[a,a]
proof
thus thesis by A1;
end;
scheme
Schemat36 {S[set,set]} : ex a,b st S[a,b]
provided
A1: for b ex a st S[a,b]
proof
set b = the set;
ex a st S[a,b] by A1;
hence thesis;
end;