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 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 on2recsfn F Fn On × On

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 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
3 onfr E Fr On
4 3 a1i E Fr On
5 2 4 4 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
6 5 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
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 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
13 12 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
14 epse E Se On
15 14 a1i E Se On
16 2 15 15 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
17 16 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
18 1 fpr1 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 F Fn On × On
19 6 13 17 18 mp3an F Fn On × On