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 No typesetting found for |- F = norec2 ( G ) with typecode |-
Assertion norec2fn ⊢ F Fn No × No

Proof

Step Hyp Ref Expression
1 norec2.1 Could not format F = norec2 ( G ) : No typesetting found for |- F = norec2 ( G ) with typecode |-
2 eqid Could not format { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } = { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } : No typesetting found for |- { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } = { <. c , d >. | c e. ( ( _Left ` d ) u. ( _Right ` d ) ) } with typecode |-
3 eqid Could not format { <. 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 ) ) } : No typesetting found for |- { <. 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 ) ) } with typecode |-
4 2 3 noxpordfr Could not format { <. 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 ) : No typesetting found for |- { <. 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 ) with typecode |-
5 2 3 noxpordpo Could not format { <. 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 ) : No typesetting found for |- { <. 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 ) with typecode |-
6 2 3 noxpordse Could not format { <. 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 ) : No typesetting found for |- { <. 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 ) with typecode |-
7 df-norec2 Could not format 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 ) : No typesetting found for |- 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 ) with typecode |-
8 1 7 eqtri Could not format 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 ) : No typesetting found for |- 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 ) with typecode |-
9 8 fpr1 Could not format ( ( { <. 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 ) ) : No typesetting found for |- ( ( { <. 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 ) ) with typecode |-
10 4 5 6 9 mp3an ⊢ F Fn No × No