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

Metamath Proof Explorer

Theorem ordtypecbv

Description: Lemma for ordtype . (Contributed by Mario Carneiro, 26-Jun-2015)

Ref Expression
Hypotheses ordtypelem.1 
|- F = recs ( G )
ordtypelem.2 
|- C = { w e. A | A. j e. ran h j R w }
ordtypelem.3 
|- G = ( h e. _V |-> ( iota_ v e. C A. u e. C -. u R v ) )
Assertion ordtypecbv 
|- recs ( ( f e. _V |-> ( iota_ s e. { y e. A | A. i e. ran f i R y } A. r e. { y e. A | A. i e. ran f i R y } -. r R s ) ) ) = F

Proof

Step Hyp Ref Expression
1 ordtypelem.1 
 |-  F = recs ( G )
2 ordtypelem.2 
 |-  C = { w e. A | A. j e. ran h j R w }
3 ordtypelem.3 
 |-  G = ( h e. _V |-> ( iota_ v e. C A. u e. C -. u R v ) )
4 breq1 
 |-  ( u = r -> ( u R v <-> r R v ) )
5 4 notbid 
 |-  ( u = r -> ( -. u R v <-> -. r R v ) )
6 5 cbvralvw 
 |-  ( A. u e. C -. u R v <-> A. r e. C -. r R v )
7 breq2 
 |-  ( v = s -> ( r R v <-> r R s ) )
8 7 notbid 
 |-  ( v = s -> ( -. r R v <-> -. r R s ) )
9 8 ralbidv 
 |-  ( v = s -> ( A. r e. C -. r R v <-> A. r e. C -. r R s ) )
10 6 9 bitrid 
 |-  ( v = s -> ( A. u e. C -. u R v <-> A. r e. C -. r R s ) )
11 10 cbvriotavw 
 |-  ( iota_ v e. C A. u e. C -. u R v ) = ( iota_ s e. C A. r e. C -. r R s )
12 breq1 
 |-  ( j = i -> ( j R w <-> i R w ) )
13 12 cbvralvw 
 |-  ( A. j e. ran h j R w <-> A. i e. ran h i R w )
14 breq2 
 |-  ( w = y -> ( i R w <-> i R y ) )
15 14 ralbidv 
 |-  ( w = y -> ( A. i e. ran h i R w <-> A. i e. ran h i R y ) )
16 13 15 bitrid 
 |-  ( w = y -> ( A. j e. ran h j R w <-> A. i e. ran h i R y ) )
17 16 cbvrabv 
 |-  { w e. A | A. j e. ran h j R w } = { y e. A | A. i e. ran h i R y }
18 2 17 eqtri 
 |-  C = { y e. A | A. i e. ran h i R y }
19 rneq 
 |-  ( h = f -> ran h = ran f )
20 19 raleqdv 
 |-  ( h = f -> ( A. i e. ran h i R y <-> A. i e. ran f i R y ) )
21 20 rabbidv 
 |-  ( h = f -> { y e. A | A. i e. ran h i R y } = { y e. A | A. i e. ran f i R y } )
22 18 21 eqtrid 
 |-  ( h = f -> C = { y e. A | A. i e. ran f i R y } )
23 22 raleqdv 
 |-  ( h = f -> ( A. r e. C -. r R s <-> A. r e. { y e. A | A. i e. ran f i R y } -. r R s ) )
24 22 23 riotaeqbidv 
 |-  ( h = f -> ( iota_ s e. C A. r e. C -. r R s ) = ( iota_ s e. { y e. A | A. i e. ran f i R y } A. r e. { y e. A | A. i e. ran f i R y } -. r R s ) )
25 11 24 eqtrid 
 |-  ( h = f -> ( iota_ v e. C A. u e. C -. u R v ) = ( iota_ s e. { y e. A | A. i e. ran f i R y } A. r e. { y e. A | A. i e. ran f i R y } -. r R s ) )
26 25 cbvmptv 
 |-  ( h e. _V |-> ( iota_ v e. C A. u e. C -. u R v ) ) = ( f e. _V |-> ( iota_ s e. { y e. A | A. i e. ran f i R y } A. r e. { y e. A | A. i e. ran f i R y } -. r R s ) )
27 3 26 eqtri 
 |-  G = ( f e. _V |-> ( iota_ s e. { y e. A | A. i e. ran f i R y } A. r e. { y e. A | A. i e. ran f i R y } -. r R s ) )
28 recseq 
 |-  ( G = ( f e. _V |-> ( iota_ s e. { y e. A | A. i e. ran f i R y } A. r e. { y e. A | A. i e. ran f i R y } -. r R s ) ) -> recs ( G ) = recs ( ( f e. _V |-> ( iota_ s e. { y e. A | A. i e. ran f i R y } A. r e. { y e. A | A. i e. ran f i R y } -. r R s ) ) ) )
29 27 28 ax-mp 
 |-  recs ( G ) = recs ( ( f e. _V |-> ( iota_ s e. { y e. A | A. i e. ran f i R y } A. r e. { y e. A | A. i e. ran f i R y } -. r R s ) ) )
30 1 29 eqtr2i 
 |-  recs ( ( f e. _V |-> ( iota_ s e. { y e. A | A. i e. ran f i R y } A. r e. { y e. A | A. i e. ran f i R y } -. r R s ) ) ) = F