Metamath Proof Explorer

Theorem bnj150

Description: Technical lemma for bnj151 . 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 bnj150.1 
|- ( ph <-> ( f ` (/) ) = _pred ( x , A , R ) )
bnj150.2 
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj150.3 
|- ( ze <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) )
bnj150.4 
|- ( ph' <-> [. 1o / n ]. ph )
bnj150.5 
|- ( ps' <-> [. 1o / n ]. ps )
bnj150.6 
|- ( th0 <-> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) ) )
bnj150.7 
|- ( ze' <-> [. 1o / n ]. ze )
bnj150.8 
|- F = { <. (/) , _pred ( x , A , R ) >. }
bnj150.9 
|- ( ph" <-> [. F / f ]. ph' )
bnj150.10 
|- ( ps" <-> [. F / f ]. ps' )
bnj150.11 
|- ( ze" <-> [. F / f ]. ze' )
Assertion bnj150 
|- th0

Proof

Step Hyp Ref Expression
1 bnj150.1 
 |-  ( ph <-> ( f ` (/) ) = _pred ( x , A , R ) )
2 bnj150.2 
 |-  ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
3 bnj150.3 
 |-  ( ze <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) )
4 bnj150.4 
 |-  ( ph' <-> [. 1o / n ]. ph )
5 bnj150.5 
 |-  ( ps' <-> [. 1o / n ]. ps )
6 bnj150.6 
 |-  ( th0 <-> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) ) )
7 bnj150.7 
 |-  ( ze' <-> [. 1o / n ]. ze )
8 bnj150.8 
 |-  F = { <. (/) , _pred ( x , A , R ) >. }
9 bnj150.9 
 |-  ( ph" <-> [. F / f ]. ph' )
10 bnj150.10 
 |-  ( ps" <-> [. F / f ]. ps' )
11 bnj150.11 
 |-  ( ze" <-> [. F / f ]. ze' )
12 8 bnj95 
 |-  F e. _V
13 sbceq1a 
 |-  ( f = F -> ( ze' <-> [. F / f ]. ze' ) )
14 13 11 bitr4di 
 |-  ( f = F -> ( ze' <-> ze" ) )
15 0ex 
 |-  (/) e. _V
16 bnj93 
 |-  ( ( R _FrSe A /\ x e. A ) -> _pred ( x , A , R ) e. _V )
17 funsng 
 |-  ( ( (/) e. _V /\ _pred ( x , A , R ) e. _V ) -> Fun { <. (/) , _pred ( x , A , R ) >. } )
18 15 16 17 sylancr 
 |-  ( ( R _FrSe A /\ x e. A ) -> Fun { <. (/) , _pred ( x , A , R ) >. } )
19 8 funeqi 
 |-  ( Fun F <-> Fun { <. (/) , _pred ( x , A , R ) >. } )
20 18 19 sylibr 
 |-  ( ( R _FrSe A /\ x e. A ) -> Fun F )
21 8 bnj96 
 |-  ( ( R _FrSe A /\ x e. A ) -> dom F = 1o )
22 20 21 bnj1422 
 |-  ( ( R _FrSe A /\ x e. A ) -> F Fn 1o )
23 8 bnj97 
 |-  ( ( R _FrSe A /\ x e. A ) -> ( F ` (/) ) = _pred ( x , A , R ) )
24 1 4 9 8 bnj125 
 |-  ( ph" <-> ( F ` (/) ) = _pred ( x , A , R ) )
25 23 24 sylibr 
 |-  ( ( R _FrSe A /\ x e. A ) -> ph" )
26 22 25 jca 
 |-  ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" ) )
27 bnj98 
 |-  A. i e. _om ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) )
28 2 5 10 8 bnj126 
 |-  ( ps" <-> A. i e. _om ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) )
29 27 28 mpbir 
 |-  ps"
30 df-3an 
 |-  ( ( F Fn 1o /\ ph" /\ ps" ) <-> ( ( F Fn 1o /\ ph" ) /\ ps" ) )
31 26 29 30 sylanblrc 
 |-  ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) )
32 3 7 4 5 bnj121 
 |-  ( ze' <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) )
33 8 9 10 11 32 bnj124 
 |-  ( ze" <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) )
34 31 33 mpbir 
 |-  ze"
35 12 14 34 ceqsexv2d 
 |-  E. f ze'
36 19.37v 
 |-  ( E. f ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) ) )
37 6 36 bitr4i 
 |-  ( th0 <-> E. f ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) )
38 37 32 bnj133 
 |-  ( th0 <-> E. f ze' )
39 35 38 mpbir 
 |-  th0