on2recsov

Description: Calculate the value of the double ordinal recursion operator. (Contributed by Scott Fenton, 3-Sep-2024)

		Ref	Expression
	Hypothesis	on2recs.1	$⊢ F = frecs (\{⟨x, y⟩ \| (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\}, On \times On, G)$
	Assertion	on2recsov	$⊢ (A \in On \land B \in On) \to A F B = ⟨A, B⟩ G ({F ↾}_{((suc A \times suc B) ∖ \{⟨A, B⟩\})})$

Proof

Step	Hyp	Ref	Expression
1		on2recs.1	$⊢ F = frecs (\{⟨x, y⟩ \| (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\}, On \times On, G)$
2		df-ov	$⊢ A F B = F (⟨A, B⟩)$
3		opelxp	$⊢ ⟨A, B⟩ \in (On \times On) \leftrightarrow (A \in On \land B \in On)$
4		eqid	$⊢ \{⟨x, y⟩ \| (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\} = \{⟨x, y⟩ \| (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\}$
5		onfr	$⊢ E Fr On$
6	5	a1i	$⊢ ⊤ \to E Fr On$
7	4 6 6	frxp2	$⊢ ⊤ \to \{⟨x, y⟩ \| (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\} Fr (On \times On)$
8	7	mptru	$⊢ \{⟨x, y⟩ \| (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\} Fr (On \times On)$
9		epweon	$⊢ E We On$
10		weso	$⊢ E We On \to E Or On$
11		sopo	$⊢ E Or On \to E Po On$
12	9 10 11	mp2b	$⊢ E Po On$
13	12	a1i	$⊢ ⊤ \to E Po On$
14	4 13 13	poxp2	$⊢ ⊤ \to \{⟨x, y⟩ \| (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\} Po (On \times On)$
15	14	mptru	$⊢ \{⟨x, y⟩ \| (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\} Po (On \times On)$
16		epse	$⊢ E Se On$
17	16	a1i	$⊢ ⊤ \to E Se On$
18	4 17 17	sexp2	$⊢ ⊤ \to \{⟨x, y⟩ \| (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\} Se (On \times On)$
19	18	mptru	$⊢ \{⟨x, y⟩ \| (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\} Se (On \times On)$
20	8 15 19	3pm3.2i	$⊢ (\{⟨x, y⟩ \| (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\} Fr (On \times On) \land \{⟨x, y⟩ \| (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\} Po (On \times On) \land \{⟨x, y⟩ \| (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\} Se (On \times On))$
21	1	fpr2	$⊢ ((\{⟨x, y⟩ \| (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\} Fr (On \times On) \land \{⟨x, y⟩ \| (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\} Po (On \times On) \land \{⟨x, y⟩ \| (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\} Se (On \times On)) \land ⟨A, B⟩ \in (On \times On)) \to F (⟨A, B⟩) = ⟨A, B⟩ G ({F ↾}_{Pred (\{⟨x, y⟩ \| (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\}, (On \times On), ⟨A, B⟩)})$
22	20 21	mpan	$⊢ ⟨A, B⟩ \in (On \times On) \to F (⟨A, B⟩) = ⟨A, B⟩ G ({F ↾}_{Pred (\{⟨x, y⟩ \| (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\}, (On \times On), ⟨A, B⟩)})$
23	3 22	sylbir	$⊢ (A \in On \land B \in On) \to F (⟨A, B⟩) = ⟨A, B⟩ G ({F ↾}_{Pred (\{⟨x, y⟩ \| (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\}, (On \times On), ⟨A, B⟩)})$
24	2 23	syl5eq	$⊢ (A \in On \land B \in On) \to A F B = ⟨A, B⟩ G ({F ↾}_{Pred (\{⟨x, y⟩ \| (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\}, (On \times On), ⟨A, B⟩)})$
25	4	xpord2pred	$⊢ (A \in On \land B \in On) \to Pred (\{⟨x, y⟩ \| (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\}, (On \times On), ⟨A, B⟩) = ((Pred (E, On, A) \cup \{A\}) \times (Pred (E, On, B) \cup \{B\})) ∖ \{⟨A, B⟩\}$
26		predon	$⊢ A \in On \to Pred (E, On, A) = A$
27	26	adantr	$⊢ (A \in On \land B \in On) \to Pred (E, On, A) = A$
28	27	uneq1d	$⊢ (A \in On \land B \in On) \to Pred (E, On, A) \cup \{A\} = A \cup \{A\}$
29		df-suc	$⊢ suc A = A \cup \{A\}$
30	28 29	eqtr4di	$⊢ (A \in On \land B \in On) \to Pred (E, On, A) \cup \{A\} = suc A$
31		predon	$⊢ B \in On \to Pred (E, On, B) = B$
32	31	adantl	$⊢ (A \in On \land B \in On) \to Pred (E, On, B) = B$
33	32	uneq1d	$⊢ (A \in On \land B \in On) \to Pred (E, On, B) \cup \{B\} = B \cup \{B\}$
34		df-suc	$⊢ suc B = B \cup \{B\}$
35	33 34	eqtr4di	$⊢ (A \in On \land B \in On) \to Pred (E, On, B) \cup \{B\} = suc B$
36	30 35	xpeq12d	$⊢ (A \in On \land B \in On) \to (Pred (E, On, A) \cup \{A\}) \times (Pred (E, On, B) \cup \{B\}) = suc A \times suc B$
37	36	difeq1d	$⊢ (A \in On \land B \in On) \to ((Pred (E, On, A) \cup \{A\}) \times (Pred (E, On, B) \cup \{B\})) ∖ \{⟨A, B⟩\} = (suc A \times suc B) ∖ \{⟨A, B⟩\}$
38	25 37	eqtrd	$⊢ (A \in On \land B \in On) \to Pred (\{⟨x, y⟩ \| (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\}, (On \times On), ⟨A, B⟩) = (suc A \times suc B) ∖ \{⟨A, B⟩\}$
39	38	reseq2d	$⊢ (A \in On \land B \in On) \to {F ↾}_{Pred (\{⟨x, y⟩ \| (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\}, (On \times On), ⟨A, B⟩)} = {F ↾}_{((suc A \times suc B) ∖ \{⟨A, B⟩\})}$
40	39	oveq2d	$⊢ (A \in On \land B \in On) \to ⟨A, B⟩ G ({F ↾}_{Pred (\{⟨x, y⟩ \| (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\}, (On \times On), ⟨A, B⟩)}) = ⟨A, B⟩ G ({F ↾}_{((suc A \times suc B) ∖ \{⟨A, B⟩\})})$
41	24 40	eqtrd	$⊢ (A \in On \land B \in On) \to A F B = ⟨A, B⟩ G ({F ↾}_{((suc A \times suc B) ∖ \{⟨A, B⟩\})})$

Metamath Proof Explorer

Theorem on2recsov

Proof