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