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

Metamath Proof Explorer

Theorem bnj553

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 bnj553.1 
|- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) )
bnj553.2 
|- ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj553.3 
|- D = ( _om \ { (/) } )
bnj553.4 
|- G = ( f u. { <. m , U_ y e. ( f ` p ) _pred ( y , A , R ) >. } )
bnj553.5 
|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) )
bnj553.6 
|- ( si <-> ( m e. D /\ n = suc m /\ p e. m ) )
bnj553.7 
|- C = U_ y e. ( f ` p ) _pred ( y , A , R )
bnj553.8 
|- G = ( f u. { <. m , C >. } )
bnj553.9 
|- B = U_ y e. ( f ` i ) _pred ( y , A , R )
bnj553.10 
|- K = U_ y e. ( G ` i ) _pred ( y , A , R )
bnj553.11 
|- L = U_ y e. ( G ` p ) _pred ( y , A , R )
bnj553.12 
|- ( ( R _FrSe A /\ ta /\ si ) -> G Fn n )
Assertion bnj553 
|- ( ( ( R _FrSe A /\ ta /\ si ) /\ i e. m /\ p = i ) -> ( G ` m ) = L )

Proof

Step Hyp Ref Expression
1 bnj553.1 
 |-  ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) )
2 bnj553.2 
 |-  ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
3 bnj553.3 
 |-  D = ( _om \ { (/) } )
4 bnj553.4 
 |-  G = ( f u. { <. m , U_ y e. ( f ` p ) _pred ( y , A , R ) >. } )
5 bnj553.5 
 |-  ( ta <-> ( f Fn m /\ ph' /\ ps' ) )
6 bnj553.6 
 |-  ( si <-> ( m e. D /\ n = suc m /\ p e. m ) )
7 bnj553.7 
 |-  C = U_ y e. ( f ` p ) _pred ( y , A , R )
8 bnj553.8 
 |-  G = ( f u. { <. m , C >. } )
9 bnj553.9 
 |-  B = U_ y e. ( f ` i ) _pred ( y , A , R )
10 bnj553.10 
 |-  K = U_ y e. ( G ` i ) _pred ( y , A , R )
11 bnj553.11 
 |-  L = U_ y e. ( G ` p ) _pred ( y , A , R )
12 bnj553.12 
 |-  ( ( R _FrSe A /\ ta /\ si ) -> G Fn n )
13 12 fnfund 
 |-  ( ( R _FrSe A /\ ta /\ si ) -> Fun G )
14 opex 
 |-  <. m , C >. e. _V
15 14 snid 
 |-  <. m , C >. e. { <. m , C >. }
16 elun2 
 |-  ( <. m , C >. e. { <. m , C >. } -> <. m , C >. e. ( f u. { <. m , C >. } ) )
17 15 16 ax-mp 
 |-  <. m , C >. e. ( f u. { <. m , C >. } )
18 17 8 eleqtrri 
 |-  <. m , C >. e. G
19 funopfv 
 |-  ( Fun G -> ( <. m , C >. e. G -> ( G ` m ) = C ) )
20 13 18 19 mpisyl 
 |-  ( ( R _FrSe A /\ ta /\ si ) -> ( G ` m ) = C )
21 20 3ad2ant1 
 |-  ( ( ( R _FrSe A /\ ta /\ si ) /\ i e. m /\ p = i ) -> ( G ` m ) = C )
22 fveq2 
 |-  ( p = i -> ( G ` p ) = ( G ` i ) )
23 22 bnj1113 
 |-  ( p = i -> U_ y e. ( G ` p ) _pred ( y , A , R ) = U_ y e. ( G ` i ) _pred ( y , A , R ) )
24 23 11 10 3eqtr4g 
 |-  ( p = i -> L = K )
25 24 3ad2ant3 
 |-  ( ( ( R _FrSe A /\ ta /\ si ) /\ i e. m /\ p = i ) -> L = K )
26 5 9 10 4 12 bnj548 
 |-  ( ( ( R _FrSe A /\ ta /\ si ) /\ i e. m ) -> B = K )
27 26 3adant3 
 |-  ( ( ( R _FrSe A /\ ta /\ si ) /\ i e. m /\ p = i ) -> B = K )
28 fveq2 
 |-  ( p = i -> ( f ` p ) = ( f ` i ) )
29 28 bnj1113 
 |-  ( p = i -> U_ y e. ( f ` p ) _pred ( y , A , R ) = U_ y e. ( f ` i ) _pred ( y , A , R ) )
30 9 7 eqeq12i 
 |-  ( B = C <-> U_ y e. ( f ` i ) _pred ( y , A , R ) = U_ y e. ( f ` p ) _pred ( y , A , R ) )
31 eqcom 
 |-  ( U_ y e. ( f ` i ) _pred ( y , A , R ) = U_ y e. ( f ` p ) _pred ( y , A , R ) <-> U_ y e. ( f ` p ) _pred ( y , A , R ) = U_ y e. ( f ` i ) _pred ( y , A , R ) )
32 30 31 bitri 
 |-  ( B = C <-> U_ y e. ( f ` p ) _pred ( y , A , R ) = U_ y e. ( f ` i ) _pred ( y , A , R ) )
33 29 32 sylibr 
 |-  ( p = i -> B = C )
34 33 3ad2ant3 
 |-  ( ( ( R _FrSe A /\ ta /\ si ) /\ i e. m /\ p = i ) -> B = C )
35 25 27 34 3eqtr2rd 
 |-  ( ( ( R _FrSe A /\ ta /\ si ) /\ i e. m /\ p = i ) -> C = L )
36 21 35 eqtrd 
 |-  ( ( ( R _FrSe A /\ ta /\ si ) /\ i e. m /\ p = i ) -> ( G ` m ) = L )