Exercise 3.3.1

Exercise 3.3.1. Show that the definition of equality in Definition 3.3.7 is reflexive, symmetric, and transitive. Also verity the substitution property: if \(f,\tilde{f}:X\to Y\) and \(g,\tilde{g}:Y\to Z\) are functions such that \(f=\tilde{f}\) and \(g=\tilde{g}\), then \(g\circ f=\tilde{g}\circ\tilde{f}\).

  • \(+\) Notation: \(\text{Domain}(f:X\to Y)= X\)
  • \(+\) Notation: \(\text{Range}(f:X\to Y)=Y\)

Reflexive

  • \(\bullet\) Show that \(\forall f,~f=f\)
  • \(\Vdash\) \(f=f\)
  • \(\equiv\) { Claim 1, Claim2, Claim 3, and Definition 3.3.7 }
    • \(\text{True}\)
  • \(\square\)
    • \(\bullet\) Claim 1: \(\text{Domain}(f)=\text{Domain}(f)\)
    • \(f:X\to Y\)
    • \(\Vdash\) \(X=X\)
    • \(\equiv\) { \(X\) is an object by Axiom 3.1,
      \(~~~\) reflexive axiom for any object }
      • \(\text{True}\)
    • \(\square\)
    • \(\bullet\) Claim 2: \(\text{Range}(f)=\text{Range}(f)\)
    • \(f:X\to Y\)
    • \(\Vdash\) \(Y=Y\)
    • \(\equiv\) { \(Y\) is an object by Axiom 3.1,
      \(~~\) reflexive axiom for any object }
      • \(\text{True}\)
    • \(\square\)
    • \(\bullet\) Claim 3: \(\forall x \in X,~f(x)=f(x)\)
    • \(\Vdash\) \(f(x)=f(x)\)
    • \(\equiv\) { \(f(x)\) is an object by definition of function,
      \(~~~\) reflexive axiom for any object }
      • \(\text{True}\)
    • \(\square\)

