Metamath Proof Explorer

Theorem bnj849

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

Ref Expression
Hypotheses bnj849.1 
|- ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
bnj849.2 
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj849.3 
|- D = ( _om \ { (/) } )
bnj849.4 
|- B = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
bnj849.5 
|- ( ch <-> ( R _FrSe A /\ X e. A /\ n e. D ) )
bnj849.6 
|- ( th <-> ( f Fn n /\ ph /\ ps ) )
bnj849.7 
|- ( ph' <-> [. g / f ]. ph )
bnj849.8 
|- ( ps' <-> [. g / f ]. ps )
bnj849.9 
|- ( th' <-> [. g / f ]. th )
bnj849.10 
|- ( ta <-> ( R _FrSe A /\ X e. A ) )
Assertion bnj849 
|- ( ( R _FrSe A /\ X e. A ) -> B e. _V )

Proof

Step Hyp Ref Expression
1 bnj849.1 
 |-  ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
2 bnj849.2 
 |-  ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
3 bnj849.3 
 |-  D = ( _om \ { (/) } )
4 bnj849.4 
 |-  B = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
5 bnj849.5 
 |-  ( ch <-> ( R _FrSe A /\ X e. A /\ n e. D ) )
6 bnj849.6 
 |-  ( th <-> ( f Fn n /\ ph /\ ps ) )
7 bnj849.7 
 |-  ( ph' <-> [. g / f ]. ph )
8 bnj849.8 
 |-  ( ps' <-> [. g / f ]. ps )
9 bnj849.9 
 |-  ( th' <-> [. g / f ]. th )
10 bnj849.10 
 |-  ( ta <-> ( R _FrSe A /\ X e. A ) )
11 1 2 3 5 6 bnj865 
 |-  E. w A. n ( ch -> E. f e. w th )
12 4 7 8 bnj873 
 |-  B = { g | E. n e. D ( g Fn n /\ ph' /\ ps' ) }
13 df-rex 
 |-  ( E. n e. D ( g Fn n /\ ph' /\ ps' ) <-> E. n ( n e. D /\ ( g Fn n /\ ph' /\ ps' ) ) )
14 19.29 
 |-  ( ( A. n ( ch -> E. f e. w th ) /\ E. n ( n e. D /\ ( g Fn n /\ ph' /\ ps' ) ) ) -> E. n ( ( ch -> E. f e. w th ) /\ ( n e. D /\ ( g Fn n /\ ph' /\ ps' ) ) ) )
15 an12 
 |-  ( ( ( ch -> E. f e. w th ) /\ ( n e. D /\ ( g Fn n /\ ph' /\ ps' ) ) ) <-> ( n e. D /\ ( ( ch -> E. f e. w th ) /\ ( g Fn n /\ ph' /\ ps' ) ) ) )
16 df-3an 
 |-  ( ( R _FrSe A /\ X e. A /\ n e. D ) <-> ( ( R _FrSe A /\ X e. A ) /\ n e. D ) )
17 10 anbi1i 
 |-  ( ( ta /\ n e. D ) <-> ( ( R _FrSe A /\ X e. A ) /\ n e. D ) )
18 16 5 17 3bitr4i 
 |-  ( ch <-> ( ta /\ n e. D ) )
19 id 
 |-  ( ch -> ch )
20 6 7 8 9 bnj581 
 |-  ( th' <-> ( g Fn n /\ ph' /\ ps' ) )
21 9 20 bitr3i 
 |-  ( [. g / f ]. th <-> ( g Fn n /\ ph' /\ ps' ) )
22 1 2 3 5 6 bnj864 
 |-  ( ch -> E! f th )
23 df-rex 
 |-  ( E. f e. w th <-> E. f ( f e. w /\ th ) )
24 exancom 
 |-  ( E. f ( f e. w /\ th ) <-> E. f ( th /\ f e. w ) )
25 23 24 sylbb 
 |-  ( E. f e. w th -> E. f ( th /\ f e. w ) )
26 nfeu1 
 |-  F/ f E! f th
27 nfe1 
 |-  F/ f E. f ( th /\ f e. w )
28 26 27 nfan 
 |-  F/ f ( E! f th /\ E. f ( th /\ f e. w ) )
29 nfsbc1v 
 |-  F/ f [. g / f ]. th
30 nfv 
 |-  F/ f g e. w
31 29 30 nfim 
 |-  F/ f ( [. g / f ]. th -> g e. w )
32 28 31 nfim 
 |-  F/ f ( ( E! f th /\ E. f ( th /\ f e. w ) ) -> ( [. g / f ]. th -> g e. w ) )
33 sbceq1a 
 |-  ( f = g -> ( th <-> [. g / f ]. th ) )
34 elequ1 
 |-  ( f = g -> ( f e. w <-> g e. w ) )
35 33 34 imbi12d 
 |-  ( f = g -> ( ( th -> f e. w ) <-> ( [. g / f ]. th -> g e. w ) ) )
36 35 imbi2d 
 |-  ( f = g -> ( ( ( E! f th /\ E. f ( th /\ f e. w ) ) -> ( th -> f e. w ) ) <-> ( ( E! f th /\ E. f ( th /\ f e. w ) ) -> ( [. g / f ]. th -> g e. w ) ) ) )
37 eupick 
 |-  ( ( E! f th /\ E. f ( th /\ f e. w ) ) -> ( th -> f e. w ) )
38 32 36 37 chvarfv 
 |-  ( ( E! f th /\ E. f ( th /\ f e. w ) ) -> ( [. g / f ]. th -> g e. w ) )
39 22 25 38 syl2an 
 |-  ( ( ch /\ E. f e. w th ) -> ( [. g / f ]. th -> g e. w ) )
40 21 39 syl5bir 
 |-  ( ( ch /\ E. f e. w th ) -> ( ( g Fn n /\ ph' /\ ps' ) -> g e. w ) )
41 40 ex 
 |-  ( ch -> ( E. f e. w th -> ( ( g Fn n /\ ph' /\ ps' ) -> g e. w ) ) )
42 19 41 embantd 
 |-  ( ch -> ( ( ch -> E. f e. w th ) -> ( ( g Fn n /\ ph' /\ ps' ) -> g e. w ) ) )
43 42 impd 
 |-  ( ch -> ( ( ( ch -> E. f e. w th ) /\ ( g Fn n /\ ph' /\ ps' ) ) -> g e. w ) )
44 18 43 sylbir 
 |-  ( ( ta /\ n e. D ) -> ( ( ( ch -> E. f e. w th ) /\ ( g Fn n /\ ph' /\ ps' ) ) -> g e. w ) )
45 44 expimpd 
 |-  ( ta -> ( ( n e. D /\ ( ( ch -> E. f e. w th ) /\ ( g Fn n /\ ph' /\ ps' ) ) ) -> g e. w ) )
46 15 45 syl5bi 
 |-  ( ta -> ( ( ( ch -> E. f e. w th ) /\ ( n e. D /\ ( g Fn n /\ ph' /\ ps' ) ) ) -> g e. w ) )
47 46 exlimdv 
 |-  ( ta -> ( E. n ( ( ch -> E. f e. w th ) /\ ( n e. D /\ ( g Fn n /\ ph' /\ ps' ) ) ) -> g e. w ) )
48 14 47 syl5 
 |-  ( ta -> ( ( A. n ( ch -> E. f e. w th ) /\ E. n ( n e. D /\ ( g Fn n /\ ph' /\ ps' ) ) ) -> g e. w ) )
49 48 expdimp 
 |-  ( ( ta /\ A. n ( ch -> E. f e. w th ) ) -> ( E. n ( n e. D /\ ( g Fn n /\ ph' /\ ps' ) ) -> g e. w ) )
50 13 49 syl5bi 
 |-  ( ( ta /\ A. n ( ch -> E. f e. w th ) ) -> ( E. n e. D ( g Fn n /\ ph' /\ ps' ) -> g e. w ) )
51 50 abssdv 
 |-  ( ( ta /\ A. n ( ch -> E. f e. w th ) ) -> { g | E. n e. D ( g Fn n /\ ph' /\ ps' ) } C_ w )
52 12 51 eqsstrid 
 |-  ( ( ta /\ A. n ( ch -> E. f e. w th ) ) -> B C_ w )
53 vex 
 |-  w e. _V
54 53 ssex 
 |-  ( B C_ w -> B e. _V )
55 52 54 syl 
 |-  ( ( ta /\ A. n ( ch -> E. f e. w th ) ) -> B e. _V )
56 55 ex 
 |-  ( ta -> ( A. n ( ch -> E. f e. w th ) -> B e. _V ) )
57 56 exlimdv 
 |-  ( ta -> ( E. w A. n ( ch -> E. f e. w th ) -> B e. _V ) )
58 11 57 mpi 
 |-  ( ta -> B e. _V )
59 10 58 sylbir 
 |-  ( ( R _FrSe A /\ X e. A ) -> B e. _V )