Wikibooks

A Practical Guide To Mizar/Syntax and Sets

< A Practical Guide To Mizar
This page may need to be reviewed for quality.
The Environment A Practical Guide To Mizar
Syntax and Sets 		Bibliography

Axioms

edit

Nowadays everything in the Mizar Mathematical Library is proven based on earlier works. Except of course the axioms. An axiom is an evident truth that needs no proof. Mathematicians try to keep the number of axioms in an axiomatic system low and independent of one another. A commonly used axiomatic system is Zermelo-Fraenkel (ZFC), but Mizar uses Tarski-Grothendieck (TG), which implies ZFC. Hence the axiomatic articles hidden.miz, tarski_0.miz and tarski_a.miz don't contain proofs in opposite to all other MIZ articles.

So what are these axioms?

First, lets call anything we come across in Mizar an object. For any two objects a and b, we can either say that a = b or a <> b (which is the same as not a = b), there is no in-between. The mathematical symbol for <> is "≠". A set is an unordered collection of objects. For any object a and any set A (sets are usually denoted with capital letters), we have either a in A or not a in A. The mathematical symbol for in is "∊". By earlier definition, a set is also an object.

The first axiom states that every object is also a set: 

:: Set axiom
theorem :: TARSKI_0:1
  for x being object holds x is set;

Why differ between objects and sets then? There are reasons, but these are best left to set theorists.

The second axiom states that two sets are equal exactly when they contain the same objects: 

:: Extensionality axiom
theorem :: TARSKI_0:2
  (for x being object holds x in X iff x in Y) implies X = Y;

The third axiom states that for every two objects, there exist a set containing only these two: 

:: Axiom of pair
theorem :: TARSKI_0:3
  for x,y being object ex z being set st
    for a being object holds
      a in z iff a = x or a = y;

The fourth axiom states that the union of a set exists, i.e. the set Z containing all objects x that are in any set Y contained in a given set X: 

:: Axiom of union
theorem :: TARSKI_0:4
  for X being set
   ex Z being set st
    for x being object holds
      x in Z iff ex Y being set st x in Y & Y in X;

The fiveth axiom states that a set X, if it is not empty, must contain a set Y such that no object x is in both X and Y: 

:: Axiom of regularity
theorem :: TARSKI_0:5
  x in X implies ex Y st Y in X & not ex x st x in X & x in Y;

This is a technical axiom that ensures that we don't have something like "a set containing only itself", because these things lead to trouble down the road.

The sixth axiom states that we can get a new set by exchanging objects in a set with other objects. 

:: Fraenkel's scheme
scheme :: TARSKI_0:sch 1
 Replacement { A() -> set, P[object, object] }:
  ex X st for x holds x in X iff ex y st y in A() & P[y,x]
 provided
  for x,y,z being object st P[x,y] & P[x,z] holds y = z;

You can see that this one looks a bit different from the others, scheme instead of theorem etc. Schemes will be explained in Relations and Functions.

The seventh and last axiom is very technical and you don't need to understand it. It basically states that "big" sets with certain properties exist: 

:: Tarski's axiom
theorem :: TARSKI_A:1
  ex M st N in M &
     (for X,Y holds X in M & Y c= X implies Y in M) &
     (for X st X in M ex Z st Z in M & for Y st Y c= X holds Y in Z) &
     (for X holds X c= M implies X,M are_equipotent or X in M);

In practice we will hardly ever use TARSKI_0 or TARSKI_A and instead use TARSKI quite often.

Qualifiers

edit

For this section, this will be the environment used: 

environ
 vocabularies TARSKI;
 notations TARSKI;
 constructors TARSKI;

begin

As seen above, one way to specify a property P holds for all objects of some type is like this: 

theorem
  for X being set holds P[X];

(For this to compile replace P[X] with an actual property like X = X for example.)

The mathematical symbol for for is "∀".

If you have several objects you can specify them like: 

theorem
  for X being set for Y being set holds P[X,Y];

This can be shortened to: 

theorem
  for X being set, Y being set holds P[X,Y];

And in case you have several object of the same type, you can shorten it further to: 

theorem
  for X, Y being set holds P[X, Y];

With the use of reserve you can shorten it even more like: 

reserve X, Y for set;

theorem
  for X for Y holds P[X, Y];

theorem
  for X, Y holds P[X, Y];

theorem
  for X holds P[X];

And finally, Mizar can infer the types from reserve, so you leave out the for: 

reserve X, Y for set;

theorem
  P[X, Y];

theorem
  P[X];

Similarly, to specify that an object (or several) of some type fulfilling a property P exists, one can use any of the following styles: 

theorem
  ex X being set st P[X];

theorem
  ex X being set st ex Y being set st P[X, Y];

theorem
  ex X being set ex Y being set st P[X, Y];

theorem
  ex X being set, Y being set st P[X, Y];

theorem
  ex X, Y being set st P[X, Y];

reserve X, Y for set;

theorem
  ex X st P[X];

theorem
  ex X st ex Y st P[X, Y];

theorem
  ex X ex Y st P[X, Y];

theorem
  ex X, Y st P[X, Y];

The mathematical symbol for ex is "∃".

When we want to prove these theorems, the corresponding syntax looks like this: 

theorem
  for X being set holds P[X]
proof
  let X be set;
  thus P[X];
end;

theorem
  ex X being set st P[X]
proof
  reconsider X = [something] as set;
  take X;
  thus P[X];
end;

where [something] is an expression of some kind. The reconsider line is not necessarily needed if X is already known as the needed type (a set in this case) or a subtype thereof. take is surprisingly flexible, which we will see later. For example, in case [something] is recognized to be of the needed type, we can drop the reconsider line and replace all X following afterwards with [something].

In case of several quantifiers of the same kind you can mix and match the following syntax: 

theorem
  for X being set holds for Y being holds P[X, Y]
proof
  let X be set;
  let Y be set;
  thus P[X, Y];
end;

theorem
  for X being set for Y being set holds P[X, Y]
proof
  let X be set, Y be set;
  thus P[X, Y];
end;

theorem
  for X being set, Y being set holds P[X, Y]
proof
  let X be set, Y be set;
  thus P[X, Y];
end;

theorem
  for X, Y being set holds P[X, Y]
proof
  let X, Y be set;
  thus P[X, Y];
end;

theorem
  ex X being set st ex Y being set st P[X, Y]
proof
  reconsider X = [something1] as set;
  take X;
  reconsider Y = [something2] as set;
  take Y;
  thus P[X, Y];
end;

theorem
  ex X being set ex Y being set st P[X, Y]
proof
  reconsider X = [something1] as set;
  reconsider Y = [something2] as set;
  take X, Y;
  thus P[X, Y];
end;

theorem
  ex X being set, Y being set st P[X,Y]
