集合 $X,Y$ の合弁 $X \cup Y$

以下の記述は,$X,Y$の合弁$X \cup Y$を$X,Y$への作用($functor$) として定義しています。

 let X,Y be set;
  func X \/ Y -> set means
:Def2:   x in it iff x in X or x in Y;
  existence
   proof
    take union {X,Y};
    let x;
    thus x in union {X,Y} implies x in X or x in Y
     proof
      assume  x in union {X,Y};
       then ex X0 being set st x in X0 & X0 in {X,Y} by TARSKI:def 4;
      hence thesis by TARSKI:def 2;
     end;
    assume x in X or x in Y;
     then consider X0 being set such that
A4:   X0 = X or X0 = Y and
A5:   x in X0;
     X0 in {X,Y} by A4,TARSKI:def 2;
    hence x in union {X,Y} by TARSKI:def 4,A5;
   end;
  uniqueness
   proof
    let A1, A2 be set such that
A6:  x in A1 iff x in X or x in Y and
A7:  x in A2 iff x in X or x in Y;
     now
      let x;
       x in A1 iff x in X or x in Y by A6;
      hence x in A1 iff x in A2 by A7;
     end;
    hence A1 = A2 by TARSKI:2;
   end;
  commutativity;
  idempotence;

文の冒頭の

 let X,Y be set;
  func X \/ Y -> set means
:Def2:   x in it iff x in X or x in Y;

は$X,Y$の合弁$X \cup Y$が

$$x \in X \cup Y \Leftrightarrow (x \in X \ or \ x \in Y)$$

を充たすものとして定義されます。$X \cup Y$は

X \/ Y

で表されています。

  existence

から存在性の証明が記述されています。

まず,既に定義されている

$$union \{X,Y\}$$

について, $x$を任意にとると,

$$x \in union \{X,Y\} \Rightarrow ( x \in X \ or \ x \in Y)$$

が成り立ちます。その証明は

$$x \in union \{X,Y\}$$

を仮定すると, $TARSKI:def 4$に書かれた$union$の定義によって

$$(\exists X0)(x \in X0 \ and \ X0 \in \{X,Y\}$$

が成り立ち,さらに$TARSKI:def 4$に書かれた$\{X,Y\}$ の定義によって,

$$X0=X \ or \ X0=Y$$

が成り立つので,結局

$$x \in X \ or \ x \in Y$$

が示され証明終了です。

逆に,

$$x \in X \ or \ x \in Y$$

を仮定すると,この仮定から,

$$A4: X0 = X \ or \ X0 = Y$$

でかつ,

$$A5: x \in X0;$$

となる$X0$を選ぶことができます。 このことから, この$X0$については,$TARSKI:def 2$に書かれた$\{X,Y\}$ によって,

$$X0 \in \{X,Y\}$$

であり,$TARSKI:def 4$に書かれた$union \{X,Y\}$, 上記の$A4,A5$ によって,

$$x \in union \{X,Y\}$$

となり,存在性の証明が終了します。

一意性の証明は

  uniqueness

の後に書かれています。

集合$A1, A2$が

$$A6: x \in A1 \Leftrightarrow (x \in X \ or \ x \in Y)$$

かつ

$$A7: x \in A2 \Leftrightarrow (x \in X \ or \ x \in Y)$$

を充たすものとします。このとき, $x$を任意にとると,$A6$により,

$$x \in A1 \Leftrightarrow (x \in X \ or \ x \in Y)$$

であり,これから,$A7$により,

$$x \in A1 \Leftrightarrow x \in A2$$

となります。従って,$TARSKI:2$に書かれている定理によって

$$A1 = A2$$

が成り立ち,一意性の証明が終了します。

  commutativity;
  idempotence;

は,$X,Y$の順序を替えた$Y \cup X$も同じものであり, $X=Y$の場合の$X \cup X$も定義されることを示しています。