Metamath Proof Explorer

Theorem lrrecpred

Description: Finally, we calculate the value of the predecessor class over R . (Contributed by Scott Fenton, 19-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 lrrec.1 
 |-  R = { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) }
2 dfpred3g 
 |-  ( A e. No -> Pred ( R , No , A ) = { b e. No | b R A } )
3 1 lrrecval 
 |-  ( ( b e. No /\ A e. No ) -> ( b R A <-> b e. ( ( _L ` A ) u. ( _R ` A ) ) ) )
4 3 ancoms 
 |-  ( ( A e. No /\ b e. No ) -> ( b R A <-> b e. ( ( _L ` A ) u. ( _R ` A ) ) ) )
5 4 rabbidva 
 |-  ( A e. No -> { b e. No | b R A } = { b e. No | b e. ( ( _L ` A ) u. ( _R ` A ) ) } )
6 dfrab2 
 |-  { b e. No | b e. ( ( _L ` A ) u. ( _R ` A ) ) } = ( { b | b e. ( ( _L ` A ) u. ( _R ` A ) ) } i^i No )
7 abid2 
 |-  { b | b e. ( ( _L ` A ) u. ( _R ` A ) ) } = ( ( _L ` A ) u. ( _R ` A ) )
8 7 ineq1i 
 |-  ( { b | b e. ( ( _L ` A ) u. ( _R ` A ) ) } i^i No ) = ( ( ( _L ` A ) u. ( _R ` A ) ) i^i No )
9 6 8 eqtri 
 |-  { b e. No | b e. ( ( _L ` A ) u. ( _R ` A ) ) } = ( ( ( _L ` A ) u. ( _R ` A ) ) i^i No )
10 5 9 eqtrdi 
 |-  ( A e. No -> { b e. No | b R A } = ( ( ( _L ` A ) u. ( _R ` A ) ) i^i No ) )
11 leftssold 
 |-  ( A e. No -> ( _L ` A ) C_ ( _Old ` ( bday ` A ) ) )
12 bdayelon 
 |-  ( bday ` A ) e. On
13 oldf 
 |-  _Old : On --> ~P No
14 13 ffvelrni 
 |-  ( ( bday ` A ) e. On -> ( _Old ` ( bday ` A ) ) e. ~P No )
15 14 elpwid 
 |-  ( ( bday ` A ) e. On -> ( _Old ` ( bday ` A ) ) C_ No )
16 12 15 ax-mp 
 |-  ( _Old ` ( bday ` A ) ) C_ No
17 11 16 sstrdi 
 |-  ( A e. No -> ( _L ` A ) C_ No )
18 rightssold 
 |-  ( A e. No -> ( _R ` A ) C_ ( _Old ` ( bday ` A ) ) )
19 18 16 sstrdi 
 |-  ( A e. No -> ( _R ` A ) C_ No )
20 17 19 unssd 
 |-  ( A e. No -> ( ( _L ` A ) u. ( _R ` A ) ) C_ No )
21 df-ss 
 |-  ( ( ( _L ` A ) u. ( _R ` A ) ) C_ No <-> ( ( ( _L ` A ) u. ( _R ` A ) ) i^i No ) = ( ( _L ` A ) u. ( _R ` A ) ) )
22 20 21 sylib 
 |-  ( A e. No -> ( ( ( _L ` A ) u. ( _R ` A ) ) i^i No ) = ( ( _L ` A ) u. ( _R ` A ) ) )
23 2 10 22 3eqtrd 
 |-  ( A e. No -> Pred ( R , No , A ) = ( ( _L ` A ) u. ( _R ` A ) ) )