Metamath Proof Explorer

Theorem bnj969

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

Proof

Step Hyp Ref Expression
1 bnj969.1 
 |-  ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
2 bnj969.2 
 |-  ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
3 bnj969.3 
 |-  ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
4 bnj969.10 
 |-  D = ( _om \ { (/) } )
5 bnj969.12 
 |-  C = U_ y e. ( f ` m ) _pred ( y , A , R )
6 bnj969.14 
 |-  ( ta <-> ( f Fn n /\ ph /\ ps ) )
7 bnj969.15 
 |-  ( si <-> ( n e. D /\ p = suc n /\ m e. n ) )
8 simpl 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ( R _FrSe A /\ X e. A ) )
9 bnj667 
 |-  ( ( n e. D /\ f Fn n /\ ph /\ ps ) -> ( f Fn n /\ ph /\ ps ) )
10 9 3 6 3imtr4i 
 |-  ( ch -> ta )
11 10 3ad2ant1 
 |-  ( ( ch /\ n = suc m /\ p = suc n ) -> ta )
12 11 adantl 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ta )
13 3 bnj1232 
 |-  ( ch -> n e. D )
14 vex 
 |-  m e. _V
15 14 bnj216 
 |-  ( n = suc m -> m e. n )
16 id 
 |-  ( p = suc n -> p = suc n )
17 13 15 16 3anim123i 
 |-  ( ( ch /\ n = suc m /\ p = suc n ) -> ( n e. D /\ m e. n /\ p = suc n ) )
18 3ancomb 
 |-  ( ( n e. D /\ p = suc n /\ m e. n ) <-> ( n e. D /\ m e. n /\ p = suc n ) )
19 7 18 bitri 
 |-  ( si <-> ( n e. D /\ m e. n /\ p = suc n ) )
20 17 19 sylibr 
 |-  ( ( ch /\ n = suc m /\ p = suc n ) -> si )
21 20 adantl 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> si )
22 8 12 21 jca32 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ( ( R _FrSe A /\ X e. A ) /\ ( ta /\ si ) ) )
23 bnj256 
 |-  ( ( R _FrSe A /\ X e. A /\ ta /\ si ) <-> ( ( R _FrSe A /\ X e. A ) /\ ( ta /\ si ) ) )
24 22 23 sylibr 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ( R _FrSe A /\ X e. A /\ ta /\ si ) )
25 4 6 7 1 2 bnj938 
 |-  ( ( R _FrSe A /\ X e. A /\ ta /\ si ) -> U_ y e. ( f ` m ) _pred ( y , A , R ) e. _V )
26 5 25 eqeltrid 
 |-  ( ( R _FrSe A /\ X e. A /\ ta /\ si ) -> C e. _V )
27 24 26 syl 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> C e. _V )