Metamath Proof Explorer

Definition df-norec2

Description: Define surreal recursion on two variables. This function is key to the development of most of surreal numbers. (Contributed by Scott Fenton, 20-Aug-2024)

Ref Expression
Assertion df-norec2 
|- norec2 ( F ) = frecs ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _L ` d ) u. ( _R ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _L ` d ) u. ( _R ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , F )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cF 
 |-  F
1 0 cnorec2 
 |-  norec2 ( F )
2 va 
 |-  a
3 vb 
 |-  b
4 2 cv 
 |-  a
5 csur 
 |-  No
6 5 5 cxp 
 |-  ( No X. No )
7 4 6 wcel 
 |-  a e. ( No X. No )
8 3 cv 
 |-  b
9 8 6 wcel 
 |-  b e. ( No X. No )
10 c1st 
 |-  1st
11 4 10 cfv 
 |-  ( 1st ` a )
12 vc 
 |-  c
13 vd 
 |-  d
14 12 cv 
 |-  c
15 cleft 
 |-  _L
16 13 cv 
 |-  d
17 16 15 cfv 
 |-  ( _L ` d )
18 cright 
 |-  _R
19 16 18 cfv 
 |-  ( _R ` d )
20 17 19 cun 
 |-  ( ( _L ` d ) u. ( _R ` d ) )
21 14 20 wcel 
 |-  c e. ( ( _L ` d ) u. ( _R ` d ) )
22 21 12 13 copab 
 |-  { <. c , d >. | c e. ( ( _L ` d ) u. ( _R ` d ) ) }
23 8 10 cfv 
 |-  ( 1st ` b )
24 11 23 22 wbr 
 |-  ( 1st ` a ) { <. c , d >. | c e. ( ( _L ` d ) u. ( _R ` d ) ) } ( 1st ` b )
25 11 23 wceq 
 |-  ( 1st ` a ) = ( 1st ` b )
26 24 25 wo 
 |-  ( ( 1st ` a ) { <. c , d >. | c e. ( ( _L ` d ) u. ( _R ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) )
27 c2nd 
 |-  2nd
28 4 27 cfv 
 |-  ( 2nd ` a )
29 8 27 cfv 
 |-  ( 2nd ` b )
30 28 29 22 wbr 
 |-  ( 2nd ` a ) { <. c , d >. | c e. ( ( _L ` d ) u. ( _R ` d ) ) } ( 2nd ` b )
31 28 29 wceq 
 |-  ( 2nd ` a ) = ( 2nd ` b )
32 30 31 wo 
 |-  ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _L ` d ) u. ( _R ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) )
33 4 8 wne 
 |-  a =/= b
34 26 32 33 w3a 
 |-  ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _L ` d ) u. ( _R ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _L ` d ) u. ( _R ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b )
35 7 9 34 w3a 
 |-  ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _L ` d ) u. ( _R ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _L ` d ) u. ( _R ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) )
36 35 2 3 copab 
 |-  { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _L ` d ) u. ( _R ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _L ` d ) u. ( _R ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) }
37 6 36 0 cfrecs 
 |-  frecs ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _L ` d ) u. ( _R ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _L ` d ) u. ( _R ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , F )
38 1 37 wceq 
 |-  norec2 ( F ) = frecs ( { <. a , b >. | ( a e. ( No X. No ) /\ b e. ( No X. No ) /\ ( ( ( 1st ` a ) { <. c , d >. | c e. ( ( _L ` d ) u. ( _R ` d ) ) } ( 1st ` b ) \/ ( 1st ` a ) = ( 1st ` b ) ) /\ ( ( 2nd ` a ) { <. c , d >. | c e. ( ( _L ` d ) u. ( _R ` d ) ) } ( 2nd ` b ) \/ ( 2nd ` a ) = ( 2nd ` b ) ) /\ a =/= b ) ) } , ( No X. No ) , F )