XFAMILY

:: Families of Subsets
::  by Andrzej Trybulec
::
:: Received December 13, 2012
:: Copyright (c) 2012-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

 vocabularies MCART_1, RECDEF_2;
 notations TARSKI, XTUPLE_0;
 constructors TARSKI, XTUPLE_0;
 theorems TARSKI;
 schemes TARSKI;

begin

scheme
  Separation { A()-> set, P[object] } :
  ex X being set st for x being set holds x in X iff x in A() & P[x]
  proof
  defpred Q[object,object] means $1 = $2 & P[$2];
A1: for x,y,z being object st Q[x,y] & Q[x,z] holds y = z;
  consider X being set such that
A2: for x being object holds x in X iff
    ex y being object st y in A() & Q[y,x] from TARSKI:sch 1(A1);
  take X;
  let x be set;
  thus x in X implies x in A() & P[x]
   proof assume x in X;
     then ex y being object st y in A() & Q[y,x] by A2;
    hence thesis;
   end;
  assume x in A() & P[x];
   then ex y being object st y in A() & Q[y,x];
  hence x in X by A2;
end;

scheme
  Extensionality { X,Y() -> set, P[set] } : X() = Y()
provided
A1: for x being set holds x in X() iff P[x] and
A2: for x being set holds x in Y() iff P[x]
proof
A3: for x being object holds x in Y() implies x in X()
   proof let x be object;
     reconsider x as set by TARSKI:1;
     x in Y() implies x in X() by A1,A2;
    hence thesis;
   end;
  for x being object holds x in X() implies x in Y()
   proof let x be object;
     reconsider x as set by TARSKI:1;
     x in X() implies x in Y() by A1,A2;
    hence thesis;
   end;
  hence thesis by A3,TARSKI:2;
end;

scheme
  SetEq { P[set] } :
  for X1,X2 being set st
    (for x being set holds x in X1 iff P[x]) &
    (for x being set holds x in X2 iff P[x]) holds X1 = X2
  proof
  let X1,X2 be set such that
A1: for x being set holds x in X1 iff P[x] and
A2: for x being set holds x in X2 iff P[x];
  thus thesis from Extensionality(A1,A2);
end;

definition let x be object;
 redefine func x`1 -> set;  :: redefines `1 (XTUPLE_0, definition)
 coherence by TARSKI:1;
 redefine func x`2 -> set;  :: redefines `2 (XTUPLE_0, definition)
 coherence by TARSKI:1;
end;

definition
  let x be object;
  redefine func x`1_3 -> set;  :: redefines `1_3 (XTUPLE_0, definition)
  coherence by TARSKI:1;
  redefine func x`2_3 -> set;  :: redefines `2_3 (XTUPLE_0, definition)
  coherence by TARSKI:1;
end;

definition
  let x be object;
  redefine func x`1_4 -> set;  :: redefines `1_4 (XTUPLE_0, definition)
  coherence by TARSKI:1;
  redefine func x`2_4 -> set;  :: redefines `2_4 (XTUPLE_0, definition)
  coherence by TARSKI:1;
end;

:: definition
::   let x1,x2 be element;
::   redefine func [x1,x2] -> set;
::   coherence by TARSKI:1;
:: end;

:: definition
::   let x1,x2,x3 be element;
::   redefine func [x1,x2,x3] -> set;
::   coherence by TARSKI:1;
:: end;