Symmetric

  • \(\bullet\) Show that \(f=g\implies g=f\)
  • \(\Vdash\) \(f=g\)
  • \(\Rightarrow\) { Claim1, Claim2, Claim3 and Definition 3.3.7 }
    • \(g=f\)
  • \(\square\)
    • \(\bullet\) Claim 1: \(\text{Domain}(f)=\text{Domain}(g)\implies\text{Domain}(g)=\text{Domain}(f)\)
    • \(f:X\to Y\)
    • \(g:X'\to Y'\)
    • \(\Vdash\) \(X=X'\)
    • \(\Rightarrow\) { \(X\) and \(X'\) are objects by Axiom 3.1,
      \(~~~\) symmetry axiom for any two objects of the same type }
      • \(X'=X\)
    • \(\square\)
    • \(\bullet\) Claim 2: \(\text{Range}(f)=\text{Range}(g)\implies\text{Range}(g)=\text{Range}(f)\)
    • \(f:X\to Y\)
    • \(g:X'\to Y'\)
    • \(\Vdash\) \(Y=Y'\)
    • \(\Rightarrow\) { \(X\) and \(X'\) are objects by Axiom 3.1,
      \(~~~\) symmetry axiom for any two objects of the same type }
      • \(Y'=Y\)
    • \(\square\)
    • \(\bullet\) Claim 3: \(\forall x \in X,~f(x)=g(x)\implies \forall x \in X,~g(x)=f(x)\)
    • \(\Vdash\) \(f(x)=g(x)\)
    • \(\Rightarrow\) { \(f(x)\) and \(g(x)\) are objects by definition of function,
      \(~~~\) the symmetry axiom for any two objects of the same type }
      • \(g(x)=f(x)\)
    • \(\square\)


Transitive

  • \(\bullet\) Show that \((f=g)\land(g=h)\implies f=h\)
  • \(\Vdash\) \((f=g)\land(g=h)\)
  • \(\Rightarrow\) { Claim1, Claim2, Claim3 and Definition 3.3.7 }
    • \(f=h\)
  • \(\square\)
    • \(\bullet\) Claim 1: \((\text{Domain}(f)=\text{Domain}(g))\land(\text{Domain}(g)=\text{Domain}(h))\implies\text{Domain}(f)=\text{Domain}(h)\)
    • \(f:X\to Y\)
    • \(g:X'\to Y'\)
    • \(h:X''\to Y''\)
    • \(\Vdash\) \(X\)
    • \(=\) { \(\text{Domain}(f)=\text{Domain}(g)\) }
      • \(X'\)
    • \(=\) { \(\text{Domain}(g)=\text{Domain}(h)\) }
      • \(X''\)
    • \(\Rightarrow\) { \(X\), \(X'\) and \(X''\) are objects by Axiom 3.1,
      \(~~~\) transitive axiom for any three objects of the same type }
      • \(X=X''\)
    • \(\square\)
    • \(\bullet\) Claim 2: \((\text{Range}(f)=\text{Range}(g))\land(\text{Range}(g)=\text{Range}(h))\implies\text{Range}(f)=\text{Range}(h)\)
    • \(f:X\to Y\)
    • \(g:X'\to Y'\)
    • \(h:X''\to Y''\)
    • \(\Vdash\) \(Y\)
    • \(=\) { \(\text{Range}(f)=\text{Range}(g)\) }
      • \(Y'\)
    • \(=\) { \(\text{Range}(g)=\text{Range}(h)\) }
      • \(Y''\)
    • \(\Rightarrow\) { \(Y\), \(Y'\) and \(Y''\) are objects by Axiom 3.1,
      \(~~~\) transitive axiom for any three objects of the same type }
      • \(Y=Y''\)
    • \(\square\)
    • \(\bullet\) Claim 3: \((\forall x \in X,~(f(x)=g(x)))\land (\forall x \in X,~(g(x)=h(x))) \implies (\forall x \in X,~f(x)=h(x))\)
    • \(\Vdash\) \(f(x)\)
    • \(=\) { \(f(x)=g(x)\) }
      • \(g(x)\)
    • \(=\) { \(g(x)=h(x)\) }
      • \(h(x)\)
    • \(\Rightarrow\) { \(f(x)\), \(g(x)\) and \(h(x)\) are objects by definition of function,
      \(~~~\) transitive axiom for any three objects of the same type }
      • \(f(x)=h(x)\)
    • \(\square\)
    Substitution
    • \(\bullet\) Show that \(g\circ f=\tilde{g}\circ\tilde{f}\).
    • \(f,\tilde{f}:X\to Y\)
    • \(g,\tilde{g}:Y\to Z\)
    • \(\Vdash\) \(g\circ f\)
    • \(=\) { Claim 1, Claim 2, Claim 3, Definition 3.3.7 and Definition 3.3.10 }
      • \(\tilde{g}\circ\tilde{f}\)
    • \(\square\)
      • \(\bullet\) Claim 1: \(\text{Domain}(g\circ f)=\text{Domain}(\tilde{g}\circ\tilde{f})\)
      • \(\Vdash\) \(\text{Domain}(g\circ f)=\text{Domain}(\tilde{g}\circ\tilde{f})\)
      • \(\equiv\) { Definition 3.3.10 }
        • \(X=X\)
      • \(\equiv\) { \(X\) is an objects by Axiom 3.1,
        \(~~~\) reflexive axiom for any object }
        • \(\text{True}\)
      • \(\square\)
      • \(\bullet\) Claim 2: \(\text{Range}(g\circ f)=\text{Range}(\tilde{g}\circ\tilde{f})\)
      • \(\Vdash\) \(\text{Range}(g\circ f)=\text{Range}(\tilde{g}\circ\tilde{f})\)
      • \(\equiv\) { Definition 3.3.10 }
        • \(Y=Y\)
      • \(\equiv\) { \(Y\) is an objects by Axiom 3.1,
        \(~~~\) reflexive axiom for any object }
        • \(\text{True}\)
      • \(\square\)
      • \(\bullet\) Claim 3: \((\forall x\in X, ~(f(x)=\tilde{f}(x)))\land (\forall y\in Y,(g(y)=\tilde{g}(y))) \implies (\forall x\in X, g(f(x))=\tilde{g}(\tilde{f}(x)))\)
      • \(\Vdash\) \(g(f(x))\)
      • \(=\) { \(\forall x\in X, f(x)=\tilde{f}(x)\),
        \(~~~\) substitution axiom for any two objects of the same type }
        • \(g(\tilde{f}(x))\)
      • \(=\) {\(\forall y\in Y, g(y)=\tilde{g}(y)\) and let \(y=\tilde{f}(x)\) }
        • \(\tilde{g}(\tilde{f}(x))\)
      • \(\square\)