Metamath Proof Explorer

Theorem bnj546

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

Proof

Step Hyp Ref Expression
1 bnj546.1 
 |-  D = ( _om \ { (/) } )
2 bnj546.2 
 |-  ( ta <-> ( f Fn m /\ ph' /\ ps' ) )
3 bnj546.3 
 |-  ( si <-> ( m e. D /\ n = suc m /\ p e. m ) )
4 bnj546.4 
 |-  ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) )
5 bnj546.5 
 |-  ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
6 3simpc 
 |-  ( ( f Fn m /\ ph' /\ ps' ) -> ( ph' /\ ps' ) )
7 2 6 sylbi 
 |-  ( ta -> ( ph' /\ ps' ) )
8 1 bnj923 
 |-  ( m e. D -> m e. _om )
9 8 3ad2ant1 
 |-  ( ( m e. D /\ n = suc m /\ p e. m ) -> m e. _om )
10 simp3 
 |-  ( ( m e. D /\ n = suc m /\ p e. m ) -> p e. m )
11 9 10 jca 
 |-  ( ( m e. D /\ n = suc m /\ p e. m ) -> ( m e. _om /\ p e. m ) )
12 3 11 sylbi 
 |-  ( si -> ( m e. _om /\ p e. m ) )
13 7 12 anim12i 
 |-  ( ( ta /\ si ) -> ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) ) )
14 bnj256 
 |-  ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) <-> ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) ) )
15 13 14 sylibr 
 |-  ( ( ta /\ si ) -> ( ph' /\ ps' /\ m e. _om /\ p e. m ) )
16 15 anim2i 
 |-  ( ( R _FrSe A /\ ( ta /\ si ) ) -> ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) )
17 16 3impb 
 |-  ( ( R _FrSe A /\ ta /\ si ) -> ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) )
18 biid 
 |-  ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) <-> ( ph' /\ ps' /\ m e. _om /\ p e. m ) )
19 4 5 18 bnj518 
 |-  ( ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) -> A. y e. ( f ` p ) _pred ( y , A , R ) e. _V )
20 fvex 
 |-  ( f ` p ) e. _V
21 iunexg 
 |-  ( ( ( f ` p ) e. _V /\ A. y e. ( f ` p ) _pred ( y , A , R ) e. _V ) -> U_ y e. ( f ` p ) _pred ( y , A , R ) e. _V )
22 20 21 mpan 
 |-  ( A. y e. ( f ` p ) _pred ( y , A , R ) e. _V -> U_ y e. ( f ` p ) _pred ( y , A , R ) e. _V )
23 17 19 22 3syl 
 |-  ( ( R _FrSe A /\ ta /\ si ) -> U_ y e. ( f ` p ) _pred ( y , A , R ) e. _V )