$\DeclareMathOperator\rank{rank}\def\union{{\textstyle\bigcup}}$
El rango de un conjunto bien fundado se define recursivamente como $\rank x = \union\{\rank y +1 : y \in x\}$ . Sería bueno que $\rank\union x$ eran sólo $\union\rank x$ . Sin embargo, no he podido encontrarlo mencionado en ninguna parte y por eso lo pregunto aquí. He aquí un resumen de mi razonamiento. \begin{align*} \rank\union x &\iff (z\union x)( \rank z+1)&\text{by def. of $\rank$}\\ &\iff (yx)(zy)( \rank z +1) &\text{by def. of $\union$}\\ &\iff (yx)( \rank y)&\text{by def. of $\rank$}\\ &\iff (yx)(+1 \rank y+1)& <\text{ iff }+1<+1\\ &\iff +1 \rank x &\text{by def. of $\rank$}\\ &\iff \union\rank x. &+1<\text{ iff } (<<) \end{align*} ¿Me estoy perdiendo algo?
