What is the intuitive way of proving that a function is total?

Question

I am experiencing a huge disconnect from learning theory behind set theory and actually applying them.

For a function to be total, we know it must satisfy these two properties, given some function $F: A \to B$:

1. Function property (i.e. common for both partial and total function): $$\forall a\in A .\forall b, b' \in B. aFb \ \land aFb' \implies b = b' $$

2. Total property:

$$\forall a \in A, \exists b\in B . aFb$$

To give you my thoughts on this:

1. Function property means that for all inputs from A, if it ever results in an output, there can only be one output from an input. This makes sense since we want our function to produce only one answer, not multiple ones.

2. Total property means that we ensure all inputs from A will get an output, and so the "total" or inclusive idea of this property.

But how do I actually apply these concepts in problems? To elucidate my problem, here is an example:

Question

Show that $F: A \to B$ is a function if and only if there exists a relation $G : B \to A$ such that $id_A \subseteq G \circ F$ and $F\circ G \subseteq id_B$.

Attempt

We have two things to prove:

1. There exists $G: B \to A \implies id_A \subseteq G \circ F \land F\circ G \subseteq id_B$.

2. $ id_A \subseteq G \circ F \land F\circ G \subseteq id_B \implies G: B \to A$

To prove the first part:

$$b (F \circ G) b' \implies \forall b,b' \in B. \exists a \in A. bGa \land aFb'$$ $$\implies \forall b, b' \in B. G(b) = a \land F(a) = b'$$ $$\implies b'= b$$

Methodology: I try to present the way of thinking of how I solve it.

1. I first choose some arbitrary $b$ and $b'$ from the set $B$ composition of $F \circ G$.

2. I expand to represent in terms of $aFb$ etc.

3. Then I convert it into a function form (e.g. $F(a) = B$)

4. Finally, I extract the insight from this: i.e. $b = b'$ This means the composition result in the identity relation and is so a subset of it.

Is this a common technique to use and solve? Moreover, the last line seems a bit coerced. What is it in my reasoning that forces it to be equal? $G$ can be a function that maps to some $a$ that will not give $b'=b$. I have no intuitive understanding of this line of reasoning except that it fulfils the question criteria.

How do I then organize my argument in terms of arguing for the total property and function property in two ways? It seems like I have 4 things to argue here, and I'm lost.