proof
  reconsider X = [something1] as set, Y = [something2] as set;
  take X, Y;
  thus P[X, Y];
end;

theorem
  ex X, Y being set st P[X, Y]
proof
  reconsider X = [something1] as set, Y = [something2] as set;
  take X, Y;
  thus P[X, Y];
end;

With the reserve keyword the proofs can become even shorter: 

reserve X, Y for set;

theorem
  for X for Y holds P[X, Y]
proof
  let X;
  let Y;
  thus P[X, Y];
end;

theorem
  for X, Y holds P[X, Y]
proof
  let X, Y;
  thus P[X, Y];
end;

theorem
  P[X, Y]
proof
  thus P[X, Y]; :: i.e. no let required at all
end;

theorem
  ex X st ex Y st P[X, Y]
proof
  reconsider X = [something1] as set;
  take X;
  reconsider Y = [something2] as set;
  take Y;
  thus P[X, Y];
end;

theorem
  ex X ex Y st P[X, Y]
proof
  reconsider X = [something1] as set;
  reconsider Y = [something2] as set;
  take X, Y;
  thus P[X, Y];
end;

theorem
  ex X, Y st P[X, Y]
proof
  reconsider X = [something1] as set;
  reconsider Y = [something2] as set;
  take X, Y;
  thus P[X, Y];
end;

If we want to use these theorems, we do it like this: 

theorem Th1:
  for X, Y being set holds P1[X, Y];

theorem Th2:
  ex X, Y being set st P2[X, Y];

theorem
  ex X, Y being set st P1[X, Y];
proof
  consider X, Y being set such that
    A1: P2[X, Y] by Th2;
  take X, Y;
  thus P1[X, Y] by Th1;
end;

Let's look a bit closer at this example. Theorems (as well as lemmata, which are like theorems but without the theorem keyword) can be given labels. Usually these are given names like Th1 (and Lm1), but anything not a keyword can be used. We can use a for statement simply by using the by keyword and the label of the theorem to use, but to use a ex statement we need syntax in the form consider … such that in connection with the by reference of the theorem.

The empty set and basic set operations

edit

For this section, this will be the environment used: 

environ
 vocabularies TARSKI, XBOOLE_0;
 notations TARSKI, XBOOLE_0;
 constructors TARSKI, XBOOLE_0;
 theorems TARSKI, XBOOLE_0;

begin

The first definition of XBOOLE_0 is the property of a set to be empty, i.e. not containing any elements (x is reserved as an object at this point): 

definition
  let X be set;
  attr X is empty means
:: XBOOLE_0:def 1

  not ex x st x in X;
end;

A property P an object A of a certain type can have is defined using the attr A is P means construct (followed by the definiens). attr is short for "attribute", which will be used instead of this kind of property from now on.

Note that this definition compiles if you copy it. This is because attributes can be defined with any definiens, even if it can never be fulfilled. A nonsense definition could be for example: 

definition
  let x be object;
  attr x is empty means
  contradiction;
end;

You can use that definition in theorems like for x being object st x is empty holds P[x];, no matter what P[x] is (for example x <> x). That statement will be readily accepted by the checker because it sees that x is empty is a contradiction, and we can infer anything from a contradiction.

Let's agree to avoid nonsense attribute definitions.

To show that an attribute can indeed be fulfilled, one can use a so-called existential cluster registration. The one in XBOOLE_0 following the empty definition reads: 

registration
  cluster empty for set;
end;

When you try to copy this registration from the abstract of XBOOLE_0 to your article, the parser will complain with a *73 error that a correctness condition is missing. To get rid of this error, we can add a proof skeleton like this: 

registration
  cluster empty for set;
  existence
  proof
    thus ex X being set st X is empty;
  end;
end;

That will now compile with the exception of *4, marking the actual proof as missing. We will not prove the existence here, it basically follows from Fraenkel's scheme. The interested reader can check it out in XBOOLE_0.

Now that the empty attribute is clustered for sets, we can use expressions like for X being empty set …, reserve X for empty set or the empty set. The latter describes the empty set that was used to prove the existence of empty sets, but it should be thought of "an arbitrary empty set".

Set operations are ways to generate new sets from existing ones. The arity of an operation indicates how many input parameters are needed to produce the output. The next definition in XBOOLE_0 is a nullary set operation and reads: 

definition
  func {} -> set equals
:: XBOOLE_0:def 2
  the empty set;
end;

Since the output of this operation (right side of the ->) is a set as well as the definiens, we don't have to prove anything here and the compiler will be satisfied with the form: 

definition
  func {} -> set equals
:: XBOOLE_0:def 2
  the empty set;
  coherence;
end;

func is short for "functor". In mathematical notation, the symbol "∅" is sometimes used instead of "{}". XBOOLE_0 also contains the functional cluster registration: 

registration
  cluster {} -> empty;
end;

which will be accepted with a coherence condition added in XBOOLE_0 because the checker can see inside the definition that was made in the same article, unlike definitions made in other articles (without additional environment work). Clusters are an easy way to add attribute inferences to the checker without having to cite a specific theorem with by: Just add other articles to your article environment behind the registrations keyword and all registrations (existential, functional and conditional) from these articles will be added to yours. For pure sets this is not very powerful, but that will change with Relations and Functions.

The set that only contains a certain object y, or "{y}" in short, is an unary operator and the first definition in TARSKI: 

definition
  let y be object;
  func { y } -> set means
:: TARSKI:def 1
  for x being object holds x in it iff x = y;
end;

it is the placeholder for the object we are defining. Since our functor definition doesn't use equals but means here, we have different correctness conditions, that are: 

definition
  let y be object;
  func { y } -> set means
:: TARSKI:def 1
  for x being object holds x in it iff x = y;
  existence
  proof
    thus ex Y being set st for x being object holds x in Y iff x = y;
  end;
  uniqueness
  proof
    thus for Y1, Y2 being set st
      (for x being object holds x in Y1 iff x = y) &
      (for x being object holds x in Y2 iff x = y)
    holds Y1 = Y2;
  end;
end;

Both existence and uniqueness are proven in TARSKI using the axioms. existence means an object of the correct type (right of ->) fulfilling the definiens must exist. uniqueness means if two objects of the same type fulfill the definiens, they must be the same. If we want to only guarantee existence but not uniqueness, we can use a mode instead, which defines a subtype of a given type fulfilling a certain definiens. object and set are modes, but their existence is not proven, instead taken as an axiom of Mizar. They are defined in HIDDEN and can automatically used in any article (HIDDEN is included automatically).

In XBOOLE_0 there is a functional cluster saying that {y} is non empty.

It is very important to understand that a set X is not the same as the set containing only X. The former does not contain X (because of the Regularity Axiom) and the latter does, making them different. Math beginners often don't get the difference when X is the empty set, but we can in fact prove that {{}} <> {}: 

