You’re correct: read literally, those definitions are mismatched, for the reasons you give. The solution is to fix the definition of “$U$-small category” to say that “$\newcommand{\C}{\mathcal{C}}\newcommand{\mor}{\mathrm{mor}}\mor(\C)$ is $\newcommand{\ob}{\mathrm{ob}}U$-small” — this is what the authors of SGA4 clearly intended (as clarified in the footnote on p2 of this modern edition, pointed out by @abx in comments), but expressed in a way that doesn’t depend on the precise encoding of the definition of categories or of ordered pairs.

There are two general points here:

• Outside of explicit investigations of set-theoretically foundational issues (and usually even within such contexts), nothing should ever depend on the specific set-theoretic implementation of ordered pairs. Anything that seems to depend on it can very safely be assumed to be a misunderstanding, an abuse of notation, or a mismatch of definitions.

• More generally, mathematics is usually written in “implementation-independent” ways as far as possible. Of course, there are often lapses from this in practice, and that sometimes leads to mismatches, as here. When such mismatches happen, the right fix is to rewrite the later definitions in more implementation-independent ways, not to tweak the implementation of the earlier definitions so that the implementation-dependent later definitions work. In ordinary human-practiced mathematics, this usually isn’t a problem, because it’s clear what people meant. But in computer-formalised mathematics (and programming more generally), this is a serious concern: if you go back and change the implementation of the earlier definition to make one later definition work, then that may break anything else that was written in an implementation-specific way. Implementation-dependent definitions are inherently fragile — so fix them, don’t take them as fixed and twist other things around to try to work with them.

You’re correct: read literally, those definitions are mismatched, for the reasons you give. The solution is to fix the definition of “$U$-small category” to say that “$\newcommand{\C}{\mathcal{C}}\newcommand{\mor}{\mathrm{mor}}\mor(\C)$ is $\newcommand{\ob}{\mathrm{ob}}U$-small” — this is what the authors of SGA4 clearly intended (as clarified in the footnote on p2 of this modern edition, pointed out by @abx in comments), but expressed in a way that doesn’t depend on the precise encoding of the definition of categories or of ordered pairs.

There are two general points here:

• Outside of explicit investigations of set-theoretically foundational issues (and usually even within such contexts), nothing should ever depend on the specific set-theoretic implementation of ordered pairs. Anything that seems to depend on it can very safely be assumed to be a misunderstanding, an abuse of notation, or a mismatch of definitions.

• More generally, mathematics is usually written in “implementation-independent” ways as far as possible. Of course, there are often lapses from this in practice, and that sometimes leads to mismatches, as here. When such mismatches happen, the right fix is to rewrite the later definitions in more implementation-independent ways, not to tweak the implementation of the earlier definitions so that the implementation-dependent later definitions work. In ordinary human-practiced mathematics, this usually isn’t a problem, because it’s clear what people meant. But in computer-formalised mathematics (and programming more generally), this is a serious concern: if you go back and change the implementation of the earlier definition to make one later definition work, then that may break anything else that was written in an implementation-specific way. Implementation-dependent definitions are inherently fragile — so fix them, don’t take them as god-given and twist other things around to try to work with them.