norec2ov - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > norec2ov		Structured version Visualization version GIF version

Theorem norec2ov 27438

Description: The value of the double-recursion surreal function. (Contributed by Scott Fenton, 20-Aug-2024.)

**Hypothesis**
Ref	Expression
norec2.1	⊢ 𝐹 = norec2 (𝐺)

**Assertion**
Ref	Expression
norec2ov	⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴𝐹𝐵) = (⟨𝐴, 𝐵⟩𝐺(𝐹 ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {⟨𝐴, 𝐵⟩}))))

Proof of Theorem norec2ov Dummy variables 𝑎 𝑏 𝑐 𝑑 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ov 7411	. . 3 ⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
2		opelxp 5712	. . . 4 ⊢ (⟨𝐴, 𝐵⟩ ∈ ( No × No ) ↔ (𝐴 ∈ No ∧ 𝐵 ∈ No ))
3		eqid 2732	. . . . . . 7 ⊢ {⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} = {⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))}
4		eqid 2732	. . . . . . 7 ⊢ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( 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 ) ∧ 𝑏 ∈ ( No × No ) ∧ (((1^st ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^st ‘𝑏) ∨ (1^st ‘𝑎) = (1^st ‘𝑏)) ∧ ((2^nd ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^nd ‘𝑏) ∨ (2^nd ‘𝑎) = (2^nd ‘𝑏)) ∧ 𝑎 ≠ 𝑏))}
5	3, 4	noxpordfr 27432	. . . . . 6 ⊢ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ (((1^st ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^st ‘𝑏) ∨ (1^st ‘𝑎) = (1^st ‘𝑏)) ∧ ((2^nd ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^nd ‘𝑏) ∨ (2^nd ‘𝑎) = (2^nd ‘𝑏)) ∧ 𝑎 ≠ 𝑏))} Fr ( No × No )
6	3, 4	noxpordpo 27431	. . . . . 6 ⊢ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ (((1^st ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^st ‘𝑏) ∨ (1^st ‘𝑎) = (1^st ‘𝑏)) ∧ ((2^nd ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^nd ‘𝑏) ∨ (2^nd ‘𝑎) = (2^nd ‘𝑏)) ∧ 𝑎 ≠ 𝑏))} Po ( No × No )
7	3, 4	noxpordse 27433	. . . . . 6 ⊢ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ (((1^st ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^st ‘𝑏) ∨ (1^st ‘𝑎) = (1^st ‘𝑏)) ∧ ((2^nd ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^nd ‘𝑏) ∨ (2^nd ‘𝑎) = (2^nd ‘𝑏)) ∧ 𝑎 ≠ 𝑏))} Se ( No × No )
8	5, 6, 7	3pm3.2i 1339	. . . . 5 ⊢ ({⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ (((1^st ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^st ‘𝑏) ∨ (1^st ‘𝑎) = (1^st ‘𝑏)) ∧ ((2^nd ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^nd ‘𝑏) ∨ (2^nd ‘𝑎) = (2^nd ‘𝑏)) ∧ 𝑎 ≠ 𝑏))} Fr ( No × No ) ∧ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ (((1^st ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^st ‘𝑏) ∨ (1^st ‘𝑎) = (1^st ‘𝑏)) ∧ ((2^nd ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^nd ‘𝑏) ∨ (2^nd ‘𝑎) = (2^nd ‘𝑏)) ∧ 𝑎 ≠ 𝑏))} Po ( No × No ) ∧ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ (((1^st ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^st ‘𝑏) ∨ (1^st ‘𝑎) = (1^st ‘𝑏)) ∧ ((2^nd ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^nd ‘𝑏) ∨ (2^nd ‘𝑎) = (2^nd ‘𝑏)) ∧ 𝑎 ≠ 𝑏))} Se ( No × No ))
9		norec2.1	. . . . . . 7 ⊢ 𝐹 = norec2 (𝐺)
10		df-norec2 27430	. . . . . . 7 ⊢ 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 ), 𝐺)
11	9, 10	eqtri 2760	. . . . . 6 ⊢ 𝐹 = 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 ), 𝐺)
12	11	fpr2 8288	. . . . 5 ⊢ ((({⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ (((1^st ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^st ‘𝑏) ∨ (1^st ‘𝑎) = (1^st ‘𝑏)) ∧ ((2^nd ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^nd ‘𝑏) ∨ (2^nd ‘𝑎) = (2^nd ‘𝑏)) ∧ 𝑎 ≠ 𝑏))} Fr ( No × No ) ∧ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ (((1^st ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^st ‘𝑏) ∨ (1^st ‘𝑎) = (1^st ‘𝑏)) ∧ ((2^nd ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^nd ‘𝑏) ∨ (2^nd ‘𝑎) = (2^nd ‘𝑏)) ∧ 𝑎 ≠ 𝑏))} Po ( No × No ) ∧ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ (((1^st ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1^st ‘𝑏) ∨ (1^st ‘𝑎) = (1^st ‘𝑏)) ∧ ((2^nd ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2^nd ‘𝑏) ∨ (2^nd ‘𝑎) = (2^nd ‘𝑏)) ∧ 𝑎 ≠ 𝑏))} Se ( No × No )) ∧ ⟨𝐴, 𝐵⟩ ∈ ( No × No )) → (𝐹‘⟨𝐴, 𝐵⟩) = (⟨𝐴, 𝐵⟩𝐺(𝐹 ↾ Pred({⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( 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 ), ⟨𝐴, 𝐵⟩))))
13	8, 12	mpan 688	. . . 4 ⊢ (⟨𝐴, 𝐵⟩ ∈ ( No × No ) → (𝐹‘⟨𝐴, 𝐵⟩) = (⟨𝐴, 𝐵⟩𝐺(𝐹 ↾ Pred({⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( 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 ), ⟨𝐴, 𝐵⟩))))
14	2, 13	sylbir 234	. . 3 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐹‘⟨𝐴, 𝐵⟩) = (⟨𝐴, 𝐵⟩𝐺(𝐹 ↾ Pred({⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( 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 ), ⟨𝐴, 𝐵⟩))))
15	1, 14	eqtrid 2784	. 2 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴𝐹𝐵) = (⟨𝐴, 𝐵⟩𝐺(𝐹 ↾ Pred({⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( 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 ), ⟨𝐴, 𝐵⟩))))
16	3, 4	noxpordpred 27434	. . . 4 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → Pred({⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( 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 ), ⟨𝐴, 𝐵⟩) = ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {⟨𝐴, 𝐵⟩}))
17	16	reseq2d 5981	. . 3 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐹 ↾ Pred({⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( 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 ), ⟨𝐴, 𝐵⟩)) = (𝐹 ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {⟨𝐴, 𝐵⟩})))
18	17	oveq2d 7424	. 2 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (⟨𝐴, 𝐵⟩𝐺(𝐹 ↾ Pred({⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( 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 ), ⟨𝐴, 𝐵⟩))) = (⟨𝐴, 𝐵⟩𝐺(𝐹 ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {⟨𝐴, 𝐵⟩}))))
19	15, 18	eqtrd 2772	1 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴𝐹𝐵) = (⟨𝐴, 𝐵⟩𝐺(𝐹 ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {⟨𝐴, 𝐵⟩}))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 ∨ wo 845 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ≠ wne 2940 ∖ cdif 3945 ∪ cun 3946 {csn 4628 ⟨cop 4634 class class class wbr 5148 {copab 5210 Po wpo 5586 Fr wfr 5628 Se wse 5629 × cxp 5674 ↾ cres 5678 Predcpred 6299 ‘cfv 6543 (class class class)co 7408 1^st c1st 7972 2^nd c2nd 7973 frecscfrecs 8264 No csur 27140 L cleft 27337 R cright 27338 norec2 cnorec2 27429

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7724

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-tp 4633 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-se 5632 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7364 df-ov 7411 df-oprab 7412 df-mpo 7413 df-1st 7974 df-2nd 7975 df-frecs 8265 df-wrecs 8296 df-recs 8370 df-1o 8465 df-2o 8466 df-no 27143 df-slt 27144 df-bday 27145 df-sslt 27280 df-scut 27282 df-made 27339 df-old 27340 df-left 27342 df-right 27343 df-norec2 27430

This theorem is referenced by: addsval 27443 mulsval 27562

W3C validator