{{}} <> {}
proof
  {} in {{}} by TARSKI:def 1;
  hence thesis by XBOOLE_0:def 1;
end;

In the second line of the proof we use that the empty set doesn't contain any elements, not even itself, but since {{}} does contain an element (proven in the line before, the element being the empty set), they cannot be the same. Also note that instead of then thus we write hence. thesis is a placeholder for the statement we are currently proving. The use of then means "use the statement from the previous line in your reasoning". It is the same as writing: 

{{}} <> {}
proof
  A1: {} in {{}} by TARSKI:def 1;
  thus thesis by A1, XBOOLE_0:def 1;
end;

Similar to TARSKI:def 1 we have the next definition in TARSKI, just this time as a binary operator: 

definition
  let y, z be object;
  func { y, z } -> set means
:: TARSKI:def 2
  x in it iff x = y or x = z;
  commutativity;
end;

commutativity means that {y,z} is the same as {z,y}, which is apparent from the definition, since the logical arguments of or commute as well. For the parser existence and uniqueness are needed again, as they always are with the func … -> … means construct.

In XBOOLE_0 there is a functional cluster saying that {y, z} is non empty.

If you are looking for more sets defined explicitly by their concrete elements, check out ENUMSET1.

XBOOLE_0 gives us more binary set operations: 

definition
  let X,Y be set;
  func X \/ Y -> set means
:: XBOOLE_0:def 3

  for x holds x in it iff x in X or x in Y;
  commutativity;
  idempotence;
  func X /\ Y -> set means
:: XBOOLE_0:def 4

  for x holds x in it iff x in X & x in Y;
  commutativity;
  idempotence;
  func X \ Y -> set means
:: XBOOLE_0:def 5 

  for x holds x in it iff x in X & not x in Y;
end;

definition
  let X, Y be set;
  func X \+\ Y -> set equals
:: XBOOLE_0:def 6
  (X \ Y) \/ (Y \ X);
  commutativity;
end;

idempotence means that if both parameters are the same, the output is the same as well. The idempotence for X \/ Y and X /\ Y is apparent from their definiens because the logical operations or and & (which means "and") are idempotent as well. X \/ Y is the union of X and Y (also written as "X ∪ Y"), X /\ Y is the intersection of X and Y (also written as "X ∩ Y"). X \ Y is the difference of X and Y (sometimes written as "X - Y"). Note that it is neither marked as commutative nor as idempotent, because it doesn't fulfill these properties in general, as we will prove below. X \+\ Y is the symmetric difference of X and Y (sometimes written as "X ∆ Y", "X ⊕ Y" or "X ⊖ Y"). It is commutative (again apparent from the definition because X \/ Y is), but not idempotent. Note that we can put several definitions into one definition block but we had to use another for X \+\ Y so we could use the previous definitions in its definiens.

Union and intersection are associative, i.e. 

for A, B, C being set holds A \/ B \/ C = A \/ (B \/ C) & A /\ B /\ C = A /\ (B /\ C)

Note that Mizar reads operations from left to right, so A \/ B \/ C is the same as (A \/ B) \/ C. The associativity of the two operations follows directly from the definitions because the logical operators or and & are associative. However, to prove this in Mizar, a little bit of work is necessary. For example: 

for A, B, C being set holds A \/ B \/ C = A \/ (B \/ C)
proof
  let A, B, C be set;
  for x being object holds x in A \/ B \/ C iff x in A \/ (B \/ C)
  proof
    let x be object;
    thus x in A \/ B \/ C implies x in A \/ (B \/ C)
    proof
      assume x in A \/ B \/ C;
      then x in A \/ B or x in C by XBOOLE_0:def 3;
      then x in A or x in B or x in C by XBOOLE_0:def 3;
      then x in A or x in B \/ C by XBOOLE_0:def 3;
      hence x in A \/ (B \/ C) by XBOOLE_0:def 3;
    end;
    thus x in A \/ (B \/ C) implies x in A \/ B \/ C
    proof
      assume x in A \/ (B \/ C);
      then x in A or x in B \/ C by XBOOLE_0:def 3;
      then x in A or (x in B or x in C) by XBOOLE_0:def 3;
      then x in A \/ B or x in C by XBOOLE_0:def 3;
      hence x in A \/ B \/ C by XBOOLE_0:def 3;
    end;
  end;
  hence thesis by TARSKI:2;
end;

We can see that this is mostly work with definitions. One can spot that we didn't write e.g.: 

then x in A or x in B or x in C by XBOOLE_0:def 3;
then x in A or (x in B or x in C);

because Mizar is able to do that step itself (as it is often the case when no by or from keyword is used). Furthermore, that means it didn't matter if we wrote x in A or x in B or x in C or x in A or (x in B or x in C) in either of these places.

About the notation: We used TARSKI:2 here which reads 

theorem :: TARSKI:2 :: Extensionality
  (for x being object holds x in X iff x in Y) implies X = Y;

We wanted to use the part X = Y, which means we had to supply the part before the implies. That is why we have the statement: 

for x being object holds x in A \/ B \/ C iff x in A \/ (B \/ C)

in our proof and continued to prove that statement "instead" of A \/ B \/ C = A \/ (B \/ C). For two statements P, Q the statement P iff Q is equivalent to (P implies Q) & (Q implies P). To prove a statement of the form R & S for two statements R, S, we write it like this: 

R & S
proof
  thus R;
  thus S;
end;

Exercise 1: Prove A /\ B /\ C = A /\ (B /\ C), based on the proof above and using XBOOLE_0:def 4 instead.

If you want to use them, the associativity laws are in the MML under XBOOLE_1:4 and XBOOLE_1:16 respectively.

Another important property that can be directly inferred from the logical operations behind the union and intersection is the distributivity. We have (A /\ B) \/ C = (A /\ C) \/ (B /\ C) and (A \/ B) /\ C = (A \/ C) /\ (B \/ C): 

for A, B, C being set holds (A \/ B) /\ C = (A /\ C) \/ (B /\ C)
proof
  let A, B, C be set;
  for x being object holds x in (A \/ B) /\ C iff x in (A /\ C) \/ (B /\ C)
  proof
    let x be object;
    thus x in (A \/ B) /\ C implies x in (A /\ C) \/ (B /\ C)
    proof
      assume x in (A \/ B) /\ C;
      then x in A \/ B & x in C by XBOOLE_0:def 4;
      then (x in A or x in B) & x in C by XBOOLE_0:def 3;
      then (x in A & x in C) or x in B /\ C by XBOOLE_0:def 4;
      then x in A /\ C or x in B /\ C by XBOOLE_0:def 4;
      hence x in (A /\ C) \/ (B /\ C) by XBOOLE_0:def 3;
    end;
    thus x in (A /\ C) \/ (B /\ C) implies x in (A \/ B) /\ C
    proof
      assume x in (A /\ C) \/ (B /\ C);
      then x in A /\ C or x in B /\ C by XBOOLE_0:def 3;
      then x in A /\ C or (x in B & x in C) by XBOOLE_0:def 4;
      then (x in A & x in C) or (x in B & x in C) by XBOOLE_0:def 4;
      then x in A \/ B & x in C by XBOOLE_0:def 3;
      hence x in (A \/ B) /\ C by XBOOLE_0:def 4;
    end;
  end;
  hence thesis by TARSKI:2;
