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	⊢ 𝐹 = frecs ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1^st ‘ 𝑥 ) E ( 1^st ‘ 𝑦 ) ∨ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) E ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } , ( On × On ) , 𝐺 )
	Assertion	on2recsfn	⊢ 𝐹 Fn ( On × On )

Proof

Step	Hyp	Ref	Expression
1		on2recs.1	⊢ 𝐹 = frecs ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1^st ‘ 𝑥 ) E ( 1^st ‘ 𝑦 ) ∨ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) E ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } , ( On × On ) , 𝐺 )
2		eqid	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1^st ‘ 𝑥 ) E ( 1^st ‘ 𝑦 ) ∨ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) E ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1^st ‘ 𝑥 ) E ( 1^st ‘ 𝑦 ) ∨ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) E ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) }
3		onfr	⊢ E Fr On
4	3	a1i	⊢ ( ⊤ → E Fr On )
5	2 4 4	frxp2	⊢ ( ⊤ → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1^st ‘ 𝑥 ) E ( 1^st ‘ 𝑦 ) ∨ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) E ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } Fr ( On × On ) )
6	5	mptru	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1^st ‘ 𝑥 ) E ( 1^st ‘ 𝑦 ) ∨ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) E ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } Fr ( On × On )
7		epweon	⊢ E We On
8		weso	⊢ ( E We On → E Or On )
9		sopo	⊢ ( E Or On → E Po On )
10	7 8 9	mp2b	⊢ E Po On
11	10	a1i	⊢ ( ⊤ → E Po On )
12	2 11 11	poxp2	⊢ ( ⊤ → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1^st ‘ 𝑥 ) E ( 1^st ‘ 𝑦 ) ∨ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) E ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } Po ( On × On ) )
13	12	mptru	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1^st ‘ 𝑥 ) E ( 1^st ‘ 𝑦 ) ∨ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) E ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } Po ( On × On )
14		epse	⊢ E Se On
15	14	a1i	⊢ ( ⊤ → E Se On )
16	2 15 15	sexp2	⊢ ( ⊤ → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1^st ‘ 𝑥 ) E ( 1^st ‘ 𝑦 ) ∨ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) E ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } Se ( On × On ) )
17	16	mptru	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1^st ‘ 𝑥 ) E ( 1^st ‘ 𝑦 ) ∨ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) E ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } Se ( On × On )
18	1	fpr1	⊢ ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1^st ‘ 𝑥 ) E ( 1^st ‘ 𝑦 ) ∨ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) E ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } Fr ( On × On ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1^st ‘ 𝑥 ) E ( 1^st ‘ 𝑦 ) ∨ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) E ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } Po ( On × On ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1^st ‘ 𝑥 ) E ( 1^st ‘ 𝑦 ) ∨ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) E ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } Se ( On × On ) ) → 𝐹 Fn ( On × On ) )
19	6 13 17 18	mp3an	⊢ 𝐹 Fn ( On × On )