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 e. ( On X. On ) /\ y e. ( On X. On ) /\ ( ( ( 1st ` x ) _E ( 1st ` y ) \/ ( 1st ` x ) = ( 1st ` y ) ) /\ ( ( 2nd ` x ) _E ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) /\ x =/= y ) ) } , ( On X. On ) , G )
Assertion on2recsov 
|- ( ( A e. On /\ B e. On ) -> ( A F B ) = ( <. A , B >. G ( F |` ( ( suc A X. suc B ) \ { <. A , B >. } ) ) ) )

Proof

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