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

Metamath Proof Explorer

Theorem bnj151

Description: Technical lemma for bnj153 . 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 bnj151.1 
|- ( ph <-> ( f ` (/) ) = _pred ( x , A , R ) )
bnj151.2 
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj151.3 
|- D = ( _om \ { (/) } )
bnj151.4 
|- ( th <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ph /\ ps ) ) )
bnj151.5 
|- ( ta <-> A. m e. D ( m _E n -> [. m / n ]. th ) )
bnj151.6 
|- ( ze <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) )
bnj151.7 
|- ( ph' <-> [. 1o / n ]. ph )
bnj151.8 
|- ( ps' <-> [. 1o / n ]. ps )
bnj151.9 
|- ( th' <-> [. 1o / n ]. th )
bnj151.10 
|- ( th0 <-> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) ) )
bnj151.11 
|- ( th1 <-> ( ( R _FrSe A /\ x e. A ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) ) )
bnj151.12 
|- ( ze' <-> [. 1o / n ]. ze )
bnj151.13 
|- F = { <. (/) , _pred ( x , A , R ) >. }
bnj151.14 
|- ( ph" <-> [. F / f ]. ph' )
bnj151.15 
|- ( ps" <-> [. F / f ]. ps' )
bnj151.16 
|- ( ze" <-> [. F / f ]. ze' )
bnj151.17 
|- ( ze0 <-> ( f Fn 1o /\ ph' /\ ps' ) )
bnj151.18 
|- ( ze1 <-> [. g / f ]. ze0 )
bnj151.19 
|- ( ph1 <-> [. g / f ]. ph' )
bnj151.20 
|- ( ps1 <-> [. g / f ]. ps' )
Assertion bnj151 
|- ( n = 1o -> ( ( n e. D /\ ta ) -> th ) )

Proof

Step Hyp Ref Expression
1 bnj151.1 
 |-  ( ph <-> ( f ` (/) ) = _pred ( x , A , R ) )
2 bnj151.2 
 |-  ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
3 bnj151.3 
 |-  D = ( _om \ { (/) } )
4 bnj151.4 
 |-  ( th <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ph /\ ps ) ) )
5 bnj151.5 
 |-  ( ta <-> A. m e. D ( m _E n -> [. m / n ]. th ) )
6 bnj151.6 
 |-  ( ze <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) )
7 bnj151.7 
 |-  ( ph' <-> [. 1o / n ]. ph )
8 bnj151.8 
 |-  ( ps' <-> [. 1o / n ]. ps )
9 bnj151.9 
 |-  ( th' <-> [. 1o / n ]. th )
10 bnj151.10 
 |-  ( th0 <-> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) ) )
11 bnj151.11 
 |-  ( th1 <-> ( ( R _FrSe A /\ x e. A ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) ) )
12 bnj151.12 
 |-  ( ze' <-> [. 1o / n ]. ze )
13 bnj151.13 
 |-  F = { <. (/) , _pred ( x , A , R ) >. }
14 bnj151.14 
 |-  ( ph" <-> [. F / f ]. ph' )
15 bnj151.15 
 |-  ( ps" <-> [. F / f ]. ps' )
16 bnj151.16 
 |-  ( ze" <-> [. F / f ]. ze' )
17 bnj151.17 
 |-  ( ze0 <-> ( f Fn 1o /\ ph' /\ ps' ) )
18 bnj151.18 
 |-  ( ze1 <-> [. g / f ]. ze0 )
19 bnj151.19 
 |-  ( ph1 <-> [. g / f ]. ph' )
20 bnj151.20 
 |-  ( ps1 <-> [. g / f ]. ps' )
21 1 2 6 7 8 10 12 13 14 15 16 bnj150 
 |-  th0
22 21 10 mpbi 
 |-  ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) )
23 1 7 bnj118 
 |-  ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) )
24 11 17 18 19 20 23 bnj149 
 |-  th1
25 24 11 mpbi 
 |-  ( ( R _FrSe A /\ x e. A ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) )
26 df-eu 
 |-  ( E! f ( f Fn 1o /\ ph' /\ ps' ) <-> ( E. f ( f Fn 1o /\ ph' /\ ps' ) /\ E* f ( f Fn 1o /\ ph' /\ ps' ) ) )
27 22 25 26 sylanbrc 
 |-  ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn 1o /\ ph' /\ ps' ) )
28 4 7 8 9 bnj130 
 |-  ( th' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn 1o /\ ph' /\ ps' ) ) )
29 27 28 mpbir 
 |-  th'
30 sbceq1a 
 |-  ( n = 1o -> ( th <-> [. 1o / n ]. th ) )
31 30 9 bitr4di 
 |-  ( n = 1o -> ( th <-> th' ) )
32 29 31 mpbiri 
 |-  ( n = 1o -> th )
33 32 a1d 
 |-  ( n = 1o -> ( ( n e. D /\ ta ) -> th ) )