Metamath Proof Explorer


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
|- R = { <. a , b >. | a e. ( ( _L ` b ) u. ( _R ` b ) ) }
noxpord.2
|- S = { <. x , y >. | ( x e. ( No X. No ) /\ y e. ( No X. No ) /\ ( ( ( 1st ` x ) R ( 1st ` y ) \/ ( 1st ` x ) = ( 1st ` y ) ) /\ ( ( 2nd ` x ) R ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) /\ x =/= y ) ) }
Assertion noxpordpo
|- S Po ( No X. No )

Proof

Step Hyp Ref Expression
1 noxpord.1
 |-  R = { <. a , b >. | a e. ( ( _L ` b ) u. ( _R ` b ) ) }
2 noxpord.2
 |-  S = { <. x , y >. | ( x e. ( No X. No ) /\ y e. ( No X. No ) /\ ( ( ( 1st ` x ) R ( 1st ` y ) \/ ( 1st ` x ) = ( 1st ` y ) ) /\ ( ( 2nd ` x ) R ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) /\ x =/= y ) ) }
3 1 lrrecpo
 |-  R Po No
4 3 a1i
 |-  ( T. -> R Po No )
5 2 4 4 poxp2
 |-  ( T. -> S Po ( No X. No ) )
6 5 mptru
 |-  S Po ( No X. No )