Metamath Proof Explorer

Theorem norec2ov

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

		Ref	Expression
	Hypothesis	norec2.1	$⊢ F = {norec2}_{s} #A# (G)$
	Assertion	norec2ov	$⊢ (A \in No \land B \in No) \to A F B = ⟨A, B⟩ G ({F ↾}_{((((L (A) \cup R (A)) \cup \{A\}) \times ((L (B) \cup R (B)) \cup \{B\})) ∖ \{⟨A, B⟩\})})$

Proof

Step	Hyp	Ref	Expression
1		norec2.1	$⊢ F = {norec2}_{s} #A# (G)$
2		df-ov	$⊢ A F B = F (⟨A, B⟩)$
3		opelxp	$⊢ ⟨A, B⟩ \in (No \times No) \leftrightarrow (A \in No \land B \in No)$
4		eqid	$⊢ \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} = \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\}$
5		eqid	$⊢ \{⟨a, b⟩ \| (a \in (No \times No) \land b \in (No \times No) \land ((1^{st} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 1^{st} (b) \lor 1^{st} (a) = 1^{st} (b)) \land (2^{nd} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 2^{nd} (b) \lor 2^{nd} (a) = 2^{nd} (b)) \land a \neq b))\} = \{⟨a, b⟩ \| (a \in (No \times No) \land b \in (No \times No) \land ((1^{st} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 1^{st} (b) \lor 1^{st} (a) = 1^{st} (b)) \land (2^{nd} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 2^{nd} (b) \lor 2^{nd} (a) = 2^{nd} (b)) \land a \neq b))\}$
6	4 5	noxpordfr	$⊢ \{⟨a, b⟩ \| (a \in (No \times No) \land b \in (No \times No) \land ((1^{st} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 1^{st} (b) \lor 1^{st} (a) = 1^{st} (b)) \land (2^{nd} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 2^{nd} (b) \lor 2^{nd} (a) = 2^{nd} (b)) \land a \neq b))\} Fr (No \times No)$
7	4 5	noxpordpo	$⊢ \{⟨a, b⟩ \| (a \in (No \times No) \land b \in (No \times No) \land ((1^{st} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 1^{st} (b) \lor 1^{st} (a) = 1^{st} (b)) \land (2^{nd} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 2^{nd} (b) \lor 2^{nd} (a) = 2^{nd} (b)) \land a \neq b))\} Po (No \times No)$
8	4 5	noxpordse	$⊢ \{⟨a, b⟩ \| (a \in (No \times No) \land b \in (No \times No) \land ((1^{st} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 1^{st} (b) \lor 1^{st} (a) = 1^{st} (b)) \land (2^{nd} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 2^{nd} (b) \lor 2^{nd} (a) = 2^{nd} (b)) \land a \neq b))\} Se (No \times No)$
9	6 7 8	3pm3.2i	$⊢ (\{⟨a, b⟩ \| (a \in (No \times No) \land b \in (No \times No) \land ((1^{st} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 1^{st} (b) \lor 1^{st} (a) = 1^{st} (b)) \land (2^{nd} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 2^{nd} (b) \lor 2^{nd} (a) = 2^{nd} (b)) \land a \neq b))\} Fr (No \times No) \land \{⟨a, b⟩ \| (a \in (No \times No) \land b \in (No \times No) \land ((1^{st} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 1^{st} (b) \lor 1^{st} (a) = 1^{st} (b)) \land (2^{nd} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 2^{nd} (b) \lor 2^{nd} (a) = 2^{nd} (b)) \land a \neq b))\} Po (No \times No) \land \{⟨a, b⟩ \| (a \in (No \times No) \land b \in (No \times No) \land ((1^{st} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 1^{st} (b) \lor 1^{st} (a) = 1^{st} (b)) \land (2^{nd} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 2^{nd} (b) \lor 2^{nd} (a) = 2^{nd} (b)) \land a \neq b))\} Se (No \times No))$
10		df-norec2	$⊢ {norec2}_{s} #A# (G) = frecs (\{⟨a, b⟩ \| (a \in (No \times No) \land b \in (No \times No) \land ((1^{st} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 1^{st} (b) \lor 1^{st} (a) = 1^{st} (b)) \land (2^{nd} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 2^{nd} (b) \lor 2^{nd} (a) = 2^{nd} (b)) \land a \neq b))\}, No \times No, G)$
11	1 10	eqtri	$⊢ F = frecs (\{⟨a, b⟩ \| (a \in (No \times No) \land b \in (No \times No) \land ((1^{st} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 1^{st} (b) \lor 1^{st} (a) = 1^{st} (b)) \land (2^{nd} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 2^{nd} (b) \lor 2^{nd} (a) = 2^{nd} (b)) \land a \neq b))\}, No \times No, G)$
12	11	fpr2	$⊢ ((\{⟨a, b⟩ \| (a \in (No \times No) \land b \in (No \times No) \land ((1^{st} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 1^{st} (b) \lor 1^{st} (a) = 1^{st} (b)) \land (2^{nd} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 2^{nd} (b) \lor 2^{nd} (a) = 2^{nd} (b)) \land a \neq b))\} Fr (No \times No) \land \{⟨a, b⟩ \| (a \in (No \times No) \land b \in (No \times No) \land ((1^{st} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 1^{st} (b) \lor 1^{st} (a) = 1^{st} (b)) \land (2^{nd} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 2^{nd} (b) \lor 2^{nd} (a) = 2^{nd} (b)) \land a \neq b))\} Po (No \times No) \land \{⟨a, b⟩ \| (a \in (No \times No) \land b \in (No \times No) \land ((1^{st} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 1^{st} (b) \lor 1^{st} (a) = 1^{st} (b)) \land (2^{nd} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 2^{nd} (b) \lor 2^{nd} (a) = 2^{nd} (b)) \land a \neq b))\} Se (No \times No)) \land ⟨A, B⟩ \in (No \times No)) \to F (⟨A, B⟩) = ⟨A, B⟩ G ({F ↾}_{Pred (\{⟨a, b⟩ \| (a \in (No \times No) \land b \in (No \times No) \land ((1^{st} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 1^{st} (b) \lor 1^{st} (a) = 1^{st} (b)) \land (2^{nd} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 2^{nd} (b) \lor 2^{nd} (a) = 2^{nd} (b)) \land a \neq b))\}, (No \times No), ⟨A, B⟩)})$
13	9 12	mpan	$⊢ ⟨A, B⟩ \in (No \times No) \to F (⟨A, B⟩) = ⟨A, B⟩ G ({F ↾}_{Pred (\{⟨a, b⟩ \| (a \in (No \times No) \land b \in (No \times No) \land ((1^{st} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 1^{st} (b) \lor 1^{st} (a) = 1^{st} (b)) \land (2^{nd} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 2^{nd} (b) \lor 2^{nd} (a) = 2^{nd} (b)) \land a \neq b))\}, (No \times No), ⟨A, B⟩)})$
14	3 13	sylbir	$⊢ (A \in No \land B \in No) \to F (⟨A, B⟩) = ⟨A, B⟩ G ({F ↾}_{Pred (\{⟨a, b⟩ \| (a \in (No \times No) \land b \in (No \times No) \land ((1^{st} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 1^{st} (b) \lor 1^{st} (a) = 1^{st} (b)) \land (2^{nd} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 2^{nd} (b) \lor 2^{nd} (a) = 2^{nd} (b)) \land a \neq b))\}, (No \times No), ⟨A, B⟩)})$
15	2 14	eqtrid	$⊢ (A \in No \land B \in No) \to A F B = ⟨A, B⟩ G ({F ↾}_{Pred (\{⟨a, b⟩ \| (a \in (No \times No) \land b \in (No \times No) \land ((1^{st} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 1^{st} (b) \lor 1^{st} (a) = 1^{st} (b)) \land (2^{nd} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 2^{nd} (b) \lor 2^{nd} (a) = 2^{nd} (b)) \land a \neq b))\}, (No \times No), ⟨A, B⟩)})$
16	4 5	noxpordpred	$⊢ (A \in No \land B \in No) \to Pred (\{⟨a, b⟩ \| (a \in (No \times No) \land b \in (No \times No) \land ((1^{st} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 1^{st} (b) \lor 1^{st} (a) = 1^{st} (b)) \land (2^{nd} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 2^{nd} (b) \lor 2^{nd} (a) = 2^{nd} (b)) \land a \neq b))\}, (No \times No), ⟨A, B⟩) = (((L (A) \cup R (A)) \cup \{A\}) \times ((L (B) \cup R (B)) \cup \{B\})) ∖ \{⟨A, B⟩\}$
17	16	reseq2d	$⊢ (A \in No \land B \in No) \to {F ↾}_{Pred (\{⟨a, b⟩ \| (a \in (No \times No) \land b \in (No \times No) \land ((1^{st} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 1^{st} (b) \lor 1^{st} (a) = 1^{st} (b)) \land (2^{nd} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 2^{nd} (b) \lor 2^{nd} (a) = 2^{nd} (b)) \land a \neq b))\}, (No \times No), ⟨A, B⟩)} = {F ↾}_{((((L (A) \cup R (A)) \cup \{A\}) \times ((L (B) \cup R (B)) \cup \{B\})) ∖ \{⟨A, B⟩\})}$
18	17	oveq2d	$⊢ (A \in No \land B \in No) \to ⟨A, B⟩ G ({F ↾}_{Pred (\{⟨a, b⟩ \| (a \in (No \times No) \land b \in (No \times No) \land ((1^{st} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 1^{st} (b) \lor 1^{st} (a) = 1^{st} (b)) \land (2^{nd} (a) \{⟨c, d⟩ \| c \in (L (d) \cup R (d))\} 2^{nd} (b) \lor 2^{nd} (a) = 2^{nd} (b)) \land a \neq b))\}, (No \times No), ⟨A, B⟩)}) = ⟨A, B⟩ G ({F ↾}_{((((L (A) \cup R (A)) \cup \{A\}) \times ((L (B) \cup R (B)) \cup \{B\})) ∖ \{⟨A, B⟩\})})$
19	15 18	eqtrd	$⊢ (A \in No \land B \in No) \to A F B = ⟨A, B⟩ G ({F ↾}_{((((L (A) \cup R (A)) \cup \{A\}) \times ((L (B) \cup R (B)) \cup \{B\})) ∖ \{⟨A, B⟩\})})$