end;

Again it doesn't matter if we write (x in A or x in B) & x in C or (x in A & x in C) or (x in B & x in C); Mizar can exchange these expressions by itself.

Exercise 2: Prove (A /\ B) \/ C = (A \/ C) /\ (B \/ C) based on the proof above.

If you want to use them, the distributivity laws are in the MML under XBOOLE_1:23 and XBOOLE_1:24 respectively.

We have now seen some examples of a direct proof, but sometimes a proof by contradiction is easier to write. Let's proof X \/ Y = {} implies X = {} (XBOOLE_1:15): 

for X, Y being set holds X \/ Y = {} implies X = {}
proof
  let X, Y be set;
  assume A1: X \/ Y = {};
  assume X <> {};
  then consider x being object such that
    A2: x in X by XBOOLE_0:7;
  x in X \/ Y by A2, XBOOLE_0:def 3;
  hence contradiction by A1, XBOOLE_0:def 1, XBOOLE_0:def 2;
end;

So instead of showing that X = {} we assume the opposite (X <> {}) and lead that to a contradiction with another assumption. Since all steps since assuming the opposite were correct, our opposite assumption must have been wrong (or math is not contradiction-free, which would be the discovery of the millennium). XBOOLE_0:7 itself follows from the definition of the empty set and reads: 

theorem :: XBOOLE_0:7
X <> {} implies ex x st x in X;

Therefore we can use the consider … such that construct as discussed in the previous section. Note that we cannot use then after a consider, we have to work with labels. When X in X it is also true that x in X or x in Y, so we can go to the next step showing that x in X \/ Y via XBOOLE_0:def 3. That set however was assumed to be empty, hence we get our contradiction after throwing in the definition of the empty set and {}. We could have omitted XBOOLE_0:def 2 if we had registrations XBOOLE_0; in our environment, since then Mizar would have inferred by itself (using the cluster discussed above) that {} is indeed empty.

Note that we don't need a theorem for X, Y being set holds X \/ Y = {} implies Y = {} because X \/ Y is commutative, i.e. Mizar can infer that on its own given XBOOLE_1:15.

Exercise 3: Prove X /\ {} = {} by contradiction.

Exercise 4: Prove X \ X = {} by contradiction. This shows that the difference of sets is not idempotent.

We will now prove that X \+\ X = {} directly, using Exercise 4 (labelled Ex4). This shows that the symmetric difference of sets is not idempotent: 

for X being set holds X \+\ X = {}
proof
  let X be set;
  thus X \+\ X = (X \ X) \/ (X \ X) by XBOOLE_0:def 6
    .= {} \/ (X \ X) by Ex4
    .= {} \/ {} by Ex4
    .= {};
end;

What we did here was using an equality chain. After the first = and the justification with by or from we don't add a semicolon but instead a .=. We repeat that until we reach what we wanted to reach, in this case {} (the last step Mizar infers from the idempotence of the union of sets). This is syntactical sugar, we could also just write: 

for X being set holds X \+\ X = {}
proof
  let X be set;
  X \+\ X = (X \ X) \/ (X \ X) by XBOOLE_0:def 6;
  then X \+\ X = {} \/ (X \ X) by Ex4;
  then X \+\ X = {} \/ {} by Ex4;
  hence X \+\ X = {};
end;

But one form is easier to read than the other.

To see that the difference of sets is not symmetric, we prove a <> b implies {a,b} \ {a} = {b} and leave the other variant to the reader: 

for a,b being object holds a <> b implies {a,b} \ {a} = {b}
proof
  let a,b be object;
  assume A1: a <> b;
  for x being object holds x in {a,b} \ {a} iff x = b
  proof
    let x be object;
    thus x in {a,b} \ {a} implies x = b
    proof
      assume x in {a,b} \ {a};
      then x in {a,b} & not x in {a} by XBOOLE_0:def 5;
      then (x = a or x = b) & not x in {a} by TARSKI:def 2;
      then (x = a or x = b) & x <> a by TARSKI:def 1;
      hence x = b;
    end;
    thus x = b implies x in {a,b} \ {a}
    proof
      assume x = b;
      then x in {a,b} & x <> a by A1, TARSKI:def 2;
      then x in {a,b} & not x in {a} by TARSKI:def 1;
      hence x in {a,b} \ {a} by XBOOLE_0:def 5;
    end;
  end;
  hence thesis by TARSKI:def 1;
end;

Exercise 5: Prove {a} \ {a,b} = {}.

Note that we only need the condition a <> b in the former statement. That is because, if we had a = b, then {a,b} = {a,a} = {a} (by ENUMSET1:29) and therefore {a,b} \ {a} = {} (by Ex4). Since we already know that {b} <> {}, we have proven that the set difference is not symmetric in general.

Note that the symmetric set difference is associative (XBOOLE_1:91).

Ordered Pairs and the Cartesian Product

edit

For this section, this will be the environment used: 

environ
 vocabularies TARSKI, XBOOLE_0, ZFMISC_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1;
 constructors TARSKI, XBOOLE_0, ZFMISC_1;
 registrations XBOOLE_0;
 requirements BOOLE;
 theorems TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0;

begin

The registrations XBOOLE_0; was commented on in the previous section. requirements BOOLE; ensures that Mizar automatically understands how the empty set interacts with the basic set operations from XBOOLE_0.

We noted in the previous section that {x,y} commutes, i.e. {x,y} = {y,x}. This is why {x,y} is also called an unordered pair. But there are many circumstances when we would want an ordered pair, such that [x,y] = [y,x] iff x = y. There are actually several ways to describe such a pair mathematically, but for now we will be satisfied with the fundamental one from TARSKI: 

definition
  let x,y be object;
  func [x,y] -> object equals
:: TARSKI:def 5
  { { x,y }, { x } };
end;

x = y implies [x,y] = [y,x] is understood by Mizar intrinsically. The other direction is given by the stronger: 

theorem :: XTUPLE_0:1
  [x1,x2] = [y1,y2] implies x1 = y1 & x2 = y2;

We can now define the Cartesian product of two sets as follows: 

definition
  let X,Y;
  func [: X,Y :] -> set means
:: ZFMISC_1:def 2

  z in it iff ex x,y st x in X & y in Y & z = [x,y];
end;

