Metamath Proof Explorer

Theorem bnj865

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 bnj865.1 
|- ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
bnj865.2 
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj865.3 
|- D = ( _om \ { (/) } )
bnj865.5 
|- ( ch <-> ( R _FrSe A /\ X e. A /\ n e. D ) )
bnj865.6 
|- ( th <-> ( f Fn n /\ ph /\ ps ) )
Assertion bnj865 
|- E. w A. n ( ch -> E. f e. w th )

Proof

Step Hyp Ref Expression
1 bnj865.1 
 |-  ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
2 bnj865.2 
 |-  ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
3 bnj865.3 
 |-  D = ( _om \ { (/) } )
4 bnj865.5 
 |-  ( ch <-> ( R _FrSe A /\ X e. A /\ n e. D ) )
5 bnj865.6 
 |-  ( 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 omex 
 |-  _om e. _V
8 difexg 
 |-  ( _om e. _V -> ( _om \ { (/) } ) e. _V )
9 7 8 ax-mp 
 |-  ( _om \ { (/) } ) e. _V
10 3 9 eqeltri 
 |-  D e. _V
11 raleq 
 |-  ( z = D -> ( A. n e. z E! f ( f Fn n /\ ph /\ ps ) <-> A. n e. D E! f ( f Fn n /\ ph /\ ps ) ) )
12 raleq 
 |-  ( z = D -> ( A. n e. z E. f e. w ( f Fn n /\ ph /\ ps ) <-> A. n e. D E. f e. w ( f Fn n /\ ph /\ ps ) ) )
13 12 exbidv 
 |-  ( z = D -> ( E. w A. n e. z E. f e. w ( f Fn n /\ ph /\ ps ) <-> E. w A. n e. D E. f e. w ( f Fn n /\ ph /\ ps ) ) )
14 11 13 imbi12d 
 |-  ( z = D -> ( ( A. n e. z E! f ( f Fn n /\ ph /\ ps ) -> E. w A. n e. z E. f e. w ( f Fn n /\ ph /\ ps ) ) <-> ( A. n e. D E! f ( f Fn n /\ ph /\ ps ) -> E. w A. n e. D E. f e. w ( f Fn n /\ ph /\ ps ) ) ) )
15 zfrep6 
 |-  ( A. n e. z E! f ( f Fn n /\ ph /\ ps ) -> E. w A. n e. z E. f e. w ( f Fn n /\ ph /\ ps ) )
16 10 14 15 vtocl 
 |-  ( A. n e. D E! f ( f Fn n /\ ph /\ ps ) -> E. w A. n e. D E. f e. w ( f Fn n /\ ph /\ ps ) )
17 6 16 syl 
 |-  ( ( R _FrSe A /\ X e. A ) -> E. w A. n e. D E. f e. w ( f Fn n /\ ph /\ ps ) )
18 19.37v 
 |-  ( E. w ( ( R _FrSe A /\ X e. A ) -> A. n e. D E. f e. w ( f Fn n /\ ph /\ ps ) ) <-> ( ( R _FrSe A /\ X e. A ) -> E. w A. n e. D E. f e. w ( f Fn n /\ ph /\ ps ) ) )
19 17 18 mpbir 
 |-  E. w ( ( R _FrSe A /\ X e. A ) -> A. n e. D E. f e. w ( f Fn n /\ ph /\ ps ) )
20 df-ral 
 |-  ( A. n e. D E. f e. w ( f Fn n /\ ph /\ ps ) <-> A. n ( n e. D -> E. f e. w ( f Fn n /\ ph /\ ps ) ) )
21 20 imbi2i 
 |-  ( ( ( R _FrSe A /\ X e. A ) -> A. n e. D E. f e. w ( f Fn n /\ ph /\ ps ) ) <-> ( ( R _FrSe A /\ X e. A ) -> A. n ( n e. D -> E. f e. w ( f Fn n /\ ph /\ ps ) ) ) )
22 19.21v 
 |-  ( A. n ( ( R _FrSe A /\ X e. A ) -> ( n e. D -> E. f e. w ( f Fn n /\ ph /\ ps ) ) ) <-> ( ( R _FrSe A /\ X e. A ) -> A. n ( n e. D -> E. f e. w ( f Fn n /\ ph /\ ps ) ) ) )
23 21 22 bitr4i 
 |-  ( ( ( R _FrSe A /\ X e. A ) -> A. n e. D E. f e. w ( f Fn n /\ ph /\ ps ) ) <-> A. n ( ( R _FrSe A /\ X e. A ) -> ( n e. D -> E. f e. w ( f Fn n /\ ph /\ ps ) ) ) )
24 23 exbii 
 |-  ( E. w ( ( R _FrSe A /\ X e. A ) -> A. n e. D E. f e. w ( f Fn n /\ ph /\ ps ) ) <-> E. w A. n ( ( R _FrSe A /\ X e. A ) -> ( n e. D -> E. f e. w ( f Fn n /\ ph /\ ps ) ) ) )
25 impexp 
 |-  ( ( ( ( R _FrSe A /\ X e. A ) /\ n e. D ) -> E. f e. w ( f Fn n /\ ph /\ ps ) ) <-> ( ( R _FrSe A /\ X e. A ) -> ( n e. D -> E. f e. w ( f Fn n /\ ph /\ ps ) ) ) )
26 df-3an 
 |-  ( ( R _FrSe A /\ X e. A /\ n e. D ) <-> ( ( R _FrSe A /\ X e. A ) /\ n e. D ) )
27 26 bicomi 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ n e. D ) <-> ( R _FrSe A /\ X e. A /\ n e. D ) )
28 27 imbi1i 
 |-  ( ( ( ( R _FrSe A /\ X e. A ) /\ n e. D ) -> E. f e. w ( f Fn n /\ ph /\ ps ) ) <-> ( ( R _FrSe A /\ X e. A /\ n e. D ) -> E. f e. w ( f Fn n /\ ph /\ ps ) ) )
