Metamath Proof Explorer

Theorem lrrecpo

Description: Now, we establish that R is a partial ordering on No . (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Hypothesis lrrec.1 
|- R = { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) }
Assertion lrrecpo 
|- R Po No

Proof

Step Hyp Ref Expression
1 lrrec.1 
 |-  R = { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) }
2 bdayelon 
 |-  ( bday ` a ) e. On
3 2 onirri 
 |-  -. ( bday ` a ) e. ( bday ` a )
4 1 lrrecval2 
 |-  ( ( a e. No /\ a e. No ) -> ( a R a <-> ( bday ` a ) e. ( bday ` a ) ) )
5 4 anidms 
 |-  ( a e. No -> ( a R a <-> ( bday ` a ) e. ( bday ` a ) ) )
6 3 5 mtbiri 
 |-  ( a e. No -> -. a R a )
7 6 adantl 
 |-  ( ( T. /\ a e. No ) -> -. a R a )
8 bdayelon 
 |-  ( bday ` c ) e. On
9 ontr1 
 |-  ( ( bday ` c ) e. On -> ( ( ( bday ` a ) e. ( bday ` b ) /\ ( bday ` b ) e. ( bday ` c ) ) -> ( bday ` a ) e. ( bday ` c ) ) )
10 8 9 ax-mp 
 |-  ( ( ( bday ` a ) e. ( bday ` b ) /\ ( bday ` b ) e. ( bday ` c ) ) -> ( bday ` a ) e. ( bday ` c ) )
11 1 lrrecval2 
 |-  ( ( a e. No /\ b e. No ) -> ( a R b <-> ( bday ` a ) e. ( bday ` b ) ) )
12 11 3adant3 
 |-  ( ( a e. No /\ b e. No /\ c e. No ) -> ( a R b <-> ( bday ` a ) e. ( bday ` b ) ) )
13 1 lrrecval2 
 |-  ( ( b e. No /\ c e. No ) -> ( b R c <-> ( bday ` b ) e. ( bday ` c ) ) )
14 13 3adant1 
 |-  ( ( a e. No /\ b e. No /\ c e. No ) -> ( b R c <-> ( bday ` b ) e. ( bday ` c ) ) )
15 12 14 anbi12d 
 |-  ( ( a e. No /\ b e. No /\ c e. No ) -> ( ( a R b /\ b R c ) <-> ( ( bday ` a ) e. ( bday ` b ) /\ ( bday ` b ) e. ( bday ` c ) ) ) )
16 1 lrrecval2 
 |-  ( ( a e. No /\ c e. No ) -> ( a R c <-> ( bday ` a ) e. ( bday ` c ) ) )
17 16 3adant2 
 |-  ( ( a e. No /\ b e. No /\ c e. No ) -> ( a R c <-> ( bday ` a ) e. ( bday ` c ) ) )
18 15 17 imbi12d 
 |-  ( ( a e. No /\ b e. No /\ c e. No ) -> ( ( ( a R b /\ b R c ) -> a R c ) <-> ( ( ( bday ` a ) e. ( bday ` b ) /\ ( bday ` b ) e. ( bday ` c ) ) -> ( bday ` a ) e. ( bday ` c ) ) ) )
19 10 18 mpbiri 
 |-  ( ( a e. No /\ b e. No /\ c e. No ) -> ( ( a R b /\ b R c ) -> a R c ) )
20 19 adantl 
 |-  ( ( T. /\ ( a e. No /\ b e. No /\ c e. No ) ) -> ( ( a R b /\ b R c ) -> a R c ) )
21 7 20 ispod 
 |-  ( T. -> R Po No )
22 21 mptru 
 |-  R Po No