Theorem noxpordpo

Description: To get through most of the textbook defintions in surreal numbers we will need recursion on two variables. This set of theorems sets up the preconditions for double recursion. This theorem establishes the partial ordering. (Contributed by Scott Fenton, 19-Aug-2024)

	Ref	Expression
Hypotheses	noxpord.1	No typesetting found for |- R = { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } with typecode |-
	noxpord.2	$$⊢S=\left\{⟨x,y⟩|\left(x\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge y\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge \left(\left(1^{st}\left(x\right)R{1}^{st}\left(y\right)\vee 1^{st}\left(x\right)=1^{st}\left(y\right)\right)\wedge \left(2^{nd}\left(x\right)R{2}^{nd}\left(y\right)\vee 2^{nd}\left(x\right)=2^{nd}\left(y\right)\right)\wedge x\ne y\right)\right)\right\}$$
Assertion	noxpordpo	$$⊢S\mathrm{Po}\left(\mathrm{No}\times \mathrm{No}\right)$$

Proof

Step	Hyp	Ref	Expression
1		noxpord.1	Could not format R = { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } : No typesetting found for |- R = { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) } with typecode |-
2		noxpord.2	$$⊢S=\left\{⟨x,y⟩|\left(x\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge y\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge \left(\left(1^{st}\left(x\right)R{1}^{st}\left(y\right)\vee 1^{st}\left(x\right)=1^{st}\left(y\right)\right)\wedge \left(2^{nd}\left(x\right)R{2}^{nd}\left(y\right)\vee 2^{nd}\left(x\right)=2^{nd}\left(y\right)\right)\wedge x\ne y\right)\right)\right\}$$
3	1	lrrecpo	$$⊢R\mathrm{Po}\mathrm{No}$$
4	3	a1i	$$⊢\top \to R\mathrm{Po}\mathrm{No}$$
5	2 4 4	poxp2	$$⊢\top \to S\mathrm{Po}\left(\mathrm{No}\times \mathrm{No}\right)$$
6	5	mptru	$$⊢S\mathrm{Po}\left(\mathrm{No}\times \mathrm{No}\right)$$