Metamath Proof Explorer

Theorem bnj929

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 bnj929.1 
|- ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
bnj929.4 
|- ( ph' <-> [. p / n ]. ph )
bnj929.7 
|- ( ph" <-> [. G / f ]. ph' )
bnj929.10 
|- D = ( _om \ { (/) } )
bnj929.13 
|- G = ( f u. { <. n , C >. } )
bnj929.50 
|- C e. _V
Assertion bnj929 
|- ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> ph" )

Proof

Step Hyp Ref Expression
1 bnj929.1 
 |-  ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
2 bnj929.4 
 |-  ( ph' <-> [. p / n ]. ph )
3 bnj929.7 
 |-  ( ph" <-> [. G / f ]. ph' )
4 bnj929.10 
 |-  D = ( _om \ { (/) } )
5 bnj929.13 
 |-  G = ( f u. { <. n , C >. } )
6 bnj929.50 
 |-  C e. _V
7 bnj645 
 |-  ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> ph )
8 bnj334 
 |-  ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) <-> ( f Fn n /\ n e. D /\ p = suc n /\ ph ) )
9 bnj257 
 |-  ( ( f Fn n /\ n e. D /\ p = suc n /\ ph ) <-> ( f Fn n /\ n e. D /\ ph /\ p = suc n ) )
10 8 9 bitri 
 |-  ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) <-> ( f Fn n /\ n e. D /\ ph /\ p = suc n ) )
11 bnj345 
 |-  ( ( f Fn n /\ n e. D /\ ph /\ p = suc n ) <-> ( p = suc n /\ f Fn n /\ n e. D /\ ph ) )
12 bnj253 
 |-  ( ( p = suc n /\ f Fn n /\ n e. D /\ ph ) <-> ( ( p = suc n /\ f Fn n ) /\ n e. D /\ ph ) )
13 10 11 12 3bitri 
 |-  ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) <-> ( ( p = suc n /\ f Fn n ) /\ n e. D /\ ph ) )
14 13 simp1bi 
 |-  ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> ( p = suc n /\ f Fn n ) )
15 5 6 bnj927 
 |-  ( ( p = suc n /\ f Fn n ) -> G Fn p )
16 15 fnfund 
 |-  ( ( p = suc n /\ f Fn n ) -> Fun G )
17 14 16 syl 
 |-  ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> Fun G )
18 5 bnj931 
 |-  f C_ G
19 18 a1i 
 |-  ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> f C_ G )
20 bnj268 
 |-  ( ( n e. D /\ f Fn n /\ p = suc n /\ ph ) <-> ( n e. D /\ p = suc n /\ f Fn n /\ ph ) )
21 bnj253 
 |-  ( ( n e. D /\ f Fn n /\ p = suc n /\ ph ) <-> ( ( n e. D /\ f Fn n ) /\ p = suc n /\ ph ) )
22 20 21 bitr3i 
 |-  ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) <-> ( ( n e. D /\ f Fn n ) /\ p = suc n /\ ph ) )
23 22 simp1bi 
 |-  ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> ( n e. D /\ f Fn n ) )
24 fndm 
 |-  ( f Fn n -> dom f = n )
25 4 bnj529 
 |-  ( n e. D -> (/) e. n )
26 eleq2 
 |-  ( dom f = n -> ( (/) e. dom f <-> (/) e. n ) )
27 26 biimpar 
 |-  ( ( dom f = n /\ (/) e. n ) -> (/) e. dom f )
28 24 25 27 syl2anr 
 |-  ( ( n e. D /\ f Fn n ) -> (/) e. dom f )
29 23 28 syl 
 |-  ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> (/) e. dom f )
30 17 19 29 bnj1502 
 |-  ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> ( G ` (/) ) = ( f ` (/) ) )
31 5 bnj918 
 |-  G e. _V
32 1 2 3 31 bnj934 
 |-  ( ( ph /\ ( G ` (/) ) = ( f ` (/) ) ) -> ph" )
33 7 30 32 syl2anc 
 |-  ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> ph" )