[: X,Y :] is usually written as "X ⨯ Y" in mathematical notation, the pair [x,y] is usually written as "(x,y)" or "⟨x,y⟩". We can also define for example triples, quadruples (which is done in XTUPLE_0 and ZFMISC_1) and more, but pairs will be enough for a while.

To understand new definitions it is often helpful to see some simple examples.

Exercise 6: Prove [:{x},{y}:] = {[x,y]} (ZFMISC_1:29) using TARSKI:def 1 and ZFMISC_1:def 2.

We will use the next example to show how to write proofs with or: 

for x,y,z being object holds [:{x},{y,z}:] = {[x,y],[x,z]}
proof
  let x,y,z be object;
  for p being object holds p in [:{x},{y,z}:] iff p = [x,y] or p = [x,z]
  proof
    let p be object;
    thus p in [:{x},{y,z}:] implies p = [x,y] or p = [x,z]
    proof
      assume p in [:{x},{y,z}:];
      then consider a,b being object such that
        A1: a in {x} & b in {y,z} & p = [a,b] by ZFMISC_1:def 2;
      a = x & (b = y or b = z) by A1, TARSKI:def 1, TARSKI:def 2;
      hence thesis by A1;
    end;
    thus p = [x,y] or p = [x,z] implies p in [:{x},{y,z}:]
    proof
      assume p = [x,y] or p = [x,z];
      then per cases;
      suppose A2: p = [x,y];
        x in {x} & y in {y,z} by TARSKI:def 1, TARSKI:def 2;
        hence thesis by A2, ZFMISC_1:def 2;
      end;
      suppose A3: p = [x,z];
        x in {x} & z in {y,z} by TARSKI:def 1, TARSKI:def 2;
        hence thesis by A3, ZFMISC_1:def 2;
      end;
    end;
  end;
  hence thesis by TARSKI:def 2;
end;

Given a statement of the form P or Q we can use the per cases construct in combination with the keyword suppose: 

P or Q;
then per cases;
suppose P;
  thus thesis;
end;
suppose Q;
  thus thesis;
end;

It is also possible to exclude a case, like this: 

P or Q;
then per cases;
suppose P;
  thus thesis;
end;
suppose Q & not P;
  thus thesis;
end;

When we want to prove a statement P or Q we can either do it directly as in the example above, if Mizar is up to it, or we can do it like this: 

P or Q
proof
  assume not P;
  thus Q;
end;

Exercise 7: Prove [:{x,y},{z}:] = {[x,z],[y,z]} based on the proof above.

The previous two statements can be found under ZFMISC_1:30.

It's also often a good exercise to see how something new interacts with something already known.

Exercise 8: Prove [:X \/ Y, Z:] = [:X, Z:] \/ [:Y, Z:]. This statement together with [:Z, X \/ Y:] = [:Z, X:] \/ [:Z, Y:] can be found under ZFMISC_1:97.

Exercise 9: Prove [:Z, X /\ Y:] = [:Z, X:] /\ [:Z , Y:]. This statement together with [:X /\ Y, Z:] = [:X, Z:] /\ [:Y, Z:] can be found under ZFMISC_1:99.

Exercise 10: Prove [:X \ Y, Z:] = [:X, Z:] \ [:Y, Z:]. This statement together with [:Z, X \ Y:] = [:Z, X:] \ [:Z, Y:] can be found under ZFMISC_1:102.

Note that a Cartesian product is empty if and only if at least one of its factors is (ZFMISC_1:90). Also note that the Cartesian product is neither commutative (cf. ZFMISC_1:110) nor idempotent (cf. ZFMISC_1:93).

Subsets and the power set

edit

For this section, this will be the environment used: 

environ
 vocabularies TARSKI, XBOOLE_0, ZFMISC_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1;
 constructors TARSKI, XBOOLE_0, ZFMISC_1;
 registrations XBOOLE_0;
 requirements BOOLE;
 theorems TARSKI, XBOOLE_0, ZFMISC_1, XBOOLE_1;

begin

We have a couple of ways now to generate new sets from old ones. However, the only way we have to relate these sets to each other is via = and <>. Time to introduce the subset predicate: 

definition
  let X,Y be set;
  pred X c= Y means
:: TARSKI:def 3
  for x being object holds x in X implies x in Y;
  reflexivity;
end;

Read as "X is a subset of Y". pred is short for predicate. X c= Y is usually written as "X ⊂ Y" or "X ⊆ Y" in mathematical notation. reflexivity means that X c= X always holds and that Mizar can recognize that. Again the reflexivity is pretty obvious from the definition when we replace Y with X.

The reflexivity is also indicating that a set is a subset of itself, which may sound a bit unneeded but does in fact help a lot with mathematical statements. If we want to exclude the reflexivity case, we can use the notation for a proper subset: 

definition
  let X,Y be set;
  pred X c< Y means
:: XBOOLE_0:def 8

  X c= Y & X <> Y;
  irreflexivity;
  asymmetry;
end;

Read as "X is a proper subset of Y". X c< Y is usually written as "X ⊊ Y" or "X ⊂ Y" in mathematical notation. The reader will have noticed that "X ⊂ Y" can mean both, subset and proper subset. The difference depends on the author of the work one is reading and is usually cleared early on. irreflexivity means that X c< X can never happen and Mizar can recognize that. asymmetry means that X c< Y always implies not Y c< X.

An imminent property of the subset property is that the empty set is a subset of every set: 

theorem :: XBOOLE_1:2
  {} c= X;

Mizar can recognize this immediately from the definition of the empty set and the subset predicate because it is vacuously true: for x being object holds x in {} implies x in Y is true because x in {} is false and we can follow anything from a false statement.

Another easy corollary of the subset predicate is the so-called "modus barbara": 

theorem :: XBOOLE_1:1
  X c= Y & Y c= Z implies X c= Z;

Such a property is also called transitivity. Mizar can infer XBOOLE_1:1 from the definition of the subset predicate as well because the logical implies used in TARSKI:def 3 is also transitive (i.e. for three statements A,B,C we have (A implies B) & (B implies C) implies (A implies C)). Note that c< is transitive as well (XBOOLE_1:56).

Some more easy observations are X c= X \/ Y (XBOOLE_1:7) and X /\ Y c= X (XBOOLE_1:17). Add in the transitivity and we immediately get X /\ Y c= X \/ Z (XBOOLE_1:29). A slightly more difficult example would be XBOOLE_1:8: 

for X,Y,Z being set holds X c= Z & Y c= Z implies X \/ Y c= Z
proof
  let X,Y,Z be set;
  assume A1: X c= Z & Y c= Z;
  for x being object st x in X \/ Y holds x in Z
  proof
    let x be object;
    assume x in X \/ Y;
    then per cases by XBOOLE_0:def 3;
    suppose x in X;
      hence x in Z by A1, TARSKI:def 3;
    end;
    suppose x in Y;
      hence x in Z by A1, TARSKI:def 3;
    end;
  end;
  hence thesis by TARSKI:def 3;
