:: Schemes
::  by Stanis\l aw T. Czuba
::
:: Received December 17, 1990
:: Copyright (c) 1990-2012 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]
  proof
    assume
A2: for a holds P[a];
    now
      let a;
      P[a] iff Q[a] by A1;
      hence Q[a] by A2;
    end;
    hence thesis;
  end;
  assume
A3: for a holds Q[a];
  now
    let a;
    P[a] iff Q[a] by A1;
    hence P[a] by A3;
  end;
  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;