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 ) )