Proof of id and associativity in Rel category

Question

I'm learning Category Theory by Steve Awodey's book. The very first exercise asks to show if $\mathbf{Rel}$ is a category. As I understood everything is already set (objects, arrow, id and composition) and all I need to do is to show that axioms for id and composition work.

I did it like this:

For id axiom using the definition of composition in $\mathbf{Rel}$:

$f \circ 1_A = \{ \langle a,b \rangle \in A \times B \mid \langle a,a \rangle \in 1_A \land \langle a,b \rangle \in f \} = f = \{ \langle a,b \rangle \in A \times B \mid \langle a,b \rangle \in B \land \langle b,b \rangle \in 1_B\} = 1_B \circ f$

For showing composition associativity I have introduced a new arrow $h\colon C \to D$:

$h \circ (g \circ f) = \{ \langle a,d \rangle \in A \times D \mid \exists c\, (\langle a,c \rangle \in g \circ f \land \langle c,d \rangle \in h) \} = \{ \langle a,d \rangle \in A \times D \mid \exists b\, (\langle a,b \rangle \in f \land \langle b,d \rangle \in h \circ g) \} = (h \circ g) \circ f$

Is it how it should be or my considerations were wrong?

Answer 1

As an example of what Derek Elkins said in his comment, you might try including detail such as, --- where the “•” is punctuation ---

   f ∘ 1
=⟨ definition of composition ⟩
  { ⟨x, z⟩ ❙ (∃ y • ⟨x,y⟩ ∈ 1 ∧ ⟨y, z⟩ ∈ f) }
=⟨ definition of identity relation ⟩
  { ⟨x, z⟩ ❙ (∃ y • x = y ∧ ⟨y, z⟩ ∈ f) }
=⟨ Removing the silly quantifier, since y = x ⟩
  { ⟨x, z⟩ ❙ ⟨x, z⟩ ∈ f }
=⟨ extensionality ⟩
  f