Metamath Proof Explorer

Theorem bnj938

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 bnj938.1 
|- D = ( _om \ { (/) } )
bnj938.2 
|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) )
bnj938.3 
|- ( si <-> ( m e. D /\ n = suc m /\ p e. m ) )
bnj938.4 
|- ( ph' <-> ( f ` (/) ) = _pred ( X , A , R ) )
bnj938.5 
|- ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
Assertion bnj938 
|- ( ( R _FrSe A /\ X e. A /\ ta /\ si ) -> U_ y e. ( f ` p ) _pred ( y , A , R ) e. _V )

Proof

Step Hyp Ref Expression
1 bnj938.1 
 |-  D = ( _om \ { (/) } )
2 bnj938.2 
 |-  ( ta <-> ( f Fn m /\ ph' /\ ps' ) )
3 bnj938.3 
 |-  ( si <-> ( m e. D /\ n = suc m /\ p e. m ) )
4 bnj938.4 
 |-  ( ph' <-> ( f ` (/) ) = _pred ( X , A , R ) )
5 bnj938.5 
 |-  ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
6 elisset 
 |-  ( X e. A -> E. x x = X )
7 6 bnj706 
 |-  ( ( R _FrSe A /\ X e. A /\ ta /\ si ) -> E. x x = X )
8 bnj291 
 |-  ( ( R _FrSe A /\ X e. A /\ ta /\ si ) <-> ( ( R _FrSe A /\ ta /\ si ) /\ X e. A ) )
9 8 simplbi 
 |-  ( ( R _FrSe A /\ X e. A /\ ta /\ si ) -> ( R _FrSe A /\ ta /\ si ) )
10 bnj602 
 |-  ( x = X -> _pred ( x , A , R ) = _pred ( X , A , R ) )
11 10 eqeq2d 
 |-  ( x = X -> ( ( f ` (/) ) = _pred ( x , A , R ) <-> ( f ` (/) ) = _pred ( X , A , R ) ) )
12 11 4 bitr4di 
 |-  ( x = X -> ( ( f ` (/) ) = _pred ( x , A , R ) <-> ph' ) )
13 12 3anbi2d 
 |-  ( x = X -> ( ( f Fn m /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps' ) <-> ( f Fn m /\ ph' /\ ps' ) ) )
14 13 2 bitr4di 
 |-  ( x = X -> ( ( f Fn m /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps' ) <-> ta ) )
15 14 3anbi2d 
 |-  ( x = X -> ( ( R _FrSe A /\ ( f Fn m /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps' ) /\ si ) <-> ( R _FrSe A /\ ta /\ si ) ) )
16 9 15 syl5ibr 
 |-  ( x = X -> ( ( R _FrSe A /\ X e. A /\ ta /\ si ) -> ( R _FrSe A /\ ( f Fn m /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps' ) /\ si ) ) )
17 biid 
 |-  ( ( f Fn m /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps' ) <-> ( f Fn m /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps' ) )
18 biid 
 |-  ( ( f ` (/) ) = _pred ( x , A , R ) <-> ( f ` (/) ) = _pred ( x , A , R ) )
19 1 17 3 18 5 bnj546 
 |-  ( ( R _FrSe A /\ ( f Fn m /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps' ) /\ si ) -> U_ y e. ( f ` p ) _pred ( y , A , R ) e. _V )
20 16 19 syl6 
 |-  ( x = X -> ( ( R _FrSe A /\ X e. A /\ ta /\ si ) -> U_ y e. ( f ` p ) _pred ( y , A , R ) e. _V ) )
21 20 exlimiv 
 |-  ( E. x x = X -> ( ( R _FrSe A /\ X e. A /\ ta /\ si ) -> U_ y e. ( f ` p ) _pred ( y , A , R ) e. _V ) )
22 7 21 mpcom 
 |-  ( ( R _FrSe A /\ X e. A /\ ta /\ si ) -> U_ y e. ( f ` p ) _pred ( y , A , R ) e. _V )