on2recsov

Description: Calculate the value of the double ordinal recursion operator. (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	on2recsov	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 𝐹 𝐵 ) = ( ⟨ 𝐴 , 𝐵 ⟩ 𝐺 ( 𝐹 ↾ ( ( suc 𝐴 × suc 𝐵 ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ) )

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		df-ov	⊢ ( 𝐴 𝐹 𝐵 ) = ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
3		opelxp	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( On × On ) ↔ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) )
4		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 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) }
5		onfr	⊢ E Fr On
6	5	a1i	⊢ ( ⊤ → E Fr On )
7	4 6 6	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 ) )
8	7	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 )
9		epweon	⊢ E We On
10		weso	⊢ ( E We On → E Or On )
11		sopo	⊢ ( E Or On → E Po On )
12	9 10 11	mp2b	⊢ E Po On
13	12	a1i	⊢ ( ⊤ → E Po On )
14	4 13 13	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 ) )
15	14	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 )
16		epse	⊢ E Se On
17	16	a1i	⊢ ( ⊤ → E Se On )
18	4 17 17	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 ) )
19	18	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 )
20	8 15 19	3pm3.2i	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 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 ) )
21	1	fpr2	⊢ ( ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 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 ) ) ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( On × On ) ) → ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ⟨ 𝐴 , 𝐵 ⟩ 𝐺 ( 𝐹 ↾ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1^st ‘ 𝑥 ) E ( 1^st ‘ 𝑦 ) ∨ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) E ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } , ( On × On ) , ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
22	20 21	mpan	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( On × On ) → ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ⟨ 𝐴 , 𝐵 ⟩ 𝐺 ( 𝐹 ↾ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1^st ‘ 𝑥 ) E ( 1^st ‘ 𝑦 ) ∨ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) E ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } , ( On × On ) , ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
23	3 22	sylbir	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ⟨ 𝐴 , 𝐵 ⟩ 𝐺 ( 𝐹 ↾ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1^st ‘ 𝑥 ) E ( 1^st ‘ 𝑦 ) ∨ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) E ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } , ( On × On ) , ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
24	2 23	syl5eq	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 𝐹 𝐵 ) = ( ⟨ 𝐴 , 𝐵 ⟩ 𝐺 ( 𝐹 ↾ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1^st ‘ 𝑥 ) E ( 1^st ‘ 𝑦 ) ∨ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) E ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } , ( On × On ) , ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
25	4	xpord2pred	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1^st ‘ 𝑥 ) E ( 1^st ‘ 𝑦 ) ∨ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) E ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } , ( On × On ) , ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( ( Pred ( E , On , 𝐴 ) ∪ { 𝐴 } ) × ( Pred ( E , On , 𝐵 ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
26		predon	⊢ ( 𝐴 ∈ On → Pred ( E , On , 𝐴 ) = 𝐴 )
27	26	adantr	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → Pred ( E , On , 𝐴 ) = 𝐴 )
28	27	uneq1d	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( Pred ( E , On , 𝐴 ) ∪ { 𝐴 } ) = ( 𝐴 ∪ { 𝐴 } ) )
29		df-suc	⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
30	28 29	eqtr4di	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( Pred ( E , On , 𝐴 ) ∪ { 𝐴 } ) = suc 𝐴 )
31		predon	⊢ ( 𝐵 ∈ On → Pred ( E , On , 𝐵 ) = 𝐵 )
32	31	adantl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → Pred ( E , On , 𝐵 ) = 𝐵 )
33	32	uneq1d	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( Pred ( E , On , 𝐵 ) ∪ { 𝐵 } ) = ( 𝐵 ∪ { 𝐵 } ) )
34		df-suc	⊢ suc 𝐵 = ( 𝐵 ∪ { 𝐵 } )
35	33 34	eqtr4di	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( Pred ( E , On , 𝐵 ) ∪ { 𝐵 } ) = suc 𝐵 )
36	30 35	xpeq12d	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( Pred ( E , On , 𝐴 ) ∪ { 𝐴 } ) × ( Pred ( E , On , 𝐵 ) ∪ { 𝐵 } ) ) = ( suc 𝐴 × suc 𝐵 ) )
37	36	difeq1d	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( ( Pred ( E , On , 𝐴 ) ∪ { 𝐴 } ) × ( Pred ( E , On , 𝐵 ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) = ( ( suc 𝐴 × suc 𝐵 ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
38	25 37	eqtrd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1^st ‘ 𝑥 ) E ( 1^st ‘ 𝑦 ) ∨ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) E ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } , ( On × On ) , ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( suc 𝐴 × suc 𝐵 ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
39	38	reseq2d	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐹 ↾ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1^st ‘ 𝑥 ) E ( 1^st ‘ 𝑦 ) ∨ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) E ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } , ( On × On ) , ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( 𝐹 ↾ ( ( suc 𝐴 × suc 𝐵 ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) )
40	39	oveq2d	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ⟨ 𝐴 , 𝐵 ⟩ 𝐺 ( 𝐹 ↾ Pred ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1^st ‘ 𝑥 ) E ( 1^st ‘ 𝑦 ) ∨ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) E ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } , ( On × On ) , ⟨ 𝐴 , 𝐵 ⟩ ) ) ) = ( ⟨ 𝐴 , 𝐵 ⟩ 𝐺 ( 𝐹 ↾ ( ( suc 𝐴 × suc 𝐵 ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ) )
41	24 40	eqtrd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 𝐹 𝐵 ) = ( ⟨ 𝐴 , 𝐵 ⟩ 𝐺 ( 𝐹 ↾ ( ( suc 𝐴 × suc 𝐵 ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ) )

Metamath Proof Explorer

Theorem on2recsov

Proof