end;

Exercise 11: Prove Z c= X & Z c= Y implies Z c= X /\ Y (XBOOLE_1:19).

Two important statements are the Absorption laws: X c= Y implies X \/ Y = Y & X /\ Y = X (XBOOLE_1:12, 28): 

for X,Y being set holds X c= Y implies X /\ Y = X
proof
  let X,Y be set;
  assume A1: X c= Y;
  for x being object holds x in X iff x in X & x in Y
  proof
    let x be object;
    thus x in X implies x in X & x in Y by A1, TARSKI:def 3;
    thus x in X & x in Y implies x in X; :: Mizar can recognize this without reference
  end;
  hence thesis by XBOOLE_0:def 4;
end;

Exercise 12: Prove X c= Y implies X \/ Y = Y (XBOOLE_1:12).

Exercise 13: Prove X c= Y implies X \ Z c= Y \ Z & Z \ Y c= Z \ X (XBOOLE_1:33, 34). For the second part you can use the fact that for statements P,Q holds (P implies Q) iff (not Q implies not P). Use that with TARSKI:def 3.

Exercise 14: Prove X1 c= Y1 & X2 c= Y2 implies [:X1,X2:] c= [:Y1,Y2:] (ZFMISC_1:96).

If you look close at the definition of the subset predicate, you will notice that it's very close to the equality of sets (TARSKI:2). And indeed: 

definition
  let X,Y be set;
  redefine pred X = Y means
:: XBOOLE_0:def 10
  X c= Y & Y c= X;
end;

redefine means that an existing attr, pred, mode or func (if properly imported via notations) is getting overwritten with an equivalent definition that might be more practical to use. It's very close to a simple theorem.

Another unary set operation is the power set, which contains all subsets of a given set: 

definition
  let X be set;
  func bool X -> set means
:: ZFMISC_1:def 1

  Z in it iff Z c= X;
end;

where Z is reserved as a set. bool X is written as "P(X)" or "2X" in mathematical notation. Its existence follows from the Tarski-Axiom. Observe ZFMISC_1:1: 

bool {} = { {} }
proof
  for x being object holds x in bool {} iff x = {}
  proof
    let x be object;
    reconsider X = x as set by TARSKI:1;
    hereby
      assume x in bool {};
      then X c= {} by ZFMISC_1:def 1;
      hence x = {} by XBOOLE_1:3;
    end;
    assume x = {};
    hence x in bool {} by ZFMISC_1:def 1, XBOOLE_1:2;
  end;
  hence thesis by TARSKI:def 1;
end;

As we have discussed earlier, this means that the power set of the empty set is not empty. The hereby construct is a placeholder for thus … where the … is the statement inferred from the keywords until the closing end;, so in this case … is x in bool {} implies x = {}. There is a variant without thus: now instead of hereby. In both cases you cannot use thesis to refer to the current statement to be proven.

Exercise 15: Prove bool { x } = { {} , { x }} (ZFMISC_1:24) using now and hereby.

Exercise 16: Prove A c= B implies bool A c= bool B (ZFMISC_1:67) using now and hereby.

As you can see, using now and hereby can make the code more compact. If this affects readability positively or negatively depends: It's especially good for short lemmata within a proof but less than optimal for very long lemmata.

Since the empty set and the original set itself are both a subset of the original set, the power set always contains those two elements. If the original set 'is' the empty set, those elements are the same. As a corollary, a power set is never empty.

Speaking of elements, it would be nice to have a type to specify something is an element of a set instead of writing for x being object st x in X. There is indeed such a mode, there is just one catch: modes must be inhabited, i.e. existence needs to be proven, but there is no element in the empty set! One way would be to define the mode only for non empty sets, but then many theorems would become more verbose. Instead, the MML gets around the problem by defining a default Element for the empty set: 

definition
  let X be set;
  mode Element of X -> set means
:: SUBSET_1:def 1
  it in X if X is non empty otherwise it is empty;
  sethood;
end;

So we end up with the situation where both not {} in {} and {} is Element of {} are true. Don't worry about it, the second variant basically never comes up. The if … otherwise construct is a convenient way to split up definitions. sethood means all instances of this mode form a set and can be used in Fraenkel operators (more about those in Relations and Functions).

A mode for subsets is defined in SUBSET_1 as well: 

definition
  let X be set;
  mode Subset of X is Element of bool X;
end;

Note that the otherwise part of the definition doesn't come into play here because the power set is never empty. We also get the definition of proper subsets: 

definition
  let E be set;
  let A be Subset of E;
  attr A is proper means
:: SUBSET_1:def 6
  A <> E;
end;

The equivalence between the Subset mode and the c= predicate as well as the Element mode and the in predicate are given via the SUBSET requirement.

Exercise Solutions

edit

Exercise 1: 

for A, B, C being set holds A /\ B /\ C = A /\ (B /\ C)
proof
  let A, B, C be set;
  for x being object holds x in A /\ B /\ C iff x in A /\ (B /\ C)
  proof
    let x be object;
    thus x in A /\ B /\ C implies x in A /\ (B /\ C)
    proof
      assume x in A /\ B /\ C;
      then x in A /\ B & x in C by XBOOLE_0:def 4;
      then x in A & x in B & x in C by XBOOLE_0:def 4;
      then x in A & x in B /\ C by XBOOLE_0:def 4;
      hence x in A /\ (B /\ C) by XBOOLE_0:def 4;
    end;
    thus x in A /\ (B /\ C) implies x in A /\ B /\ C
    proof
      assume x in A /\ (B /\ C);
      then x in A & x in B /\ C by XBOOLE_0:def 4;
      then x in A & (x in B & x in C) by XBOOLE_0:def 4;
      then x in A /\ B & x in C by XBOOLE_0:def 4;
      hence x in A /\ B /\ C by XBOOLE_0:def 4;
    end;
  end;
  hence thesis by TARSKI:2;
end;

Exercise 2: 

for A, B, C being set holds (A /\ B) \/ C = (A \/ C) /\ (B \/ C)
proof
  let A, B, C be set;
  for x being object holds x in (A /\ B) \/ C iff x in (A \/ C) /\ (B \/ C)
  proof
    let x be object;
    thus x in (A /\ B) \/ C implies x in (A \/ C) /\ (B \/ C)
    proof
      assume x in (A /\ B) \/ C;
      then x in A /\ B or x in C by XBOOLE_0:def 3;
      then (x in A & x in B) or x in C by XBOOLE_0:def 4;
      then (x in A or x in C) & x in B \/ C by XBOOLE_0:def 3;
      then x in A \/ C & x in B \/ C by XBOOLE_0:def 3;
      hence x in (A \/ C) /\ (B \/ C) by XBOOLE_0:def 4;
    end;
    thus x in (A \/ C) /\ (B \/ C) implies x in (A /\ B) \/ C
    proof
      assume x in (A \/ C) /\ (B \/ C);
      then x in A \/ C & x in B \/ C by XBOOLE_0:def 4;
      then x in A \/ C & (x in B or x in C) by XBOOLE_0:def 3;
      then (x in A or x in C) & (x in B or x in C) by XBOOLE_0:def 3;
      then x in A /\ B or x in C by XBOOLE_0:def 4;
      hence x in (A /\ B) \/ C by XBOOLE_0:def 3;
    end;
  end;
  hence thesis by TARSKI:2;
