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 )