Metamath Proof Explorer

Theorem norec2fn

Description: The double-recursion operator on surreals yields a function on pairs of surreals. (Contributed by Scott Fenton, 20-Aug-2024)

Ref Expression
Hypothesis norec2.1 
|- F = norec2 ( G )
Assertion norec2fn 
|- F Fn ( No X. No )

Proof

Step Hyp Ref Expression
1 norec2.1 
 |-  F = norec2 ( G )
2 eqid 
 |-  { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } = { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) }
3 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 ) ) }
4 2 3 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 )
5 2 3 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 )
6 2 3 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 )
7 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 )
8 1 7 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 )
9 8 fpr1 
 |-  ( ( { <. 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 ) ) -> F Fn ( No X. No ) )
10 4 5 6 9 mp3an 
 |-  F Fn ( No X. No )