Metamath Proof Explorer

Theorem oieq1

Description: Equality theorem for ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015)

Ref Expression
Assertion oieq1 
|- ( R = S -> OrdIso ( R , A ) = OrdIso ( S , A ) )

Proof

Step Hyp Ref Expression
1 weeq1 
 |-  ( R = S -> ( R We A <-> S We A ) )
2 seeq1 
 |-  ( R = S -> ( R Se A <-> S Se A ) )
3 1 2 anbi12d 
 |-  ( R = S -> ( ( R We A /\ R Se A ) <-> ( S We A /\ S Se A ) ) )
4 breq 
 |-  ( R = S -> ( j R w <-> j S w ) )
5 4 ralbidv 
 |-  ( R = S -> ( A. j e. ran h j R w <-> A. j e. ran h j S w ) )
6 5 rabbidv 
 |-  ( R = S -> { w e. A | A. j e. ran h j R w } = { w e. A | A. j e. ran h j S w } )
7 breq 
 |-  ( R = S -> ( u R v <-> u S v ) )
8 7 notbid 
 |-  ( R = S -> ( -. u R v <-> -. u S v ) )
9 6 8 raleqbidv 
 |-  ( R = S -> ( A. u e. { w e. A | A. j e. ran h j R w } -. u R v <-> A. u e. { w e. A | A. j e. ran h j S w } -. u S v ) )
10 6 9 riotaeqbidv 
 |-  ( R = S -> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) = ( iota_ v e. { w e. A | A. j e. ran h j S w } A. u e. { w e. A | A. j e. ran h j S w } -. u S v ) )
11 10 mpteq2dv 
 |-  ( R = S -> ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) = ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j S w } A. u e. { w e. A | A. j e. ran h j S w } -. u S v ) ) )
12 recseq 
 |-  ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) = ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j S w } A. u e. { w e. A | A. j e. ran h j S w } -. u S v ) ) -> recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) = recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j S w } A. u e. { w e. A | A. j e. ran h j S w } -. u S v ) ) ) )
13 11 12 syl 
 |-  ( R = S -> recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) = recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j S w } A. u e. { w e. A | A. j e. ran h j S w } -. u S v ) ) ) )
14 13 imaeq1d 
 |-  ( R = S -> ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) " x ) = ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j S w } A. u e. { w e. A | A. j e. ran h j S w } -. u S v ) ) ) " x ) )
15 breq 
 |-  ( R = S -> ( z R t <-> z S t ) )
16 14 15 raleqbidv 
 |-  ( R = S -> ( A. z e. ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) " x ) z R t <-> A. z e. ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j S w } A. u e. { w e. A | A. j e. ran h j S w } -. u S v ) ) ) " x ) z S t ) )
17 16 rexbidv 
 |-  ( R = S -> ( E. t e. A A. z e. ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) " x ) z R t <-> E. t e. A A. z e. ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j S w } A. u e. { w e. A | A. j e. ran h j S w } -. u S v ) ) ) " x ) z S t ) )
18 17 rabbidv 
 |-  ( R = S -> { x e. On | E. t e. A A. z e. ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) " x ) z R t } = { x e. On | E. t e. A A. z e. ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j S w } A. u e. { w e. A | A. j e. ran h j S w } -. u S v ) ) ) " x ) z S t } )
19 13 18 reseq12d 
 |-  ( R = S -> ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) |` { x e. On | E. t e. A A. z e. ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) " x ) z R t } ) = ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j S w } A. u e. { w e. A | A. j e. ran h j S w } -. u S v ) ) ) |` { x e. On | E. t e. A A. z e. ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j S w } A. u e. { w e. A | A. j e. ran h j S w } -. u S v ) ) ) " x ) z S t } ) )
20 3 19 ifbieq1d 
 |-  ( R = S -> if ( ( R We A /\ R Se A ) , ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) |` { x e. On | E. t e. A A. z e. ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) " x ) z R t } ) , (/) ) = if ( ( S We A /\ S Se A ) , ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j S w } A. u e. { w e. A | A. j e. ran h j S w } -. u S v ) ) ) |` { x e. On | E. t e. A A. z e. ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j S w } A. u e. { w e. A | A. j e. ran h j S w } -. u S v ) ) ) " x ) z S t } ) , (/) ) )
21 df-oi 
 |-  OrdIso ( R , A ) = if ( ( R We A /\ R Se A ) , ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) |` { x e. On | E. t e. A A. z e. ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) " x ) z R t } ) , (/) )
22 df-oi 
 |-  OrdIso ( S , A ) = if ( ( S We A /\ S Se A ) , ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j S w } A. u e. { w e. A | A. j e. ran h j S w } -. u S v ) ) ) |` { x e. On | E. t e. A A. z e. ( recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j S w } A. u e. { w e. A | A. j e. ran h j S w } -. u S v ) ) ) " x ) z S t } ) , (/) )
23 20 21 22 3eqtr4g 
 |-  ( R = S -> OrdIso ( R , A ) = OrdIso ( S , A ) )