Theorem “Identity relation” “Relationship via `Id`”:
    x ⦗ Id ⦘ y  ≡  x = y
Proof:
    x ⦗ Id ⦘ y  ≡  x = y
  ≡⟨ “Infix relationship” ⟩
    ⟨ x, y ⟩ ∈ Id  ≡  x = y
  ≡⟨ “Definition of `Id` via 𝕀” ⟩
    ⟨ x, y ⟩ ∈ 𝕀 𝐔  ≡  x = y
  ≡⟨ “Definition of 𝕀” ⟩
    ⟨ x, y ⟩ ∈ { z ❙ z ∈ 𝐔 • ⟨ z, z ⟩ } ≡  x = y
  ≡⟨ “Set membership” ⟩
    (∃ z ❙ z ∈ 𝐔 • ⟨ x, y ⟩ = ⟨ z , z ⟩ ) ≡  x = y
  ≡⟨ “Pair equality” ⟩
    (∃ z ❙ z ∈ 𝐔 • ( x = z ) ∧ ( y = z ) ) ≡  x = y
  ≡⟨ “Trading for ∃” ⟩
    (∃ z ❙ z ∈ 𝐔 ∧ ( x = z ) • ( y = z ) ) ≡  x = y
  ≡⟨ “Symmetry of ∧” ⟩
    (∃ z ❙ ( x = z ) ∧ z ∈ 𝐔 • ( y = z ) ) ≡  x = y
  ≡⟨ “Trading for ∃” ⟩
    (∃ z ❙ ( x = z ) • z ∈ 𝐔 ∧ ( y = z ) ) ≡  x = y
  ≡⟨ “One-point rule for ∃” ⟩
    (z ∈ 𝐔 ∧ ( y = z ))[ z ≔ x ] ≡ x = y
  ≡⟨ Substitution ⟩
    (x ∈ 𝐔 ∧ ( y = x )) ≡  x = y
  ≡⟨ “Universal set” ⟩
    true ∧ ( y = x ) ≡  x = y
  ≡⟨ “Identity of ∧” ⟩
    ( y = x ) ≡  x = y
  ≡⟨ “Reflexivity of ≡” ⟩
    true



Theorem “Identity of ⨾”: Id ⨾ R = R
Proof:
  Using “Relation extensionality”:
    Subproof for `∀ a • ∀ b • a ⦗ Id ⨾ R ⦘ b ≡ a ⦗ R ⦘ b`:
      For any `a`, `b`:
          a ⦗ Id ⨾ R ⦘ b
        ≡⟨ “Relation composition” ⟩
          ∃ c • a ⦗ Id ⦘ c ∧ c ⦗ R ⦘ b
        ≡⟨ “Identity relation” ⟩
          ∃ c • a = c ∧ c ⦗ R ⦘ b
        ≡⟨ “Trading for ∃” ⟩
          ∃ c ❙ a = c • c ⦗ R ⦘ b
        ≡⟨ “One-point rule for ∃” ⟩
          (c ⦗ R ⦘ b)[c ≔ a]
        ≡⟨ Substitution ⟩
          a ⦗ R ⦘ b


Theorem “Right-identity of ⨾” “Identity of ⨾”:
    R ⨾ Id = R
Proof:
  Using “Relation extensionality”:
    Subproof for `∀ a • ∀ b • a ⦗ R ⨾ Id ⦘ b ≡ a ⦗ R ⦘ b`:
      For any `a`, `b`:
          a ⦗ R ⨾ Id ⦘ b
        ≡⟨ “Relation composition” ⟩
          ∃ c • a ⦗ R ⦘ c ∧ c ⦗ Id ⦘ b
        ≡⟨ “Identity relation” ⟩
          ∃ c • a ⦗ R ⦘ c ∧ c = b
        ≡⟨ “Trading for ∃” ⟩
          ∃ c ❙ c = b • a ⦗ R ⦘ c
        ≡⟨ “One-point rule for ∃” ⟩
          (a ⦗ R ⦘ c)[c ≔ b]
        ≡⟨ Substitution ⟩
          a ⦗ R ⦘ b