Metamath Proof Explorer

Theorem bnj999

Description: Technical lemma for bnj69 . 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 bnj999.1 
|- ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
bnj999.2 
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj999.3 
|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
bnj999.7 
|- ( ph' <-> [. p / n ]. ph )
bnj999.8 
|- ( ps' <-> [. p / n ]. ps )
bnj999.9 
|- ( ch' <-> [. p / n ]. ch )
bnj999.10 
|- ( ph" <-> [. G / f ]. ph' )
bnj999.11 
|- ( ps" <-> [. G / f ]. ps' )
bnj999.12 
|- ( ch" <-> [. G / f ]. ch' )
bnj999.15 
|- C = U_ y e. ( f ` m ) _pred ( y , A , R )
bnj999.16 
|- G = ( f u. { <. n , C >. } )
Assertion bnj999 
|- ( ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> _pred ( y , A , R ) C_ ( G ` suc i ) )

Proof

Step Hyp Ref Expression
1 bnj999.1 
 |-  ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
2 bnj999.2 
 |-  ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
3 bnj999.3 
 |-  ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
4 bnj999.7 
 |-  ( ph' <-> [. p / n ]. ph )
5 bnj999.8 
 |-  ( ps' <-> [. p / n ]. ps )
6 bnj999.9 
 |-  ( ch' <-> [. p / n ]. ch )
7 bnj999.10 
 |-  ( ph" <-> [. G / f ]. ph' )
8 bnj999.11 
 |-  ( ps" <-> [. G / f ]. ps' )
9 bnj999.12 
 |-  ( ch" <-> [. G / f ]. ch' )
10 bnj999.15 
 |-  C = U_ y e. ( f ` m ) _pred ( y , A , R )
11 bnj999.16 
 |-  G = ( f u. { <. n , C >. } )
12 vex 
 |-  p e. _V
13 3 4 5 6 12 bnj919 
 |-  ( ch' <-> ( p e. D /\ f Fn p /\ ph' /\ ps' ) )
14 11 bnj918 
 |-  G e. _V
15 13 7 8 9 14 bnj976 
 |-  ( ch" <-> ( p e. D /\ G Fn p /\ ph" /\ ps" ) )
16 15 bnj1254 
 |-  ( ch" -> ps" )
17 16 anim1i 
 |-  ( ( ch" /\ ( i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) -> ( ps" /\ ( i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) )
18 bnj252 
 |-  ( ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) <-> ( ch" /\ ( i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) )
19 bnj252 
 |-  ( ( ps" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) <-> ( ps" /\ ( i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) )
20 17 18 19 3imtr4i 
 |-  ( ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> ( ps" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) )
21 ssiun2 
 |-  ( y e. ( G ` i ) -> _pred ( y , A , R ) C_ U_ y e. ( G ` i ) _pred ( y , A , R ) )
22 21 bnj708 
 |-  ( ( ps" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> _pred ( y , A , R ) C_ U_ y e. ( G ` i ) _pred ( y , A , R ) )
23 3simpa 
 |-  ( ( ps" /\ i e. _om /\ suc i e. p ) -> ( ps" /\ i e. _om ) )
24 23 ancomd 
 |-  ( ( ps" /\ i e. _om /\ suc i e. p ) -> ( i e. _om /\ ps" ) )
25 simp3 
 |-  ( ( ps" /\ i e. _om /\ suc i e. p ) -> suc i e. p )
26 2 5 12 bnj539 
 |-  ( ps' <-> A. i e. _om ( suc i e. p -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
27 26 8 10 11 bnj965 
 |-  ( ps" <-> A. i e. _om ( suc i e. p -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) )
28 27 bnj228 
 |-  ( ( i e. _om /\ ps" ) -> ( suc i e. p -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) )
29 24 25 28 sylc 
 |-  ( ( ps" /\ i e. _om /\ suc i e. p ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) )
30 29 bnj721 
 |-  ( ( ps" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) )
31 22 30 sseqtrrd 
 |-  ( ( ps" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> _pred ( y , A , R ) C_ ( G ` suc i ) )
32 20 31 syl 
 |-  ( ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> _pred ( y , A , R ) C_ ( G ` suc i ) )