29 25 28 bitr3i 
 |-  ( ( ( R _FrSe A /\ X e. A ) -> ( n e. D -> E. f e. w ( f Fn n /\ ph /\ ps ) ) ) <-> ( ( R _FrSe A /\ X e. A /\ n e. D ) -> E. f e. w ( f Fn n /\ ph /\ ps ) ) )
30 29 albii 
 |-  ( A. n ( ( R _FrSe A /\ X e. A ) -> ( n e. D -> E. f e. w ( f Fn n /\ ph /\ ps ) ) ) <-> A. n ( ( R _FrSe A /\ X e. A /\ n e. D ) -> E. f e. w ( f Fn n /\ ph /\ ps ) ) )
31 30 exbii 
 |-  ( E. w A. n ( ( R _FrSe A /\ X e. A ) -> ( n e. D -> E. f e. w ( f Fn n /\ ph /\ ps ) ) ) <-> E. w A. n ( ( R _FrSe A /\ X e. A /\ n e. D ) -> E. f e. w ( f Fn n /\ ph /\ ps ) ) )
32 24 31 bitri 
 |-  ( E. w ( ( R _FrSe A /\ X e. A ) -> A. n e. D E. f e. w ( f Fn n /\ ph /\ ps ) ) <-> E. w A. n ( ( R _FrSe A /\ X e. A /\ n e. D ) -> E. f e. w ( f Fn n /\ ph /\ ps ) ) )
33 19 32 mpbi 
 |-  E. w A. n ( ( R _FrSe A /\ X e. A /\ n e. D ) -> E. f e. w ( f Fn n /\ ph /\ ps ) )
34 4 bicomi 
 |-  ( ( R _FrSe A /\ X e. A /\ n e. D ) <-> ch )
35 34 imbi1i 
 |-  ( ( ( R _FrSe A /\ X e. A /\ n e. D ) -> E. f e. w ( f Fn n /\ ph /\ ps ) ) <-> ( ch -> E. f e. w ( f Fn n /\ ph /\ ps ) ) )
36 35 albii 
 |-  ( A. n ( ( R _FrSe A /\ X e. A /\ n e. D ) -> E. f e. w ( f Fn n /\ ph /\ ps ) ) <-> A. n ( ch -> E. f e. w ( f Fn n /\ ph /\ ps ) ) )
37 36 exbii 
 |-  ( E. w A. n ( ( R _FrSe A /\ X e. A /\ n e. D ) -> E. f e. w ( f Fn n /\ ph /\ ps ) ) <-> E. w A. n ( ch -> E. f e. w ( f Fn n /\ ph /\ ps ) ) )
38 33 37 mpbi 
 |-  E. w A. n ( ch -> E. f e. w ( f Fn n /\ ph /\ ps ) )
39 5 rexbii 
 |-  ( E. f e. w th <-> E. f e. w ( f Fn n /\ ph /\ ps ) )
40 39 imbi2i 
 |-  ( ( ch -> E. f e. w th ) <-> ( ch -> E. f e. w ( f Fn n /\ ph /\ ps ) ) )
41 40 albii 
 |-  ( A. n ( ch -> E. f e. w th ) <-> A. n ( ch -> E. f e. w ( f Fn n /\ ph /\ ps ) ) )
42 41 exbii 
 |-  ( E. w A. n ( ch -> E. f e. w th ) <-> E. w A. n ( ch -> E. f e. w ( f Fn n /\ ph /\ ps ) ) )
43 38 42 mpbir 
 |-  E. w A. n ( ch -> E. f e. w th )