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 syl5eq
 |-  ( 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 syl5bb
 |-  ( 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" )