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

Metamath Proof Explorer

Theorem bnj944

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

Proof

Step Hyp Ref Expression
1 bnj944.1 
 |-  ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
2 bnj944.2 
 |-  ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
3 bnj944.3 
 |-  ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
4 bnj944.4 
 |-  ( ph' <-> [. p / n ]. ph )
5 bnj944.7 
 |-  ( ph" <-> [. G / f ]. ph' )
6 bnj944.10 
 |-  D = ( _om \ { (/) } )
7 bnj944.12 
 |-  C = U_ y e. ( f ` m ) _pred ( y , A , R )
8 bnj944.13 
 |-  G = ( f u. { <. n , C >. } )
9 bnj944.14 
 |-  ( ta <-> ( f Fn n /\ ph /\ ps ) )
10 bnj944.15 
 |-  ( si <-> ( n e. D /\ p = suc n /\ m e. n ) )
11 simpl 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ( R _FrSe A /\ X e. A ) )
12 bnj667 
 |-  ( ( n e. D /\ f Fn n /\ ph /\ ps ) -> ( f Fn n /\ ph /\ ps ) )
13 3 12 sylbi 
 |-  ( ch -> ( f Fn n /\ ph /\ ps ) )
14 13 9 sylibr 
 |-  ( ch -> ta )
15 14 3ad2ant1 
 |-  ( ( ch /\ n = suc m /\ p = suc n ) -> ta )
16 15 adantl 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ta )
17 3 bnj1232 
 |-  ( ch -> n e. D )
18 vex 
 |-  m e. _V
19 18 bnj216 
 |-  ( n = suc m -> m e. n )
20 id 
 |-  ( p = suc n -> p = suc n )
21 17 19 20 3anim123i 
 |-  ( ( ch /\ n = suc m /\ p = suc n ) -> ( n e. D /\ m e. n /\ p = suc n ) )
22 3ancomb 
 |-  ( ( n e. D /\ p = suc n /\ m e. n ) <-> ( n e. D /\ m e. n /\ p = suc n ) )
23 10 22 bitri 
 |-  ( si <-> ( n e. D /\ m e. n /\ p = suc n ) )
24 21 23 sylibr 
 |-  ( ( ch /\ n = suc m /\ p = suc n ) -> si )
25 24 adantl 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> si )
26 bnj253 
 |-  ( ( R _FrSe A /\ X e. A /\ ta /\ si ) <-> ( ( R _FrSe A /\ X e. A ) /\ ta /\ si ) )
27 11 16 25 26 syl3anbrc 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ( R _FrSe A /\ X e. A /\ ta /\ si ) )
28 6 9 10 1 2 bnj938 
 |-  ( ( R _FrSe A /\ X e. A /\ ta /\ si ) -> U_ y e. ( f ` m ) _pred ( y , A , R ) e. _V )
29 7 28 eqeltrid 
 |-  ( ( R _FrSe A /\ X e. A /\ ta /\ si ) -> C e. _V )
30 27 29 syl 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> C e. _V )
31 bnj658 
 |-  ( ( n e. D /\ f Fn n /\ ph /\ ps ) -> ( n e. D /\ f Fn n /\ ph ) )
32 3 31 sylbi 
 |-  ( ch -> ( n e. D /\ f Fn n /\ ph ) )
33 32 3ad2ant1 
 |-  ( ( ch /\ n = suc m /\ p = suc n ) -> ( n e. D /\ f Fn n /\ ph ) )
34 simp3 
 |-  ( ( ch /\ n = suc m /\ p = suc n ) -> p = suc n )
35 bnj291 
 |-  ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) <-> ( ( n e. D /\ f Fn n /\ ph ) /\ p = suc n ) )
36 33 34 35 sylanbrc 
 |-  ( ( ch /\ n = suc m /\ p = suc n ) -> ( n e. D /\ p = suc n /\ f Fn n /\ ph ) )
37 36 adantl 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ( n e. D /\ p = suc n /\ f Fn n /\ ph ) )
38 opeq2 
 |-  ( C = if ( C e. _V , C , (/) ) -> <. n , C >. = <. n , if ( C e. _V , C , (/) ) >. )
39 38 sneqd 
 |-  ( C = if ( C e. _V , C , (/) ) -> { <. n , C >. } = { <. n , if ( C e. _V , C , (/) ) >. } )
40 39 uneq2d 
 |-  ( C = if ( C e. _V , C , (/) ) -> ( f u. { <. n , C >. } ) = ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) )
41 8 40 eqtrid 
 |-  ( C = if ( C e. _V , C , (/) ) -> G = ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) )
42 41 sbceq1d 
 |-  ( C = if ( C e. _V , C , (/) ) -> ( [. G / f ]. ph' <-> [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' ) )
43 5 42 bitrid 
 |-  ( C = if ( C e. _V , C , (/) ) -> ( ph" <-> [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' ) )
44 43 imbi2d 
 |-  ( C = if ( C e. _V , C , (/) ) -> ( ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> ph" ) <-> ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' ) ) )
45 biid 
 |-  ( [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' <-> [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' )
46 eqid 
 |-  ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) = ( f u. { <. n , if ( C e. _V , C , (/) ) >. } )
47 0ex 
 |-  (/) e. _V
48 47 elimel 
 |-  if ( C e. _V , C , (/) ) e. _V
49 1 4 45 6 46 48 bnj929 
 |-  ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' )
50 44 49 dedth 
 |-  ( C e. _V -> ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> ph" ) )
51 30 37 50 sylc 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ph" )