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 ( 𝐹 ) = frecs ( { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ ( ( ( 1^st ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 1^st ‘ 𝑏 ) ∨ ( 1^st ‘ 𝑎 ) = ( 1^st ‘ 𝑏 ) ) ∧ ( ( 2^nd ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 2^nd ‘ 𝑏 ) ∨ ( 2^nd ‘ 𝑎 ) = ( 2^nd ‘ 𝑏 ) ) ∧ 𝑎 ≠ 𝑏 ) ) } , ( No × No ) , 𝐹 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	⊢ 𝐹
1	0	cnorec2	⊢ norec2 ( 𝐹 )
2		va	⊢ 𝑎
3		vb	⊢ 𝑏
4	2	cv	⊢ 𝑎
5		csur	⊢ No
6	5 5	cxp	⊢ ( No × No )
7	4 6	wcel	⊢ 𝑎 ∈ ( No × No )
8	3	cv	⊢ 𝑏
9	8 6	wcel	⊢ 𝑏 ∈ ( No × No )
10		c1st	⊢ 1^st
11	4 10	cfv	⊢ ( 1^st ‘ 𝑎 )
12		vc	⊢ 𝑐
13		vd	⊢ 𝑑
14	12	cv	⊢ 𝑐
15		cleft	⊢ L
16	13	cv	⊢ 𝑑
17	16 15	cfv	⊢ ( L ‘ 𝑑 )
18		cright	⊢ R
19	16 18	cfv	⊢ ( R ‘ 𝑑 )
20	17 19	cun	⊢ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) )
21	14 20	wcel	⊢ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) )
22	21 12 13	copab	⊢ { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) }
23	8 10	cfv	⊢ ( 1^st ‘ 𝑏 )
24	11 23 22	wbr	⊢ ( 1^st ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 1^st ‘ 𝑏 )
25	11 23	wceq	⊢ ( 1^st ‘ 𝑎 ) = ( 1^st ‘ 𝑏 )
26	24 25	wo	⊢ ( ( 1^st ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 1^st ‘ 𝑏 ) ∨ ( 1^st ‘ 𝑎 ) = ( 1^st ‘ 𝑏 ) )
27		c2nd	⊢ 2^nd
28	4 27	cfv	⊢ ( 2^nd ‘ 𝑎 )
29	8 27	cfv	⊢ ( 2^nd ‘ 𝑏 )
30	28 29 22	wbr	⊢ ( 2^nd ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 2^nd ‘ 𝑏 )
31	28 29	wceq	⊢ ( 2^nd ‘ 𝑎 ) = ( 2^nd ‘ 𝑏 )
32	30 31	wo	⊢ ( ( 2^nd ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 2^nd ‘ 𝑏 ) ∨ ( 2^nd ‘ 𝑎 ) = ( 2^nd ‘ 𝑏 ) )
33	4 8	wne	⊢ 𝑎 ≠ 𝑏
34	26 32 33	w3a	⊢ ( ( ( 1^st ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 1^st ‘ 𝑏 ) ∨ ( 1^st ‘ 𝑎 ) = ( 1^st ‘ 𝑏 ) ) ∧ ( ( 2^nd ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 2^nd ‘ 𝑏 ) ∨ ( 2^nd ‘ 𝑎 ) = ( 2^nd ‘ 𝑏 ) ) ∧ 𝑎 ≠ 𝑏 )
35	7 9 34	w3a	⊢ ( 𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ ( ( ( 1^st ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 1^st ‘ 𝑏 ) ∨ ( 1^st ‘ 𝑎 ) = ( 1^st ‘ 𝑏 ) ) ∧ ( ( 2^nd ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 2^nd ‘ 𝑏 ) ∨ ( 2^nd ‘ 𝑎 ) = ( 2^nd ‘ 𝑏 ) ) ∧ 𝑎 ≠ 𝑏 ) )
36	35 2 3	copab	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ ( ( ( 1^st ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 1^st ‘ 𝑏 ) ∨ ( 1^st ‘ 𝑎 ) = ( 1^st ‘ 𝑏 ) ) ∧ ( ( 2^nd ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 2^nd ‘ 𝑏 ) ∨ ( 2^nd ‘ 𝑎 ) = ( 2^nd ‘ 𝑏 ) ) ∧ 𝑎 ≠ 𝑏 ) ) }
37	6 36 0	cfrecs	⊢ frecs ( { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ ( ( ( 1^st ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 1^st ‘ 𝑏 ) ∨ ( 1^st ‘ 𝑎 ) = ( 1^st ‘ 𝑏 ) ) ∧ ( ( 2^nd ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 2^nd ‘ 𝑏 ) ∨ ( 2^nd ‘ 𝑎 ) = ( 2^nd ‘ 𝑏 ) ) ∧ 𝑎 ≠ 𝑏 ) ) } , ( No × No ) , 𝐹 )
38	1 37	wceq	⊢ norec2 ( 𝐹 ) = frecs ( { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ ( ( ( 1^st ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 1^st ‘ 𝑏 ) ∨ ( 1^st ‘ 𝑎 ) = ( 1^st ‘ 𝑏 ) ) ∧ ( ( 2^nd ‘ 𝑎 ) { ⟨ 𝑐 , 𝑑 ⟩ ∣ 𝑐 ∈ ( ( L ‘ 𝑑 ) ∪ ( R ‘ 𝑑 ) ) } ( 2^nd ‘ 𝑏 ) ∨ ( 2^nd ‘ 𝑎 ) = ( 2^nd ‘ 𝑏 ) ) ∧ 𝑎 ≠ 𝑏 ) ) } , ( No × No ) , 𝐹 )

Metamath Proof Explorer

Definition df-norec2

Detailed syntax breakdown