This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oieq2

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

Ref Expression
Assertion oieq2 
|- ( A = B -> OrdIso ( R , A ) = OrdIso ( R , B ) )

Proof

Step Hyp Ref Expression
1 weeq2 
 |-  ( A = B -> ( R We A <-> R We B ) )
2 seeq2 
 |-  ( A = B -> ( R Se A <-> R Se B ) )
3 1 2 anbi12d 
 |-  ( A = B -> ( ( R We A /\ R Se A ) <-> ( R We B /\ R Se B ) ) )
4 rabeq 
 |-  ( A = B -> { w e. A | A. j e. ran h j R w } = { w e. B | A. j e. ran h j R w } )
5 4 raleqdv 
 |-  ( A = B -> ( A. u e. { w e. A | A. j e. ran h j R w } -. u R v <-> A. u e. { w e. B | A. j e. ran h j R w } -. u R v ) )
6 4 5 riotaeqbidv 
 |-  ( A = B -> ( 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. B | A. j e. ran h j R w } A. u e. { w e. B | A. j e. ran h j R w } -. u R v ) )
7 6 mpteq2dv 
 |-  ( A = B -> ( 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. B | A. j e. ran h j R w } A. u e. { w e. B | A. j e. ran h j R w } -. u R v ) ) )
8 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. B | A. j e. ran h j R w } A. u e. { w e. B | 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 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. B | A. j e. ran h j R w } A. u e. { w e. B | A. j e. ran h j R w } -. u R v ) ) ) )
9 7 8 syl 
 |-  ( A = B -> 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. B | A. j e. ran h j R w } A. u e. { w e. B | A. j e. ran h j R w } -. u R v ) ) ) )
10 9 imaeq1d 
 |-  ( A = B -> ( 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. B | A. j e. ran h j R w } A. u e. { w e. B | A. j e. ran h j R w } -. u R v ) ) ) " x ) )
11 10 raleqdv 
 |-  ( A = B -> ( 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. B | A. j e. ran h j R w } A. u e. { w e. B | A. j e. ran h j R w } -. u R v ) ) ) " x ) z R t ) )
12 11 rexeqbi1dv 
 |-  ( A = B -> ( 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. B A. z e. ( recs ( ( h e. _V |-> ( iota_ v e. { w e. B | A. j e. ran h j R w } A. u e. { w e. B | A. j e. ran h j R w } -. u R v ) ) ) " x ) z R t ) )
13 12 rabbidv 
 |-  ( A = B -> { 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. B A. z e. ( recs ( ( h e. _V |-> ( iota_ v e. { w e. B | A. j e. ran h j R w } A. u e. { w e. B | A. j e. ran h j R w } -. u R v ) ) ) " x ) z R t } )
14 9 13 reseq12d 
 |-  ( A = B -> ( 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. B | A. j e. ran h j R w } A. u e. { w e. B | A. j e. ran h j R w } -. u R v ) ) ) |` { x e. On | E. t e. B A. z e. ( recs ( ( h e. _V |-> ( iota_ v e. { w e. B | A. j e. ran h j R w } A. u e. { w e. B | A. j e. ran h j R w } -. u R v ) ) ) " x ) z R t } ) )
15 3 14 ifbieq1d 
 |-  ( A = B -> 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 ( ( R We B /\ R Se B ) , ( recs ( ( h e. _V |-> ( iota_ v e. { w e. B | A. j e. ran h j R w } A. u e. { w e. B | A. j e. ran h j R w } -. u R v ) ) ) |` { x e. On | E. t e. B A. z e. ( recs ( ( h e. _V |-> ( iota_ v e. { w e. B | A. j e. ran h j R w } A. u e. { w e. B | A. j e. ran h j R w } -. u R v ) ) ) " x ) z R t } ) , (/) ) )
16 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 } ) , (/) )
17 df-oi 
 |-  OrdIso ( R , B ) = if ( ( R We B /\ R Se B ) , ( recs ( ( h e. _V |-> ( iota_ v e. { w e. B | A. j e. ran h j R w } A. u e. { w e. B | A. j e. ran h j R w } -. u R v ) ) ) |` { x e. On | E. t e. B A. z e. ( recs ( ( h e. _V |-> ( iota_ v e. { w e. B | A. j e. ran h j R w } A. u e. { w e. B | A. j e. ran h j R w } -. u R v ) ) ) " x ) z R t } ) , (/) )
18 15 16 17 3eqtr4g 
 |-  ( A = B -> OrdIso ( R , A ) = OrdIso ( R , B ) )