Metamath Proof Explorer

Theorem bnj558

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 bnj558.3 
|- D = ( _om \ { (/) } )
bnj558.16 
|- G = ( f u. { <. m , U_ y e. ( f ` p ) _pred ( y , A , R ) >. } )
bnj558.17 
|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) )
bnj558.18 
|- ( si <-> ( m e. D /\ n = suc m /\ p e. m ) )
bnj558.19 
|- ( et <-> ( m e. D /\ n = suc m /\ p e. _om /\ m = suc p ) )
bnj558.20 
|- ( ze <-> ( i e. _om /\ suc i e. n /\ m = suc i ) )
bnj558.21 
|- B = U_ y e. ( f ` i ) _pred ( y , A , R )
bnj558.22 
|- C = U_ y e. ( f ` p ) _pred ( y , A , R )
bnj558.23 
|- K = U_ y e. ( G ` i ) _pred ( y , A , R )
bnj558.24 
|- L = U_ y e. ( G ` p ) _pred ( y , A , R )
bnj558.25 
|- G = ( f u. { <. m , C >. } )
bnj558.28 
|- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) )
bnj558.29 
|- ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj558.36 
|- ( ( R _FrSe A /\ ta /\ si ) -> G Fn n )
Assertion bnj558 
|- ( ( R _FrSe A /\ ta /\ et /\ ze ) -> ( G ` suc i ) = K )

Proof

Step Hyp Ref Expression
1 bnj558.3 
 |-  D = ( _om \ { (/) } )
2 bnj558.16 
 |-  G = ( f u. { <. m , U_ y e. ( f ` p ) _pred ( y , A , R ) >. } )
3 bnj558.17 
 |-  ( ta <-> ( f Fn m /\ ph' /\ ps' ) )
4 bnj558.18 
 |-  ( si <-> ( m e. D /\ n = suc m /\ p e. m ) )
5 bnj558.19 
 |-  ( et <-> ( m e. D /\ n = suc m /\ p e. _om /\ m = suc p ) )
6 bnj558.20 
 |-  ( ze <-> ( i e. _om /\ suc i e. n /\ m = suc i ) )
7 bnj558.21 
 |-  B = U_ y e. ( f ` i ) _pred ( y , A , R )
8 bnj558.22 
 |-  C = U_ y e. ( f ` p ) _pred ( y , A , R )
9 bnj558.23 
 |-  K = U_ y e. ( G ` i ) _pred ( y , A , R )
10 bnj558.24 
 |-  L = U_ y e. ( G ` p ) _pred ( y , A , R )
11 bnj558.25 
 |-  G = ( f u. { <. m , C >. } )
12 bnj558.28 
 |-  ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) )
13 bnj558.29 
 |-  ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
14 bnj558.36 
 |-  ( ( R _FrSe A /\ ta /\ si ) -> G Fn n )
15 1 2 3 4 5 6 7 8 9 10 11 12 13 14 bnj557 
 |-  ( ( R _FrSe A /\ ta /\ et /\ ze ) -> ( G ` m ) = L )
16 bnj422 
 |-  ( ( R _FrSe A /\ ta /\ et /\ ze ) <-> ( et /\ ze /\ R _FrSe A /\ ta ) )
17 bnj253 
 |-  ( ( et /\ ze /\ R _FrSe A /\ ta ) <-> ( ( et /\ ze ) /\ R _FrSe A /\ ta ) )
18 16 17 bitri 
 |-  ( ( R _FrSe A /\ ta /\ et /\ ze ) <-> ( ( et /\ ze ) /\ R _FrSe A /\ ta ) )
19 18 simp1bi 
 |-  ( ( R _FrSe A /\ ta /\ et /\ ze ) -> ( et /\ ze ) )
20 5 6 9 10 9 10 bnj554 
 |-  ( ( et /\ ze ) -> ( ( G ` m ) = L <-> ( G ` suc i ) = K ) )
21 19 20 syl 
 |-  ( ( R _FrSe A /\ ta /\ et /\ ze ) -> ( ( G ` m ) = L <-> ( G ` suc i ) = K ) )
22 15 21 mpbid 
 |-  ( ( R _FrSe A /\ ta /\ et /\ ze ) -> ( G ` suc i ) = K )