Metamath Proof Explorer

Theorem bnj1000

Description: Technical lemma for bnj852 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1000.1 
|- ( ps <-> A. i e. _om ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj1000.2 
|- ( ps" <-> [. G / f ]. ps )
bnj1000.3 
|- G e. _V
bnj1000.15 
|- C = U_ y e. ( f ` m ) _pred ( y , A , R )
bnj1000.16 
|- G = ( f u. { <. n , C >. } )
Assertion bnj1000 
|- ( ps" <-> A. i e. _om ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) )

Proof

Step Hyp Ref Expression
1 bnj1000.1 
 |-  ( ps <-> A. i e. _om ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
2 bnj1000.2 
 |-  ( ps" <-> [. G / f ]. ps )
3 bnj1000.3 
 |-  G e. _V
4 bnj1000.15 
 |-  C = U_ y e. ( f ` m ) _pred ( y , A , R )
5 bnj1000.16 
 |-  G = ( f u. { <. n , C >. } )
6 df-ral 
 |-  ( A. i e. _om ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> A. i ( i e. _om -> ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) )
7 6 bicomi 
 |-  ( A. i ( i e. _om -> ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) <-> A. i e. _om ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
8 7 sbcbii 
 |-  ( [. G / f ]. A. i ( i e. _om -> ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) <-> [. G / f ]. A. i e. _om ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
9 nfv 
 |-  F/ f i e. _om
10 9 sbc19.21g 
 |-  ( G e. _V -> ( [. G / f ]. ( i e. _om -> ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) <-> ( i e. _om -> [. G / f ]. ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) )
11 3 10 ax-mp 
 |-  ( [. G / f ]. ( i e. _om -> ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) <-> ( i e. _om -> [. G / f ]. ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) )
12 nfv 
 |-  F/ f suc i e. N
13 12 sbc19.21g 
 |-  ( G e. _V -> ( [. G / f ]. ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> ( suc i e. N -> [. G / f ]. ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) )
14 3 13 ax-mp 
 |-  ( [. G / f ]. ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> ( suc i e. N -> [. G / f ]. ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
15 fveq1 
 |-  ( f = G -> ( f ` suc i ) = ( G ` suc i ) )
16 fveq1 
 |-  ( f = G -> ( f ` i ) = ( G ` i ) )
17 ax-5 
 |-  ( w e. ( f ` i ) -> A. y w e. ( f ` i ) )
18 nfcv 
 |-  F/_ y f
19 nfcv 
 |-  F/_ y n
20 nfiu1 
 |-  F/_ y U_ y e. ( f ` m ) _pred ( y , A , R )
21 4 20 nfcxfr 
 |-  F/_ y C
22 19 21 nfop 
 |-  F/_ y <. n , C >.
23 22 nfsn 
 |-  F/_ y { <. n , C >. }
24 18 23 nfun 
 |-  F/_ y ( f u. { <. n , C >. } )
25 5 24 nfcxfr 
 |-  F/_ y G
26 nfcv 
 |-  F/_ y i
27 25 26 nffv 
 |-  F/_ y ( G ` i )
28 27 nfcrii 
 |-  ( w e. ( G ` i ) -> A. y w e. ( G ` i ) )
29 17 28 bnj1316 
 |-  ( ( f ` i ) = ( G ` i ) -> U_ y e. ( f ` i ) _pred ( y , A , R ) = U_ y e. ( G ` i ) _pred ( y , A , R ) )
30 16 29 syl 
 |-  ( f = G -> U_ y e. ( f ` i ) _pred ( y , A , R ) = U_ y e. ( G ` i ) _pred ( y , A , R ) )
31 15 30 eqeq12d 
 |-  ( f = G -> ( ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) <-> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) )
32 fveq1 
 |-  ( f = e -> ( f ` suc i ) = ( e ` suc i ) )
33 fveq1 
 |-  ( f = e -> ( f ` i ) = ( e ` i ) )
34 ax-5 
 |-  ( ( f ` i ) = ( e ` i ) -> A. y ( f ` i ) = ( e ` i ) )
35 34 bnj956 
 |-  ( ( f ` i ) = ( e ` i ) -> U_ y e. ( f ` i ) _pred ( y , A , R ) = U_ y e. ( e ` i ) _pred ( y , A , R ) )
36 33 35 syl 
 |-  ( f = e -> U_ y e. ( f ` i ) _pred ( y , A , R ) = U_ y e. ( e ` i ) _pred ( y , A , R ) )
37 32 36 eqeq12d 
 |-  ( f = e -> ( ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) <-> ( e ` suc i ) = U_ y e. ( e ` i ) _pred ( y , A , R ) ) )
38 fveq1 
 |-  ( e = G -> ( e ` suc i ) = ( G ` suc i ) )
39 fveq1 
 |-  ( e = G -> ( e ` i ) = ( G ` i ) )
40 ax-5 
 |-  ( w e. ( e ` i ) -> A. y w e. ( e ` i ) )
41 40 28 bnj1316 
 |-  ( ( e ` i ) = ( G ` i ) -> U_ y e. ( e ` i ) _pred ( y , A , R ) = U_ y e. ( G ` i ) _pred ( y , A , R ) )
42 39 41 syl 
 |-  ( e = G -> U_ y e. ( e ` i ) _pred ( y , A , R ) = U_ y e. ( G ` i ) _pred ( y , A , R ) )
43 38 42 eqeq12d 
 |-  ( e = G -> ( ( e ` suc i ) = U_ y e. ( e ` i ) _pred ( y , A , R ) <-> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) )
44 3 31 37 43 bnj610 
 |-  ( [. G / f ]. ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) <-> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) )
45 44 imbi2i 
 |-  ( ( suc i e. N -> [. G / f ]. ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) )
46 14 45 bitri 
 |-  ( [. G / f ]. ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) )
47 46 imbi2i 
 |-  ( ( i e. _om -> [. G / f ]. ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) <-> ( i e. _om -> ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) )
48 11 47 bitri 
 |-  ( [. G / f ]. ( i e. _om -> ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) <-> ( i e. _om -> ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) )
49 48 albii 
 |-  ( A. i [. G / f ]. ( i e. _om -> ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) <-> A. i ( i e. _om -> ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) )
50 sbcal 
 |-  ( [. G / f ]. A. i ( i e. _om -> ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) <-> A. i [. G / f ]. ( i e. _om -> ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) )
51 df-ral 
 |-  ( A. i e. _om ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) <-> A. i ( i e. _om -> ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) )
52 49 50 51 3bitr4ri 
 |-  ( A. i e. _om ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) <-> [. G / f ]. A. i ( i e. _om -> ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) )
53 1 sbcbii 
 |-  ( [. G / f ]. ps <-> [. G / f ]. A. i e. _om ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
54 8 52 53 3bitr4ri 
 |-  ( [. G / f ]. ps <-> A. i e. _om ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) )
55 2 54 bitri 
 |-  ( ps" <-> A. i e. _om ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) )