Metamath Proof Explorer

Theorem on2recsfn

Description: Show that double recursion over ordinals yields a function over pairs of ordinals. (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	on2recsfn	$⊢ F Fn (On \times On)$

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		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))\}$
3		onfr	$⊢ E Fr On$
4	3	a1i	$⊢ ⊤ \to E Fr On$
5	2 4 4	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)$
6	5	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)$
7		epweon	$⊢ E We On$
8		weso	$⊢ E We On \to E Or On$
9		sopo	$⊢ E Or On \to E Po On$
10	7 8 9	mp2b	$⊢ E Po On$
11	10	a1i	$⊢ ⊤ \to E Po On$
12	2 11 11	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)$
13	12	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)$
14		epse	$⊢ E Se On$
15	14	a1i	$⊢ ⊤ \to E Se On$
16	2 15 15	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)$
17	16	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)$
18	1	fpr1	$⊢ (\{⟨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)) \to F Fn (On \times On)$
19	6 13 17 18	mp3an	$⊢ F Fn (On \times On)$