Metamath Proof Explorer


Theorem 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 On × On y On × On 1 st x E 1 st y 1 st x = 1 st y 2 nd x E 2 nd y 2 nd x = 2 nd y x y On × On G
Assertion on2recsov A On B On A F B = A B G F suc A × suc B A B

Proof

Step Hyp Ref Expression
1 on2recs.1 F = frecs x y | x On × On y On × On 1 st x E 1 st y 1 st x = 1 st y 2 nd x E 2 nd y 2 nd x = 2 nd y x y On × On G
2 df-ov A F B = F A B
3 opelxp A B On × On A On B On
4 eqid x y | x On × On y On × On 1 st x E 1 st y 1 st x = 1 st y 2 nd x E 2 nd y 2 nd x = 2 nd y x y = x y | x On × On y On × On 1 st x E 1 st y 1 st x = 1 st y 2 nd x E 2 nd y 2 nd x = 2 nd y x y
5 onfr E Fr On
6 5 a1i E Fr On
7 4 6 6 frxp2 x y | x On × On y On × On 1 st x E 1 st y 1 st x = 1 st y 2 nd x E 2 nd y 2 nd x = 2 nd y x y Fr On × On
8 7 mptru x y | x On × On y On × On 1 st x E 1 st y 1 st x = 1 st y 2 nd x E 2 nd y 2 nd x = 2 nd y x y 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 x y | x On × On y On × On 1 st x E 1 st y 1 st x = 1 st y 2 nd x E 2 nd y 2 nd x = 2 nd y x y Po On × On
15 14 mptru x y | x On × On y On × On 1 st x E 1 st y 1 st x = 1 st y 2 nd x E 2 nd y 2 nd x = 2 nd y x y Po On × On
16 epse E Se On
17 16 a1i E Se On
18 4 17 17 sexp2 x y | x On × On y On × On 1 st x E 1 st y 1 st x = 1 st y 2 nd x E 2 nd y 2 nd x = 2 nd y x y Se On × On
19 18 mptru x y | x On × On y On × On 1 st x E 1 st y 1 st x = 1 st y 2 nd x E 2 nd y 2 nd x = 2 nd y x y Se On × On
20 8 15 19 3pm3.2i x y | x On × On y On × On 1 st x E 1 st y 1 st x = 1 st y 2 nd x E 2 nd y 2 nd x = 2 nd y x y Fr On × On x y | x On × On y On × On 1 st x E 1 st y 1 st x = 1 st y 2 nd x E 2 nd y 2 nd x = 2 nd y x y Po On × On x y | x On × On y On × On 1 st x E 1 st y 1 st x = 1 st y 2 nd x E 2 nd y 2 nd x = 2 nd y x y Se On × On
21 1 fpr2 x y | x On × On y On × On 1 st x E 1 st y 1 st x = 1 st y 2 nd x E 2 nd y 2 nd x = 2 nd y x y Fr On × On x y | x On × On y On × On 1 st x E 1 st y 1 st x = 1 st y 2 nd x E 2 nd y 2 nd x = 2 nd y x y Po On × On x y | x On × On y On × On 1 st x E 1 st y 1 st x = 1 st y 2 nd x E 2 nd y 2 nd x = 2 nd y x y Se On × On A B On × On F A B = A B G F Pred x y | x On × On y On × On 1 st x E 1 st y 1 st x = 1 st y 2 nd x E 2 nd y 2 nd x = 2 nd y x y On × On A B
22 20 21 mpan A B On × On F A B = A B G F Pred x y | x On × On y On × On 1 st x E 1 st y 1 st x = 1 st y 2 nd x E 2 nd y 2 nd x = 2 nd y x y On × On A B
23 3 22 sylbir A On B On F A B = A B G F Pred x y | x On × On y On × On 1 st x E 1 st y 1 st x = 1 st y 2 nd x E 2 nd y 2 nd x = 2 nd y x y On × On A B
24 2 23 syl5eq A On B On A F B = A B G F Pred x y | x On × On y On × On 1 st x E 1 st y 1 st x = 1 st y 2 nd x E 2 nd y 2 nd x = 2 nd y x y On × On A B
25 4 xpord2pred A On B On Pred x y | x On × On y On × On 1 st x E 1 st y 1 st x = 1 st y 2 nd x E 2 nd y 2 nd x = 2 nd y x y On × On A B = Pred E On A A × Pred E On B B A B
26 predon A On Pred E On A = A
27 26 adantr A On B On Pred E On A = A
28 27 uneq1d A On B On Pred E On A A = A A
29 df-suc suc A = A A
30 28 29 eqtr4di A On B On Pred E On A A = suc A
31 predon B On Pred E On B = B
32 31 adantl A On B On Pred E On B = B
33 32 uneq1d A On B On Pred E On B B = B B
34 df-suc suc B = B B
35 33 34 eqtr4di A On B On Pred E On B B = suc B
36 30 35 xpeq12d A On B On Pred E On A A × Pred E On B B = suc A × suc B
37 36 difeq1d A On B On Pred E On A A × Pred E On B B A B = suc A × suc B A B
38 25 37 eqtrd A On B On Pred x y | x On × On y On × On 1 st x E 1 st y 1 st x = 1 st y 2 nd x E 2 nd y 2 nd x = 2 nd y x y On × On A B = suc A × suc B A B
39 38 reseq2d A On B On F Pred x y | x On × On y On × On 1 st x E 1 st y 1 st x = 1 st y 2 nd x E 2 nd y 2 nd x = 2 nd y x y On × On A B = F suc A × suc B A B
40 39 oveq2d A On B On A B G F Pred x y | x On × On y On × On 1 st x E 1 st y 1 st x = 1 st y 2 nd x E 2 nd y 2 nd x = 2 nd y x y On × On A B = A B G F suc A × suc B A B
41 24 40 eqtrd A On B On A F B = A B G F suc A × suc B A B