Metamath Proof Explorer

Theorem bnj580

Description: Technical lemma for bnj579 . 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 bnj580.1 
|- ( ph <-> ( f ` (/) ) = _pred ( x , A , R ) )
bnj580.2 
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj580.3 
|- ( ch <-> ( f Fn n /\ ph /\ ps ) )
bnj580.4 
|- ( ph' <-> [. g / f ]. ph )
bnj580.5 
|- ( ps' <-> [. g / f ]. ps )
bnj580.6 
|- ( ch' <-> [. g / f ]. ch )
bnj580.7 
|- D = ( _om \ { (/) } )
bnj580.8 
|- ( th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) )
bnj580.9 
|- ( ta <-> A. k e. n ( k _E j -> [. k / j ]. th ) )
Assertion bnj580 
|- ( n e. D -> E* f ch )

Proof

Step Hyp Ref Expression
1 bnj580.1 
 |-  ( ph <-> ( f ` (/) ) = _pred ( x , A , R ) )
2 bnj580.2 
 |-  ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
3 bnj580.3 
 |-  ( ch <-> ( f Fn n /\ ph /\ ps ) )
4 bnj580.4 
 |-  ( ph' <-> [. g / f ]. ph )
5 bnj580.5 
 |-  ( ps' <-> [. g / f ]. ps )
6 bnj580.6 
 |-  ( ch' <-> [. g / f ]. ch )
7 bnj580.7 
 |-  D = ( _om \ { (/) } )
8 bnj580.8 
 |-  ( th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) )
9 bnj580.9 
 |-  ( ta <-> A. k e. n ( k _E j -> [. k / j ]. th ) )
10 3 simp1bi 
 |-  ( ch -> f Fn n )
11 3 4 5 6 bnj581 
 |-  ( ch' <-> ( g Fn n /\ ph' /\ ps' ) )
12 11 simp1bi 
 |-  ( ch' -> g Fn n )
13 10 12 bnj240 
 |-  ( ( n e. D /\ ch /\ ch' ) -> ( f Fn n /\ g Fn n ) )
14 4 1 bnj154 
 |-  ( ph' <-> ( g ` (/) ) = _pred ( x , A , R ) )
15 vex 
 |-  g e. _V
16 2 5 15 bnj540 
 |-  ( ps' <-> A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) )
17 8 bnj591 
 |-  ( [. k / j ]. th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) )
18 1 2 3 7 14 16 11 8 17 9 bnj594 
 |-  ( ( j e. n /\ ta ) -> th )
19 18 ex 
 |-  ( j e. n -> ( ta -> th ) )
20 19 rgen 
 |-  A. j e. n ( ta -> th )
21 vex 
 |-  n e. _V
22 21 9 bnj110 
 |-  ( ( _E Fr n /\ A. j e. n ( ta -> th ) ) -> A. j e. n th )
23 20 22 mpan2 
 |-  ( _E Fr n -> A. j e. n th )
24 8 ralbii 
 |-  ( A. j e. n th <-> A. j e. n ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) )
25 23 24 sylib 
 |-  ( _E Fr n -> A. j e. n ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) )
26 25 r19.21be 
 |-  A. j e. n ( _E Fr n -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) )
27 7 bnj923 
 |-  ( n e. D -> n e. _om )
28 nnord 
 |-  ( n e. _om -> Ord n )
29 ordfr 
 |-  ( Ord n -> _E Fr n )
30 27 28 29 3syl 
 |-  ( n e. D -> _E Fr n )
31 30 3ad2ant1 
 |-  ( ( n e. D /\ ch /\ ch' ) -> _E Fr n )
32 31 pm4.71ri 
 |-  ( ( n e. D /\ ch /\ ch' ) <-> ( _E Fr n /\ ( n e. D /\ ch /\ ch' ) ) )
33 32 imbi1i 
 |-  ( ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> ( ( _E Fr n /\ ( n e. D /\ ch /\ ch' ) ) -> ( f ` j ) = ( g ` j ) ) )
34 impexp 
 |-  ( ( ( _E Fr n /\ ( n e. D /\ ch /\ ch' ) ) -> ( f ` j ) = ( g ` j ) ) <-> ( _E Fr n -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) )
35 33 34 bitri 
 |-  ( ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> ( _E Fr n -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) )
36 35 ralbii 
 |-  ( A. j e. n ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> A. j e. n ( _E Fr n -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) )
37 26 36 mpbir 
 |-  A. j e. n ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) )
38 r19.21v 
 |-  ( A. j e. n ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> ( ( n e. D /\ ch /\ ch' ) -> A. j e. n ( f ` j ) = ( g ` j ) ) )
39 37 38 mpbi 
 |-  ( ( n e. D /\ ch /\ ch' ) -> A. j e. n ( f ` j ) = ( g ` j ) )
40 eqfnfv 
 |-  ( ( f Fn n /\ g Fn n ) -> ( f = g <-> A. j e. n ( f ` j ) = ( g ` j ) ) )
41 40 biimprd 
 |-  ( ( f Fn n /\ g Fn n ) -> ( A. j e. n ( f ` j ) = ( g ` j ) -> f = g ) )
42 13 39 41 sylc 
 |-  ( ( n e. D /\ ch /\ ch' ) -> f = g )
43 42 3expib 
 |-  ( n e. D -> ( ( ch /\ ch' ) -> f = g ) )
44 43 alrimivv 
 |-  ( n e. D -> A. f A. g ( ( ch /\ ch' ) -> f = g ) )
45 sbsbc 
 |-  ( [ g / f ] ch <-> [. g / f ]. ch )
46 45 anbi2i 
 |-  ( ( ch /\ [ g / f ] ch ) <-> ( ch /\ [. g / f ]. ch ) )
47 46 imbi1i 
 |-  ( ( ( ch /\ [ g / f ] ch ) -> f = g ) <-> ( ( ch /\ [. g / f ]. ch ) -> f = g ) )
48 47 2albii 
 |-  ( A. f A. g ( ( ch /\ [ g / f ] ch ) -> f = g ) <-> A. f A. g ( ( ch /\ [. g / f ]. ch ) -> f = g ) )
49 nfv 
 |-  F/ g ch
50 49 mo3 
 |-  ( E* f ch <-> A. f A. g ( ( ch /\ [ g / f ] ch ) -> f = g ) )
51 6 anbi2i 
 |-  ( ( ch /\ ch' ) <-> ( ch /\ [. g / f ]. ch ) )
52 51 imbi1i 
 |-  ( ( ( ch /\ ch' ) -> f = g ) <-> ( ( ch /\ [. g / f ]. ch ) -> f = g ) )
53 52 2albii 
 |-  ( A. f A. g ( ( ch /\ ch' ) -> f = g ) <-> A. f A. g ( ( ch /\ [. g / f ]. ch ) -> f = g ) )
54 48 50 53 3bitr4i 
 |-  ( E* f ch <-> A. f A. g ( ( ch /\ ch' ) -> f = g ) )
55 44 54 sylibr 
 |-  ( n e. D -> E* f ch )