Definition df-norec2 34106

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 34105	. 2 class norec2 (𝐹)
3		csur 33843	. . . 4 class No
4	3, 3	cxp 5587	. . 3 class ( No × No )
5		va	. . . . . . 7 setvar 𝑎
6	5	cv 1538	. . . . . 6 class 𝑎
7	6, 4	wcel 2106	. . . . 5 wff 𝑎 ∈ ( No × No )
8		vb	. . . . . . 7 setvar 𝑏
9	8	cv 1538	. . . . . 6 class 𝑏
10	9, 4	wcel 2106	. . . . 5 wff 𝑏 ∈ ( No × No )
11		c1st 7829	. . . . . . . . 9 class 1st
12	6, 11	cfv 6433	. . . . . . . 8 class (1st ‘𝑎)
13	9, 11	cfv 6433	. . . . . . . 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 34029	. . . . . . . . . . . 12 class L
19	17, 18	cfv 6433	. . . . . . . . . . 11 class ( L ‘𝑑)
20		cright 34030	. . . . . . . . . . . 12 class R
21	17, 20	cfv 6433	. . . . . . . . . . 11 class ( R ‘𝑑)
22	19, 21	cun 3885	. . . . . . . . . 10 class (( L ‘𝑑) ∪ ( R ‘𝑑))
23	15, 22	wcel 2106	. . . . . . . . 9 wff 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))
24	23, 14, 16	copab 5136	. . . . . . . 8 class {⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))}
25	12, 13, 24	wbr 5074	. . . . . . 7 wff (1st ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1st ‘𝑏)
26	12, 13	wceq 1539	. . . . . . 7 wff (1st ‘𝑎) = (1st ‘𝑏)
27	25, 26	wo 844	. . . . . 6 wff ((1st ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1st ‘𝑏) ∨ (1st ‘𝑎) = (1st ‘𝑏))
28		c2nd 7830	. . . . . . . . 9 class 2nd
29	6, 28	cfv 6433	. . . . . . . 8 class (2nd ‘𝑎)
30	9, 28	cfv 6433	. . . . . . . 8 class (2nd ‘𝑏)
31	29, 30, 24	wbr 5074	. . . . . . 7 wff (2nd ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2nd ‘𝑏)
32	29, 30	wceq 1539	. . . . . . 7 wff (2nd ‘𝑎) = (2nd ‘𝑏)
33	31, 32	wo 844	. . . . . 6 wff ((2nd ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2nd ‘𝑏) ∨ (2nd ‘𝑎) = (2nd ‘𝑏))
34	6, 9	wne 2943	. . . . . 6 wff 𝑎 ≠ 𝑏
35	27, 33, 34	w3a 1086	. . . . 5 wff (((1st ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1st ‘𝑏) ∨ (1st ‘𝑎) = (1st ‘𝑏)) ∧ ((2nd ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2nd ‘𝑏) ∨ (2nd ‘𝑎) = (2nd ‘𝑏)) ∧ 𝑎 ≠ 𝑏)
36	7, 10, 35	w3a 1086	. . . 4 wff (𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ (((1st ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1st ‘𝑏) ∨ (1st ‘𝑎) = (1st ‘𝑏)) ∧ ((2nd ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2nd ‘𝑏) ∨ (2nd ‘𝑎) = (2nd ‘𝑏)) ∧ 𝑎 ≠ 𝑏))
37	36, 5, 8	copab 5136	. . 3 class {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ (((1st ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1st ‘𝑏) ∨ (1st ‘𝑎) = (1st ‘𝑏)) ∧ ((2nd ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2nd ‘𝑏) ∨ (2nd ‘𝑎) = (2nd ‘𝑏)) ∧ 𝑎 ≠ 𝑏))}
38	4, 37, 1	cfrecs 8096	. 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  34113  norec2ov  34114