Definition df-norec2 34033

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.)

Assertion

Ref	Expression
df-norec2	⊢ norec2 (𝐹) = frecs({⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ (((1st ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1st ‘𝑏) ∨ (1st ‘𝑎) = (1st ‘𝑏)) ∧ ((2nd ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2nd ‘𝑏) ∨ (2nd ‘𝑎) = (2nd ‘𝑏)) ∧ 𝑎 ≠ 𝑏))}, ( No × No ), 𝐹)

Distinct variable group:   𝐹,𝑎,𝑏,𝑐,𝑑

Detailed syntax breakdown of Definition df-norec2

Step	Hyp	Ref	Expression
1		cF	. . 3 class 𝐹
2	1	cnorec2 34032	. 2 class norec2 (𝐹)
3		csur 33770	. . . 4 class No
4	3, 3	cxp 5578	. . 3 class ( No × No )
5		va	. . . . . . 7 setvar 𝑎
6	5	cv 1538	. . . . . 6 class 𝑎
7	6, 4	wcel 2108	. . . . 5 wff 𝑎 ∈ ( No × No )
8		vb	. . . . . . 7 setvar 𝑏
9	8	cv 1538	. . . . . 6 class 𝑏
10	9, 4	wcel 2108	. . . . 5 wff 𝑏 ∈ ( No × No )
11		c1st 7802	. . . . . . . . 9 class 1st
12	6, 11	cfv 6418	. . . . . . . 8 class (1st ‘𝑎)
13	9, 11	cfv 6418	. . . . . . . 8 class (1st ‘𝑏)
14		vc	. . . . . . . . . . 11 setvar 𝑐
15	14	cv 1538	. . . . . . . . . 10 class 𝑐
16		vd	. . . . . . . . . . . . 13 setvar 𝑑
17	16	cv 1538	. . . . . . . . . . . 12 class 𝑑
18		cleft 33956	. . . . . . . . . . . 12 class L
19	17, 18	cfv 6418	. . . . . . . . . . 11 class ( L ‘𝑑)
20		cright 33957	. . . . . . . . . . . 12 class R
21	17, 20	cfv 6418	. . . . . . . . . . 11 class ( R ‘𝑑)
22	19, 21	cun 3881	. . . . . . . . . 10 class (( L ‘𝑑) ∪ ( R ‘𝑑))
23	15, 22	wcel 2108	. . . . . . . . 9 wff 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))
24	23, 14, 16	copab 5132	. . . . . . . 8 class {⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))}
25	12, 13, 24	wbr 5070	. . . . . . 7 wff (1st ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1st ‘𝑏)
26	12, 13	wceq 1539	. . . . . . 7 wff (1st ‘𝑎) = (1st ‘𝑏)
27	25, 26	wo 843	. . . . . 6 wff ((1st ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1st ‘𝑏) ∨ (1st ‘𝑎) = (1st ‘𝑏))
28		c2nd 7803	. . . . . . . . 9 class 2nd
29	6, 28	cfv 6418	. . . . . . . 8 class (2nd ‘𝑎)
30	9, 28	cfv 6418	. . . . . . . 8 class (2nd ‘𝑏)
31	29, 30, 24	wbr 5070	. . . . . . 7 wff (2nd ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2nd ‘𝑏)
32	29, 30	wceq 1539	. . . . . . 7 wff (2nd ‘𝑎) = (2nd ‘𝑏)
33	31, 32	wo 843	. . . . . 6 wff ((2nd ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2nd ‘𝑏) ∨ (2nd ‘𝑎) = (2nd ‘𝑏))
34	6, 9	wne 2942	. . . . . 6 wff 𝑎 ≠ 𝑏
35	27, 33, 34	w3a 1085	. . . . 5 wff (((1st ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1st ‘𝑏) ∨ (1st ‘𝑎) = (1st ‘𝑏)) ∧ ((2nd ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2nd ‘𝑏) ∨ (2nd ‘𝑎) = (2nd ‘𝑏)) ∧ 𝑎 ≠ 𝑏)
36	7, 10, 35	w3a 1085	. . . 4 wff (𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ (((1st ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1st ‘𝑏) ∨ (1st ‘𝑎) = (1st ‘𝑏)) ∧ ((2nd ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2nd ‘𝑏) ∨ (2nd ‘𝑎) = (2nd ‘𝑏)) ∧ 𝑎 ≠ 𝑏))
37	36, 5, 8	copab 5132	. . 3 class {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ (((1st ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1st ‘𝑏) ∨ (1st ‘𝑎) = (1st ‘𝑏)) ∧ ((2nd ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2nd ‘𝑏) ∨ (2nd ‘𝑎) = (2nd ‘𝑏)) ∧ 𝑎 ≠ 𝑏))}
38	4, 37, 1	cfrecs 8067	. 2 class frecs({⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ (((1st ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1st ‘𝑏) ∨ (1st ‘𝑎) = (1st ‘𝑏)) ∧ ((2nd ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2nd ‘𝑏) ∨ (2nd ‘𝑎) = (2nd ‘𝑏)) ∧ 𝑎 ≠ 𝑏))}, ( No × No ), 𝐹)
39	2, 38	wceq 1539	1 wff norec2 (𝐹) = frecs({⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ (((1st ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1st ‘𝑏) ∨ (1st ‘𝑎) = (1st ‘𝑏)) ∧ ((2nd ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2nd ‘𝑏) ∨ (2nd ‘𝑎) = (2nd ‘𝑏)) ∧ 𝑎 ≠ 𝑏))}, ( No × No ), 𝐹)

This definition is referenced by:  norec2fn  34040  norec2ov  34041