end;

Exercise 3: 

for X being set holds X /\ {} = {}
proof
  let X be set;
  assume X /\ {} <> {};
  then consider x being object such that
    A1: x in X /\ {} by XBOOLE_0:7;
  x in {} by A1, XBOOLE_0:def 4;
  hence contradiction by XBOOLE_0:def 1, XBOOLE_0:def 2;
end;

Exercise 4: 

Ex4: for X being set holds X \ X = {}
proof
  let X be set;
  assume X \ X <> {};
  then consider x being object such that
    A1: x in X \ X by XBOOLE_0:7;
  x in X & not x in X by A1, XBOOLE_0:def 5;
  hence contradiction;
end;

Exercise 5: 

for a,b being object holds {a} \ {a,b} = {}
proof
  let a,b be object;
  assume {a} \ {a,b} <> {};
  then consider x being object such that
    A1: x in {a} \ {a,b} by XBOOLE_0:7;
  x in {a} & not x in {a,b} by A1, XBOOLE_0:def 5;
  then x = a & not (x = a or x = b) by TARSKI:def 1, TARSKI:def 2;
  hence contradiction;
end;

Exercise 6: 

for x,y being object holds [:{x},{y}:] = {[x,y]}
proof
  let x,y be object;
  for z being object holds z in [:{x},{y}:] iff z = [x,y]
  proof
    let z be object;
    thus z in [:{x},{y}:] implies z = [x,y]
    proof
      assume z in [:{x},{y}:];
      then consider a,b being object such that
        A1: a in {x} & b in {y} & z = [a,b] by ZFMISC_1:def 2;
      a = x & b = y by A1, TARSKI:def 1;
      hence z = [x,y] by A1;
    end;
    thus z = [x,y] implies z in [:{x},{y}:]
    proof
      assume A2: z = [x,y];
      x in {x} & y in {y} by TARSKI:def 1;
      hence z in [:{x},{y}:] by A2, ZFMISC_1:def 2;
    end;
  end;
  hence thesis by TARSKI:def 1;
end;

Exercise 7: 

for x,y,z being object holds [:{x,y},{z}:] = {[x,z],[y,z]}
proof
  let x,y,z be object;
  for p being object holds p in [:{x,y},{z}:] iff p = [x,z] or p = [y,z]
  proof
    let p be object;
    thus p in [:{x,y},{z}:] implies p = [x,z] or p = [y,z]
    proof
      assume p in [:{x,y},{z}:];
      then consider a,b being object such that
        A1: a in {x,y} & b in {z} & p = [a,b] by ZFMISC_1:def 2;
      (a = x or a = y) & b = z by A1, TARSKI:def 1, TARSKI:def 2;
      hence thesis by A1;
    end;
    thus p = [x,z] or p = [y,z] implies p in [:{x,y},{z}:]
    proof
      assume p = [x,z] or p = [y,z];
      then per cases;
      suppose A2: p = [x,z];
        x in {x,y} & z in {z} by TARSKI:def 1, TARSKI:def 2;
        hence thesis by A2, ZFMISC_1:def 2;
      end;
      suppose A3: p = [y,z];
        y in {x,y} & z in {z} by TARSKI:def 1, TARSKI:def 2;
        hence thesis by A3, ZFMISC_1:def 2;
      end;
    end;
  end;
  hence thesis by TARSKI:def 2;
end;

Exercise 8: 

for X,Y,Z being set holds [:X \/ Y, Z:] = [:X, Z:] \/ [:Y, Z:]
proof
  let X,Y,Z be set;
  for p being object holds p in [:X \/ Y, Z:] iff
    p in [:X, Z:] or p in [:Y, Z:]
  proof
    let p be object;
    thus p in [:X \/ Y, Z:] implies p in [:X, Z:] or p in [:Y, Z:]
    proof
      assume p in [:X \/ Y, Z:];
      then consider a,b being object such that
        A1: a in X \/ Y & b in Z & p = [a,b] by ZFMISC_1:def 2;
      a in X or a in Y by A1, XBOOLE_0:def 3;
      hence thesis by A1, ZFMISC_1:def 2;
    end;
    thus p in [:X, Z:] or p in [:Y, Z:] implies p in [:X \/ Y, Z:]
    proof
      assume p in [:X, Z:] or p in [:Y, Z:];
      then per cases;
      suppose p in [:X, Z:];
        then consider a,b being object such that
          A2: a in X & b in Z & p = [a,b] by ZFMISC_1:def 2;
        a in X \/ Y by A2, XBOOLE_0:def 3;
        hence thesis by A2, ZFMISC_1:def 2;
      end;
      suppose p in [:Y, Z:];
        then consider a,b being object such that
          A3: a in Y & b in Z & p = [a,b] by ZFMISC_1:def 2;
        a in X \/ Y by A3, XBOOLE_0:def 3;
        hence thesis by A3, ZFMISC_1:def 2;
      end;
    end;
  end;
  hence thesis by XBOOLE_0:def 3;
end;

Exercise 9: 

for X,Y,Z being set holds [:Z, X /\ Y:] = [:Z, X:] /\ [:Z, Y:]
proof
  let X,Y,Z be set;
  for p being object holds p in [:Z, X /\ Y:] iff
    p in [:Z, X:] & p in [:Z, Y:]
  proof
    let p be object;
    thus p in [:Z, X /\ Y:] implies p in [:Z, X:] & p in [:Z, Y:]
    proof
      assume p in [:Z, X /\ Y:];
      then consider a,b being object such that
        A1: a in Z & b in X /\ Y & p = [a,b] by ZFMISC_1:def 2;
      A2: b in X & b in Y by A1, XBOOLE_0:def 4;
      hence p in [:Z, X:] by A1, ZFMISC_1:def 2;
      thus p in [:Z, Y:] by A1, A2, ZFMISC_1:def 2;
    end;
    thus p in [:Z, X:] & p in [:Z, Y:] implies p in [:Z, X /\ Y:]
    proof
      assume A3: p in [:Z, X:] & p in [:Z, Y:];
      then consider a,b being object such that
        A4: a in Z & b in X & p = [a,b] by ZFMISC_1:def 2;
      consider c,d being object such that
        A5: c in Z & d in Y & p = [c,d] by A3, ZFMISC_1:def 2;
      b = d by A4, A5, XTUPLE_0:1;
      then b in X /\ Y by A4, A5, XBOOLE_0:def 4;
      hence p in [:Z, X /\ Y:] by A4, ZFMISC_1:def 2;
    end;
  end;
  hence thesis by XBOOLE_0:def 4;
