Metamath Proof Explorer

Theorem bnj864

Description: Technical lemma for bnj69 . 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 bnj864.1 
|- ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
bnj864.2 
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj864.3 
|- D = ( _om \ { (/) } )
bnj864.4 
|- ( ch <-> ( R _FrSe A /\ X e. A /\ n e. D ) )
bnj864.5 
|- ( th <-> ( f Fn n /\ ph /\ ps ) )
Assertion bnj864 
|- ( ch -> E! f th )

Proof

Step Hyp Ref Expression
1 bnj864.1 
 |-  ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
2 bnj864.2 
 |-  ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
3 bnj864.3 
 |-  D = ( _om \ { (/) } )
4 bnj864.4 
 |-  ( ch <-> ( R _FrSe A /\ X e. A /\ n e. D ) )
5 bnj864.5 
 |-  ( th <-> ( f Fn n /\ ph /\ ps ) )
6 1 2 3 bnj852 
 |-  ( ( R _FrSe A /\ X e. A ) -> A. n e. D E! f ( f Fn n /\ ph /\ ps ) )
7 df-ral 
 |-  ( A. n e. D E! f ( f Fn n /\ ph /\ ps ) <-> A. n ( n e. D -> E! f ( f Fn n /\ ph /\ ps ) ) )
8 7 imbi2i 
 |-  ( ( ( R _FrSe A /\ X e. A ) -> A. n e. D E! f ( f Fn n /\ ph /\ ps ) ) <-> ( ( R _FrSe A /\ X e. A ) -> A. n ( n e. D -> E! f ( f Fn n /\ ph /\ ps ) ) ) )
9 19.21v 
 |-  ( A. n ( ( R _FrSe A /\ X e. A ) -> ( n e. D -> E! f ( f Fn n /\ ph /\ ps ) ) ) <-> ( ( R _FrSe A /\ X e. A ) -> A. n ( n e. D -> E! f ( f Fn n /\ ph /\ ps ) ) ) )
10 impexp 
 |-  ( ( ( ( R _FrSe A /\ X e. A ) /\ n e. D ) -> E! f ( f Fn n /\ ph /\ ps ) ) <-> ( ( R _FrSe A /\ X e. A ) -> ( n e. D -> E! f ( f Fn n /\ ph /\ ps ) ) ) )
11 df-3an 
 |-  ( ( R _FrSe A /\ X e. A /\ n e. D ) <-> ( ( R _FrSe A /\ X e. A ) /\ n e. D ) )
12 11 bicomi 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ n e. D ) <-> ( R _FrSe A /\ X e. A /\ n e. D ) )
13 12 imbi1i 
 |-  ( ( ( ( R _FrSe A /\ X e. A ) /\ n e. D ) -> E! f ( f Fn n /\ ph /\ ps ) ) <-> ( ( R _FrSe A /\ X e. A /\ n e. D ) -> E! f ( f Fn n /\ ph /\ ps ) ) )
14 10 13 bitr3i 
 |-  ( ( ( R _FrSe A /\ X e. A ) -> ( n e. D -> E! f ( f Fn n /\ ph /\ ps ) ) ) <-> ( ( R _FrSe A /\ X e. A /\ n e. D ) -> E! f ( f Fn n /\ ph /\ ps ) ) )
15 14 albii 
 |-  ( A. n ( ( R _FrSe A /\ X e. A ) -> ( n e. D -> E! f ( f Fn n /\ ph /\ ps ) ) ) <-> A. n ( ( R _FrSe A /\ X e. A /\ n e. D ) -> E! f ( f Fn n /\ ph /\ ps ) ) )
16 8 9 15 3bitr2i 
 |-  ( ( ( R _FrSe A /\ X e. A ) -> A. n e. D E! f ( f Fn n /\ ph /\ ps ) ) <-> A. n ( ( R _FrSe A /\ X e. A /\ n e. D ) -> E! f ( f Fn n /\ ph /\ ps ) ) )
17 6 16 mpbi 
 |-  A. n ( ( R _FrSe A /\ X e. A /\ n e. D ) -> E! f ( f Fn n /\ ph /\ ps ) )
18 17 spi 
 |-  ( ( R _FrSe A /\ X e. A /\ n e. D ) -> E! f ( f Fn n /\ ph /\ ps ) )
19 5 eubii 
 |-  ( E! f th <-> E! f ( f Fn n /\ ph /\ ps ) )
20 18 4 19 3imtr4i 
 |-  ( ch -> E! f th )