This is a fairly minor, technical question, but I'll toss it out in case someone has a good idea on it.

Suppose $(X,<_X)$ and $(Y,<_Y)$ are well-founded orderings (not necessarily linearly ordered, though I don't think it matters). Consider the ordering ${<}$ on $X\times Y$ given by $(x',y') < (x,y)$ if $x'\leq x$ and $y'\leq y$, and either $x' < x$ or $y' < y$. Note that this is not the lexicographic ordering; indeed, it's symmetric.

Obviously $X\times Y$ is well-founded. Suppose I want to prove this carefully (by which I really mean "in the formal theory $ID_1$"); more precisely, let's take $X$ to be a set with two properties: $$Cl_X:\forall x(\forall x'<_X x. x'\in X)\rightarrow x\in X$$ and $$Ind_X: \forall Z[\forall x(\forall x'<_X x. x'\in Z)\rightarrow x\in Z)\rightarrow X\subseteq Z]$$ and similarly for $Y$. (These just characterize that $X$ is its own well-founded part.) I want to prove that for all $(x,y)\in X\times Y$, $(x,y)$ are in the well-founded part of $X\times Y$ under ${<}$; call the well-founded part of $X\times Y$ $Acc(X\times Y)$.

I know one way to prove this: for each $x\in X$, define $Y_x=\{y\in Y\mid (x,y)\in Acc(X\times Y)\}$. Let $X'$ be the set of $x\in X$ such that $Y\subseteq Y_x$. Then it would be good enough to show that $X'$ satisfies the closure property, so I can apply $Ind_X$. To do this, in turn, I show that, if $Y\subseteq Y_{x'}$ for all $x'<_X x$ then $Y_x$ satisfies the closure property, so I can apply $Ind_Y$.

Of course, that means I know I second way: I could swap $X$ and $Y$ in the above proof. Moreover, when one works through the details, it's clear that I'm really proving that the lexicographic ordering is well-founded, and using the fact that ${<}$ is a subrelation of the lexicographic ordering.

Which brings me to my question: is there a proof that $Acc(X\times Y)=X\times Y$ which is *symmetric*?

`well-ordered' be`

well-founded' throughout? (In my book `well-ordered' implies linearly ordered because, in particular, every two-element sets has a minimum.) $\endgroup$