end;

Exercise 10: 

for X,Y,Z being set holds [:X \ Y, Z:] = [:X, Z:] \ [:Y, Z:]
proof
  let X,Y,Z be set;
  for p being object holds p in [:X \ Y, Z:] iff
    p in [:X, Z:] & not p in [:Y, Z:]
  proof
    let p be object;
    thus p in [:X \ Y, Z:] implies p in [:X, Z:] & not p in [:Y, Z:]
    proof
      assume p in [:X \ Y, Z:];
      then consider a,b being object such that
        A1: a in X \ Y & b in Z & p = [a,b] by ZFMISC_1:def 2;
      A2: a in X & not a in Y by A1, XBOOLE_0:def 5;
      hence p in [:X, Z:] by A1, ZFMISC_1:def 2;
      assume p in [:Y, Z:];
      then consider c,d being object such that
        A3: c in Y & d in Z & p = [c,d] by ZFMISC_1:def 2;
      a = c by A1, A3, XTUPLE_0:1;
      hence contradiction by A2, A3;
    end;
    thus p in [:X, Z:] & not p in [:Y, Z:] implies p in [:X \ Y, Z:]
    proof
      assume A4: p in [:X, Z:] & not p in [:Y, Z:];
      then consider a,b being object such that
        A5: a in X & b in Z & p = [a,b] by ZFMISC_1:def 2;
      not a in Y by A4, A5, ZFMISC_1:def 2;
      then a in X \ Y by A5, XBOOLE_0:def 5;
      hence p in [:X \ Y, Z:] by A5, ZFMISC_1:def 2;
    end;
  end;
  hence thesis by XBOOLE_0:def 5;
end;

Exercise 11: 

for X,Y,Z being set holds Z c= X & Z c= Y implies Z c= X /\ Y
proof
  let X,Y,Z be set;
  assume A1: Z c= X & Z c= Y;
  for x being object st x in Z holds x in X /\ Y
  proof
    let x be object;
    assume x in Z;
    then x in X & x in Y by A1, TARSKI:def 3;
    hence x in X /\ Y by XBOOLE_0:def 4;
  end;
  hence thesis by TARSKI:def 3;
end;

Exercise 12: 

for X,Y being set holds X c= Y implies X \/ Y = Y
proof
  let X,Y be set;
  assume A1: X c= Y;
  for x being object holds x in Y iff x in X or x in Y
  proof
    let x be object;
    thus x in Y implies x in X or x in Y;
    thus x in X or x in Y implies x in Y by A1, TARSKI:def 3;
  end;
  hence thesis by XBOOLE_0:def 3;
end;

Exercise 13: 

for X,Y,Z being set holds X c= Y implies X \ Z c= Y \ Z & Z \ Y c= Z \ X
proof
  let X,Y,Z be set;
  assume A1: X c= Y;
  for x being object holds x in X \ Z implies x in Y \ Z
  proof
    let x be object;
    assume x in X \ Z;
    then x in X & not x in Z by XBOOLE_0:def 5;
    then x in Y & not x in Z by A1, TARSKI:def 3;
    hence thesis by XBOOLE_0:def 5;
  end;
  hence X \ Z c= Y \ Z by TARSKI:def 3;
  for x being object holds x in Z \ Y implies x in Z \ X
  proof
    let x be object;
    assume x in Z \ Y;
    then x in Z & not x in Y by XBOOLE_0:def 5;
    then x in Z & not x in X by A1, TARSKI:def 3;
    hence thesis by XBOOLE_0:def 5;
  end;
  hence Z \ Y c= Z \ X by TARSKI:def 3;
end;

Exercise 14: 

for X1,Y1,X2,Y2 being set st X1 c= Y1 & X2 c= Y2 holds [:X1,X2:] c= [:Y1,Y2:]
proof
  let X1,Y1,X2,Y2 be set;
  assume A1: X1 c= Y1 & X2 c= Y2;
  for p being object st p in [:X1,X2:] holds p in [:Y1,Y2:]
  proof
    let p be object;
    assume p in [:X1,X2:];
    then consider a,b being object such that
      A2: a in X1 & b in X2 & p = [a,b] by ZFMISC_1:def 2;
    a in Y1 & b in Y2 by A1, A2, TARSKI:def 3;
    hence thesis by A2, ZFMISC_1:def 2;
  end;
  hence thesis by TARSKI:def 3;
end;

Exercise 15: 

for x being object holds bool { x } = { {} , { x }}
proof
  let x be object;
  now
    let z be object;
    reconsider Z = z as set by TARSKI:1;
    thus z in bool {x} implies z = {} or z = {x}
    proof
      assume z in bool {x};
      then A1: Z c= {x} by ZFMISC_1:def 1;
      per cases;
      suppose Z = {};
        hence thesis;
      end;
      suppose A2: Z <> {};
        now
          let y be object;
          hereby
            assume y in Z;
            then y in {x} by A1, TARSKI:def 3;
            hence y = x by TARSKI:def 1;
          end;
          assume A3: y = x;
          assume A4: not y in Z;
          consider a being object such that
            A5: a in Z by A2, XBOOLE_0:def 1; :: this is enough thanks to BOOLE requirement, no XBOOLE_0:7 needed
          a in {x} & a <> y by A1, A4, A5, TARSKI:def 3;
          hence contradiction by A3, TARSKI:def 1;
        end;
        hence thesis by TARSKI:def 1;
      end;
    end;
    assume z = {} or z = {x};
    then per cases;
    suppose z = {};
      then Z c= {x} by XBOOLE_1:2;
      hence z in bool {x} by ZFMISC_1:def 1;
    end;
    suppose z = {x};
      hence z in bool {x} by ZFMISC_1:def 1;
    end;
  end;
  hence thesis by TARSKI:def 2;
end;

Exercise 16: 

for A,B being set holds A c= B implies bool A c= bool B
proof
  let A,B be set;
  assume A1: A c= B;
  now
    let z be object;
    reconsider Z = z as set by TARSKI:1;
    assume z in bool A;
    then Z c= A by ZFMISC_1:def 1;
    then Z c= B by A1, XBOOLE_1:1;
    hence z in bool B by ZFMISC_1:def 1;
  end;
  hence thesis by TARSKI:def 3;
end;
Retrieved from "https://en.wikibooks.org/wiki/A_Practical_Guide_To_Mizar/Syntax_and_Sets"