Metamath Proof Explorer

Theorem bnj149

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) (Proof shortened by Mario Carneiro, 22-Dec-2016) (New usage is discouraged.)

Ref Expression
Hypotheses bnj149.1 
|- ( th1 <-> ( ( R _FrSe A /\ x e. A ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) ) )
bnj149.2 
|- ( ze0 <-> ( f Fn 1o /\ ph' /\ ps' ) )
bnj149.3 
|- ( ze1 <-> [. g / f ]. ze0 )
bnj149.4 
|- ( ph1 <-> [. g / f ]. ph' )
bnj149.5 
|- ( ps1 <-> [. g / f ]. ps' )
bnj149.6 
|- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) )
Assertion bnj149 
|- th1

Proof

Step Hyp Ref Expression
1 bnj149.1 
 |-  ( th1 <-> ( ( R _FrSe A /\ x e. A ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) ) )
2 bnj149.2 
 |-  ( ze0 <-> ( f Fn 1o /\ ph' /\ ps' ) )
3 bnj149.3 
 |-  ( ze1 <-> [. g / f ]. ze0 )
4 bnj149.4 
 |-  ( ph1 <-> [. g / f ]. ph' )
5 bnj149.5 
 |-  ( ps1 <-> [. g / f ]. ps' )
6 bnj149.6 
 |-  ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) )
7 simpr1 
 |-  ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> f Fn 1o )
8 df1o2 
 |-  1o = { (/) }
9 8 fneq2i 
 |-  ( f Fn 1o <-> f Fn { (/) } )
10 7 9 sylib 
 |-  ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> f Fn { (/) } )
11 simpr2 
 |-  ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> ph' )
12 11 6 sylib 
 |-  ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> ( f ` (/) ) = _pred ( x , A , R ) )
13 fvex 
 |-  ( f ` (/) ) e. _V
14 13 elsn 
 |-  ( ( f ` (/) ) e. { _pred ( x , A , R ) } <-> ( f ` (/) ) = _pred ( x , A , R ) )
15 12 14 sylibr 
 |-  ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> ( f ` (/) ) e. { _pred ( x , A , R ) } )
16 0ex 
 |-  (/) e. _V
17 fveq2 
 |-  ( g = (/) -> ( f ` g ) = ( f ` (/) ) )
18 17 eleq1d 
 |-  ( g = (/) -> ( ( f ` g ) e. { _pred ( x , A , R ) } <-> ( f ` (/) ) e. { _pred ( x , A , R ) } ) )
19 16 18 ralsn 
 |-  ( A. g e. { (/) } ( f ` g ) e. { _pred ( x , A , R ) } <-> ( f ` (/) ) e. { _pred ( x , A , R ) } )
20 15 19 sylibr 
 |-  ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> A. g e. { (/) } ( f ` g ) e. { _pred ( x , A , R ) } )
21 ffnfv 
 |-  ( f : { (/) } --> { _pred ( x , A , R ) } <-> ( f Fn { (/) } /\ A. g e. { (/) } ( f ` g ) e. { _pred ( x , A , R ) } ) )
22 10 20 21 sylanbrc 
 |-  ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> f : { (/) } --> { _pred ( x , A , R ) } )
23 bnj93 
 |-  ( ( R _FrSe A /\ x e. A ) -> _pred ( x , A , R ) e. _V )
24 23 adantr 
 |-  ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> _pred ( x , A , R ) e. _V )
25 fsng 
 |-  ( ( (/) e. _V /\ _pred ( x , A , R ) e. _V ) -> ( f : { (/) } --> { _pred ( x , A , R ) } <-> f = { <. (/) , _pred ( x , A , R ) >. } ) )
26 16 24 25 sylancr 
 |-  ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> ( f : { (/) } --> { _pred ( x , A , R ) } <-> f = { <. (/) , _pred ( x , A , R ) >. } ) )
27 22 26 mpbid 
 |-  ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> f = { <. (/) , _pred ( x , A , R ) >. } )
28 27 ex 
 |-  ( ( R _FrSe A /\ x e. A ) -> ( ( f Fn 1o /\ ph' /\ ps' ) -> f = { <. (/) , _pred ( x , A , R ) >. } ) )
29 28 alrimiv 
 |-  ( ( R _FrSe A /\ x e. A ) -> A. f ( ( f Fn 1o /\ ph' /\ ps' ) -> f = { <. (/) , _pred ( x , A , R ) >. } ) )
30 mo2icl 
 |-  ( A. f ( ( f Fn 1o /\ ph' /\ ps' ) -> f = { <. (/) , _pred ( x , A , R ) >. } ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) )
31 29 30 syl 
 |-  ( ( R _FrSe A /\ x e. A ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) )
32 31 1 mpbir 
 |-  th1