Metamath Proof Explorer

Theorem norec2ov

Description: The value of the double-recursion surreal function. (Contributed by Scott Fenton, 20-Aug-2024)

Ref Expression
Hypothesis norec2.1 
|- F = norec2 ( G )
Assertion norec2ov 
|- ( ( A e. No /\ B e. No ) -> ( A F B ) = ( <. A , B >. G ( F |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ) )

Proof

Step Hyp Ref Expression
1 norec2.1 
 |-  F = norec2 ( G )
2 df-ov 
 |-  ( A F B ) = ( F ` <. A , B >. )
3 opelxp 
 |-  ( <. A , B >. e. ( No X. No ) <-> ( A e. No /\ B e. No ) )
4 eqid 
 |-  { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } = { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) }
5 eqid 
 |-  { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } = { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) }
6 4 5 noxpordfr 
 |-  { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } Fr ( No X. No )
7 4 5 noxpordpo 
 |-  { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } Po ( No X. No )
8 4 5 noxpordse 
 |-  { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } Se ( No X. No )
9 6 7 8 3pm3.2i 
 |-  ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } Fr ( No X. No ) /\ { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } Po ( No X. No ) /\ { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } Se ( No X. No ) )
10 df-norec2 
 |-  norec2 ( G ) = frecs ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , G )
11 1 10 eqtri 
 |-  F = frecs ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , G )
12 11 fpr2 
 |-  ( ( ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } Fr ( No X. No ) /\ { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } Po ( No X. No ) /\ { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } Se ( No X. No ) ) /\ <. A , B >. e. ( No X. No ) ) -> ( F ` <. A , B >. ) = ( <. A , B >. G ( F |` Pred ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , <. A , B >. ) ) ) )
13 9 12 mpan 
 |-  ( <. A , B >. e. ( No X. No ) -> ( F ` <. A , B >. ) = ( <. A , B >. G ( F |` Pred ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , <. A , B >. ) ) ) )
14 3 13 sylbir 
 |-  ( ( A e. No /\ B e. No ) -> ( F ` <. A , B >. ) = ( <. A , B >. G ( F |` Pred ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , <. A , B >. ) ) ) )
15 2 14 eqtrid 
 |-  ( ( A e. No /\ B e. No ) -> ( A F B ) = ( <. A , B >. G ( F |` Pred ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , <. A , B >. ) ) ) )
16 4 5 noxpordpred 
 |-  ( ( A e. No /\ B e. No ) -> Pred ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , <. A , B >. ) = ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) )
17 16 reseq2d 
 |-  ( ( A e. No /\ B e. No ) -> ( F |` Pred ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , <. A , B >. ) ) = ( F |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) )
18 17 oveq2d 
 |-  ( ( A e. No /\ B e. No ) -> ( <. A , B >. G ( F |` Pred ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , <. A , B >. ) ) ) = ( <. A , B >. G ( F |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ) )
19 15 18 eqtrd 
 |-  ( ( A e. No /\ B e. No ) -> ( A F B ) = ( <. A , B >. G ( F |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ) )