Metamath Proof Explorer

Theorem bnj557

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

Proof

Step Hyp Ref Expression
1 bnj557.3 
 |-  D = ( _om \ { (/) } )
2 bnj557.16 
 |-  G = ( f u. { <. m , U_ y e. ( f ` p ) _pred ( y , A , R ) >. } )
3 bnj557.17 
 |-  ( ta <-> ( f Fn m /\ ph' /\ ps' ) )
4 bnj557.18 
 |-  ( si <-> ( m e. D /\ n = suc m /\ p e. m ) )
5 bnj557.19 
 |-  ( et <-> ( m e. D /\ n = suc m /\ p e. _om /\ m = suc p ) )
6 bnj557.20 
 |-  ( ze <-> ( i e. _om /\ suc i e. n /\ m = suc i ) )
7 bnj557.21 
 |-  B = U_ y e. ( f ` i ) _pred ( y , A , R )
8 bnj557.22 
 |-  C = U_ y e. ( f ` p ) _pred ( y , A , R )
9 bnj557.23 
 |-  K = U_ y e. ( G ` i ) _pred ( y , A , R )
10 bnj557.24 
 |-  L = U_ y e. ( G ` p ) _pred ( y , A , R )
11 bnj557.25 
 |-  G = ( f u. { <. m , C >. } )
12 bnj557.28 
 |-  ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) )
13 bnj557.29 
 |-  ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
14 bnj557.36 
 |-  ( ( R _FrSe A /\ ta /\ si ) -> G Fn n )
15 3an4anass 
 |-  ( ( ( R _FrSe A /\ ta /\ et ) /\ ze ) <-> ( ( R _FrSe A /\ ta ) /\ ( et /\ ze ) ) )
16 4 5 bnj556 
 |-  ( et -> si )
17 16 3anim3i 
 |-  ( ( R _FrSe A /\ ta /\ et ) -> ( R _FrSe A /\ ta /\ si ) )
18 vex 
 |-  i e. _V
19 18 bnj216 
 |-  ( m = suc i -> i e. m )
20 6 19 bnj837 
 |-  ( ze -> i e. m )
21 17 20 anim12i 
 |-  ( ( ( R _FrSe A /\ ta /\ et ) /\ ze ) -> ( ( R _FrSe A /\ ta /\ si ) /\ i e. m ) )
22 15 21 sylbir 
 |-  ( ( ( R _FrSe A /\ ta ) /\ ( et /\ ze ) ) -> ( ( R _FrSe A /\ ta /\ si ) /\ i e. m ) )
23 5 bnj1254 
 |-  ( et -> m = suc p )
24 6 simp3bi 
 |-  ( ze -> m = suc i )
25 bnj551 
 |-  ( ( m = suc p /\ m = suc i ) -> p = i )
26 23 24 25 syl2an 
 |-  ( ( et /\ ze ) -> p = i )
27 26 adantl 
 |-  ( ( ( R _FrSe A /\ ta ) /\ ( et /\ ze ) ) -> p = i )
28 22 27 jca 
 |-  ( ( ( R _FrSe A /\ ta ) /\ ( et /\ ze ) ) -> ( ( ( R _FrSe A /\ ta /\ si ) /\ i e. m ) /\ p = i ) )
29 bnj256 
 |-  ( ( R _FrSe A /\ ta /\ et /\ ze ) <-> ( ( R _FrSe A /\ ta ) /\ ( et /\ ze ) ) )
30 df-3an 
 |-  ( ( ( R _FrSe A /\ ta /\ si ) /\ i e. m /\ p = i ) <-> ( ( ( R _FrSe A /\ ta /\ si ) /\ i e. m ) /\ p = i ) )
31 28 29 30 3imtr4i 
 |-  ( ( R _FrSe A /\ ta /\ et /\ ze ) -> ( ( R _FrSe A /\ ta /\ si ) /\ i e. m /\ p = i ) )
32 12 13 1 2 3 4 8 11 7 9 10 14 bnj553 
 |-  ( ( ( R _FrSe A /\ ta /\ si ) /\ i e. m /\ p = i ) -> ( G ` m ) = L )
33 31 32 syl 
 |-  ( ( R _FrSe A /\ ta /\ et /\ ze ) -> ( G ` m ) = L )