:: Families of Subsets :: by Andrzej Trybulec :: :: Received December 13, 2012 :: Copyright (c) 2012-2018 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; coherence by TARSKI:1; redefine func x`2 -> set; coherence by TARSKI:1; end; definition let x be object; redefine func x`1_3 -> set; coherence by TARSKI:1; redefine func x`2_3 -> set; coherence by TARSKI:1; end; definition let x be object; redefine func x`1_4 -> set; coherence by TARSKI:1; redefine func x`2_4 -> set; 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;