Metamath Proof Explorer

Theorem dfoi

Description: Rewrite df-oi with abbreviations. (Contributed by Mario Carneiro, 24-Jun-2015)

Ref Expression
Hypotheses dfoi.1 
|- C = { w e. A | A. j e. ran h j R w }
dfoi.2 
|- G = ( h e. _V |-> ( iota_ v e. C A. u e. C -. u R v ) )
dfoi.3 
|- F = recs ( G )
Assertion dfoi 
|- OrdIso ( R , A ) = if ( ( R We A /\ R Se A ) , ( F |` { x e. On | E. t e. A A. z e. ( F " x ) z R t } ) , (/) )

Proof

Step Hyp Ref Expression
1 dfoi.1 
 |-  C = { w e. A | A. j e. ran h j R w }
2 dfoi.2 
 |-  G = ( h e. _V |-> ( iota_ v e. C A. u e. C -. u R v ) )
3 dfoi.3 
 |-  F = recs ( G )
4 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 } ) , (/) )
5 1 a1i 
 |-  ( h e. _V -> C = { w e. A | A. j e. ran h j R w } )
6 5 raleqdv 
 |-  ( h e. _V -> ( A. u e. C -. u R v <-> A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) )
7 5 6 riotaeqbidv 
 |-  ( h e. _V -> ( iota_ v e. C A. u e. C -. u R 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 ) )
8 7 mpteq2ia 
 |-  ( h e. _V |-> ( iota_ v e. C A. u e. C -. u R v ) ) = ( 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 ) )
9 2 8 eqtri 
 |-  G = ( 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 ) )
10 recseq 
 |-  ( G = ( 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 ( G ) = 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 ) ) ) )
11 9 10 ax-mp 
 |-  recs ( G ) = 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 ) ) )
12 3 11 eqtri 
 |-  F = 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 ) ) )
13 12 imaeq1i 
 |-  ( F " x ) = ( 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 )
14 13 raleqi 
 |-  ( A. z e. ( F " x ) z R t <-> 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 )
15 14 rexbii 
 |-  ( E. t e. A A. z e. ( F " 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 R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) " x ) z R t )
16 15 rabbii 
 |-  { x e. On | E. t e. A A. z e. ( F " 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 R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) ) " x ) z R t }
17 12 16 reseq12i 
 |-  ( F |` { x e. On | E. t e. A A. z e. ( F " x ) z R t } ) = ( 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 } )
18 ifeq1 
 |-  ( ( F |` { x e. On | E. t e. A A. z e. ( F " x ) z R t } ) = ( 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 A /\ R Se A ) , ( F |` { x e. On | E. t e. A A. z e. ( F " x ) z R t } ) , (/) ) = 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 } ) , (/) ) )
19 17 18 ax-mp 
 |-  if ( ( R We A /\ R Se A ) , ( F |` { x e. On | E. t e. A A. z e. ( F " x ) z R t } ) , (/) ) = 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 } ) , (/) )
20 4 19 eqtr4i 
 |-  OrdIso ( R , A ) = if ( ( R We A /\ R Se A ) , ( F |` { x e. On | E. t e. A A. z e. ( F " x ) z R t } ) , (/) )