Metamath Proof Explorer

Theorem bnj153

Description: Technical lemma for bnj852 . 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 bnj153.1 
|- ( ph <-> ( f ` (/) ) = _pred ( x , A , R ) )
bnj153.2 
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj153.3 
|- D = ( _om \ { (/) } )
bnj153.4 
|- ( th <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ph /\ ps ) ) )
bnj153.5 
|- ( ta <-> A. m e. D ( m _E n -> [. m / n ]. th ) )
Assertion bnj153 
|- ( n = 1o -> ( ( n e. D /\ ta ) -> th ) )

Proof

Step Hyp Ref Expression
1 bnj153.1 
 |-  ( ph <-> ( f ` (/) ) = _pred ( x , A , R ) )
2 bnj153.2 
 |-  ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
3 bnj153.3 
 |-  D = ( _om \ { (/) } )
4 bnj153.4 
 |-  ( th <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ph /\ ps ) ) )
5 bnj153.5 
 |-  ( ta <-> A. m e. D ( m _E n -> [. m / n ]. th ) )
6 biid 
 |-  ( ( ( R _FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) )
7 biid 
 |-  ( [. 1o / n ]. ph <-> [. 1o / n ]. ph )
8 1 7 bnj118 
 |-  ( [. 1o / n ]. ph <-> ( f ` (/) ) = _pred ( x , A , R ) )
9 8 bicomi 
 |-  ( ( f ` (/) ) = _pred ( x , A , R ) <-> [. 1o / n ]. ph )
10 bnj105 
 |-  1o e. _V
11 2 10 bnj92 
 |-  ( [. 1o / n ]. ps <-> A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
12 11 bicomi 
 |-  ( A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> [. 1o / n ]. ps )
13 biid 
 |-  ( [. 1o / n ]. th <-> [. 1o / n ]. th )
14 biid 
 |-  ( ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ( f ` (/) ) = _pred ( x , A , R ) /\ A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) <-> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ( f ` (/) ) = _pred ( x , A , R ) /\ A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) )
15 biid 
 |-  ( ( ( R _FrSe A /\ x e. A ) -> E* f ( f Fn 1o /\ ( f ` (/) ) = _pred ( x , A , R ) /\ A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) <-> ( ( R _FrSe A /\ x e. A ) -> E* f ( f Fn 1o /\ ( f ` (/) ) = _pred ( x , A , R ) /\ A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) )
16 biid 
 |-  ( [. 1o / n ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) <-> [. 1o / n ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) )
17 biid 
 |-  ( [. 1o / n ]. ps <-> [. 1o / n ]. ps )
18 6 16 7 17 bnj121 
 |-  ( [. 1o / n ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ [. 1o / n ]. ph /\ [. 1o / n ]. ps ) ) )
19 8 anbi2i 
 |-  ( ( f Fn 1o /\ [. 1o / n ]. ph ) <-> ( f Fn 1o /\ ( f ` (/) ) = _pred ( x , A , R ) ) )
20 19 11 anbi12i 
 |-  ( ( ( f Fn 1o /\ [. 1o / n ]. ph ) /\ [. 1o / n ]. ps ) <-> ( ( f Fn 1o /\ ( f ` (/) ) = _pred ( x , A , R ) ) /\ A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) )
21 df-3an 
 |-  ( ( f Fn 1o /\ [. 1o / n ]. ph /\ [. 1o / n ]. ps ) <-> ( ( f Fn 1o /\ [. 1o / n ]. ph ) /\ [. 1o / n ]. ps ) )
22 df-3an 
 |-  ( ( f Fn 1o /\ ( f ` (/) ) = _pred ( x , A , R ) /\ A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) <-> ( ( f Fn 1o /\ ( f ` (/) ) = _pred ( x , A , R ) ) /\ A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) )
23 20 21 22 3bitr4i 
 |-  ( ( f Fn 1o /\ [. 1o / n ]. ph /\ [. 1o / n ]. ps ) <-> ( f Fn 1o /\ ( f ` (/) ) = _pred ( x , A , R ) /\ A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) )
24 23 imbi2i 
 |-  ( ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ [. 1o / n ]. ph /\ [. 1o / n ]. ps ) ) <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ( f ` (/) ) = _pred ( x , A , R ) /\ A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) )
25 18 24 bitri 
 |-  ( [. 1o / n ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ( f ` (/) ) = _pred ( x , A , R ) /\ A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) )
26 25 bicomi 
 |-  ( ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ( f ` (/) ) = _pred ( x , A , R ) /\ A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) <-> [. 1o / n ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) )
27 eqid 
 |-  { <. (/) , _pred ( x , A , R ) >. } = { <. (/) , _pred ( x , A , R ) >. }
28 biid 
 |-  ( [. { <. (/) , _pred ( x , A , R ) >. } / f ]. ( f ` (/) ) = _pred ( x , A , R ) <-> [. { <. (/) , _pred ( x , A , R ) >. } / f ]. ( f ` (/) ) = _pred ( x , A , R ) )
29 biid 
 |-  ( [. { <. (/) , _pred ( x , A , R ) >. } / f ]. A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> [. { <. (/) , _pred ( x , A , R ) >. } / f ]. A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
30 26 sbcbii 
 |-  ( [. { <. (/) , _pred ( x , A , R ) >. } / f ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ( f ` (/) ) = _pred ( x , A , R ) /\ A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) <-> [. { <. (/) , _pred ( x , A , R ) >. } / f ]. [. 1o / n ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) )
31 biid 
 |-  ( [. { <. (/) , _pred ( x , A , R ) >. } / f ]. [. 1o / n ]. ph <-> [. { <. (/) , _pred ( x , A , R ) >. } / f ]. [. 1o / n ]. ph )
32 biid 
 |-  ( [. { <. (/) , _pred ( x , A , R ) >. } / f ]. [. 1o / n ]. ps <-> [. { <. (/) , _pred ( x , A , R ) >. } / f ]. [. 1o / n ]. ps )
33 biid 
 |-  ( [. { <. (/) , _pred ( x , A , R ) >. } / f ]. [. 1o / n ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) <-> [. { <. (/) , _pred ( x , A , R ) >. } / f ]. [. 1o / n ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) )
34 27 31 32 33 18 bnj124 
 |-  ( [. { <. (/) , _pred ( x , A , R ) >. } / f ]. [. 1o / n ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) <-> ( ( R _FrSe A /\ x e. A ) -> ( { <. (/) , _pred ( x , A , R ) >. } Fn 1o /\ [. { <. (/) , _pred ( x , A , R ) >. } / f ]. [. 1o / n ]. ph /\ [. { <. (/) , _pred ( x , A , R ) >. } / f ]. [. 1o / n ]. ps ) ) )
35 1 7 31 27 bnj125 
 |-  ( [. { <. (/) , _pred ( x , A , R ) >. } / f ]. [. 1o / n ]. ph <-> ( { <. (/) , _pred ( x , A , R ) >. } ` (/) ) = _pred ( x , A , R ) )
36 35 anbi2i 
 |-  ( ( { <. (/) , _pred ( x , A , R ) >. } Fn 1o /\ [. { <. (/) , _pred ( x , A , R ) >. } / f ]. [. 1o / n ]. ph ) <-> ( { <. (/) , _pred ( x , A , R ) >. } Fn 1o /\ ( { <. (/) , _pred ( x , A , R ) >. } ` (/) ) = _pred ( x , A , R ) ) )
37 2 17 32 27 bnj126 
 |-  ( [. { <. (/) , _pred ( x , A , R ) >. } / f ]. [. 1o / n ]. ps <-> A. i e. _om ( suc i e. 1o -> ( { <. (/) , _pred ( x , A , R ) >. } ` suc i ) = U_ y e. ( { <. (/) , _pred ( x , A , R ) >. } ` i ) _pred ( y , A , R ) ) )
38 36 37 anbi12i 
 |-  ( ( ( { <. (/) , _pred ( x , A , R ) >. } Fn 1o /\ [. { <. (/) , _pred ( x , A , R ) >. } / f ]. [. 1o / n ]. ph ) /\ [. { <. (/) , _pred ( x , A , R ) >. } / f ]. [. 1o / n ]. ps ) <-> ( ( { <. (/) , _pred ( x , A , R ) >. } Fn 1o /\ ( { <. (/) , _pred ( x , A , R ) >. } ` (/) ) = _pred ( x , A , R ) ) /\ A. i e. _om ( suc i e. 1o -> ( { <. (/) , _pred ( x , A , R ) >. } ` suc i ) = U_ y e. ( { <. (/) , _pred ( x , A , R ) >. } ` i ) _pred ( y , A , R ) ) ) )
39 df-3an 
 |-  ( ( { <. (/) , _pred ( x , A , R ) >. } Fn 1o /\ [. { <. (/) , _pred ( x , A , R ) >. } / f ]. [. 1o / n ]. ph /\ [. { <. (/) , _pred ( x , A , R ) >. } / f ]. [. 1o / n ]. ps ) <-> ( ( { <. (/) , _pred ( x , A , R ) >. } Fn 1o /\ [. { <. (/) , _pred ( x , A , R ) >. } / f ]. [. 1o / n ]. ph ) /\ [. { <. (/) , _pred ( x , A , R ) >. } / f ]. [. 1o / n ]. ps ) )
40 df-3an 
 |-  ( ( { <. (/) , _pred ( x , A , R ) >. } Fn 1o /\ ( { <. (/) , _pred ( x , A , R ) >. } ` (/) ) = _pred ( x , A , R ) /\ A. i e. _om ( suc i e. 1o -> ( { <. (/) , _pred ( x , A , R ) >. } ` suc i ) = U_ y e. ( { <. (/) , _pred ( x , A , R ) >. } ` i ) _pred ( y , A , R ) ) ) <-> ( ( { <. (/) , _pred ( x , A , R ) >. } Fn 1o /\ ( { <. (/) , _pred ( x , A , R ) >. } ` (/) ) = _pred ( x , A , R ) ) /\ A. i e. _om ( suc i e. 1o -> ( { <. (/) , _pred ( x , A , R ) >. } ` suc i ) = U_ y e. ( { <. (/) , _pred ( x , A , R ) >. } ` i ) _pred ( y , A , R ) ) ) )
41 38 39 40 3bitr4i 
 |-  ( ( { <. (/) , _pred ( x , A , R ) >. } Fn 1o /\ [. { <. (/) , _pred ( x , A , R ) >. } / f ]. [. 1o / n ]. ph /\ [. { <. (/) , _pred ( x , A , R ) >. } / f ]. [. 1o / n ]. ps ) <-> ( { <. (/) , _pred ( x , A , R ) >. } Fn 1o /\ ( { <. (/) , _pred ( x , A , R ) >. } ` (/) ) = _pred ( x , A , R ) /\ A. i e. _om ( suc i e. 1o -> ( { <. (/) , _pred ( x , A , R ) >. } ` suc i ) = U_ y e. ( { <. (/) , _pred ( x , A , R ) >. } ` i ) _pred ( y , A , R ) ) ) )
42 41 imbi2i 
 |-  ( ( ( R _FrSe A /\ x e. A ) -> ( { <. (/) , _pred ( x , A , R ) >. } Fn 1o /\ [. { <. (/) , _pred ( x , A , R ) >. } / f ]. [. 1o / n ]. ph /\ [. { <. (/) , _pred ( x , A , R ) >. } / f ]. [. 1o / n ]. ps ) ) <-> ( ( R _FrSe A /\ x e. A ) -> ( { <. (/) , _pred ( x , A , R ) >. } Fn 1o /\ ( { <. (/) , _pred ( x , A , R ) >. } ` (/) ) = _pred ( x , A , R ) /\ A. i e. _om ( suc i e. 1o -> ( { <. (/) , _pred ( x , A , R ) >. } ` suc i ) = U_ y e. ( { <. (/) , _pred ( x , A , R ) >. } ` i ) _pred ( y , A , R ) ) ) ) )
43 34 42 bitri 
 |-  ( [. { <. (/) , _pred ( x , A , R ) >. } / f ]. [. 1o / n ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) <-> ( ( R _FrSe A /\ x e. A ) -> ( { <. (/) , _pred ( x , A , R ) >. } Fn 1o /\ ( { <. (/) , _pred ( x , A , R ) >. } ` (/) ) = _pred ( x , A , R ) /\ A. i e. _om ( suc i e. 1o -> ( { <. (/) , _pred ( x , A , R ) >. } ` suc i ) = U_ y e. ( { <. (/) , _pred ( x , A , R ) >. } ` i ) _pred ( y , A , R ) ) ) ) )
44 30 43 bitr2i 
 |-  ( ( ( R _FrSe A /\ x e. A ) -> ( { <. (/) , _pred ( x , A , R ) >. } Fn 1o /\ ( { <. (/) , _pred ( x , A , R ) >. } ` (/) ) = _pred ( x , A , R ) /\ A. i e. _om ( suc i e. 1o -> ( { <. (/) , _pred ( x , A , R ) >. } ` suc i ) = U_ y e. ( { <. (/) , _pred ( x , A , R ) >. } ` i ) _pred ( y , A , R ) ) ) ) <-> [. { <. (/) , _pred ( x , A , R ) >. } / f ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ( f ` (/) ) = _pred ( x , A , R ) /\ A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) )
45 biid 
 |-  ( ( f Fn 1o /\ ( f ` (/) ) = _pred ( x , A , R ) /\ A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) <-> ( f Fn 1o /\ ( f ` (/) ) = _pred ( x , A , R ) /\ A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) )
46 biid 
 |-  ( ( f Fn 1o /\ [. 1o / n ]. ph /\ [. 1o / n ]. ps ) <-> ( f Fn 1o /\ [. 1o / n ]. ph /\ [. 1o / n ]. ps ) )
47 biid 
 |-  ( [. g / f ]. ( f Fn 1o /\ [. 1o / n ]. ph /\ [. 1o / n ]. ps ) <-> [. g / f ]. ( f Fn 1o /\ [. 1o / n ]. ph /\ [. 1o / n ]. ps ) )
48 biid 
 |-  ( [. g / f ]. [. 1o / n ]. ph <-> [. g / f ]. [. 1o / n ]. ph )
49 biid 
 |-  ( [. g / f ]. [. 1o / n ]. ps <-> [. g / f ]. [. 1o / n ]. ps )
50 46 47 48 49 bnj156 
 |-  ( [. g / f ]. ( f Fn 1o /\ [. 1o / n ]. ph /\ [. 1o / n ]. ps ) <-> ( g Fn 1o /\ [. g / f ]. [. 1o / n ]. ph /\ [. g / f ]. [. 1o / n ]. ps ) )
51 48 8 bnj154 
 |-  ( [. g / f ]. [. 1o / n ]. ph <-> ( g ` (/) ) = _pred ( x , A , R ) )
52 51 anbi2i 
 |-  ( ( g Fn 1o /\ [. g / f ]. [. 1o / n ]. ph ) <-> ( g Fn 1o /\ ( g ` (/) ) = _pred ( x , A , R ) ) )
53 17 11 bitri 
 |-  ( [. 1o / n ]. ps <-> A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
54 49 53 bnj155 
 |-  ( [. g / f ]. [. 1o / n ]. ps <-> A. i e. _om ( suc i e. 1o -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) )
55 52 54 anbi12i 
 |-  ( ( ( g Fn 1o /\ [. g / f ]. [. 1o / n ]. ph ) /\ [. g / f ]. [. 1o / n ]. ps ) <-> ( ( g Fn 1o /\ ( g ` (/) ) = _pred ( x , A , R ) ) /\ A. i e. _om ( suc i e. 1o -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) )
56 df-3an 
 |-  ( ( g Fn 1o /\ [. g / f ]. [. 1o / n ]. ph /\ [. g / f ]. [. 1o / n ]. ps ) <-> ( ( g Fn 1o /\ [. g / f ]. [. 1o / n ]. ph ) /\ [. g / f ]. [. 1o / n ]. ps ) )
57 df-3an 
 |-  ( ( g Fn 1o /\ ( g ` (/) ) = _pred ( x , A , R ) /\ A. i e. _om ( suc i e. 1o -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) <-> ( ( g Fn 1o /\ ( g ` (/) ) = _pred ( x , A , R ) ) /\ A. i e. _om ( suc i e. 1o -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) )
58 55 56 57 3bitr4i 
 |-  ( ( g Fn 1o /\ [. g / f ]. [. 1o / n ]. ph /\ [. g / f ]. [. 1o / n ]. ps ) <-> ( g Fn 1o /\ ( g ` (/) ) = _pred ( x , A , R ) /\ A. i e. _om ( suc i e. 1o -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) )
59 50 58 bitri 
 |-  ( [. g / f ]. ( f Fn 1o /\ [. 1o / n ]. ph /\ [. 1o / n ]. ps ) <-> ( g Fn 1o /\ ( g ` (/) ) = _pred ( x , A , R ) /\ A. i e. _om ( suc i e. 1o -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) )
60 23 sbcbii 
 |-  ( [. g / f ]. ( f Fn 1o /\ [. 1o / n ]. ph /\ [. 1o / n ]. ps ) <-> [. g / f ]. ( f Fn 1o /\ ( f ` (/) ) = _pred ( x , A , R ) /\ A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) )
61 59 60 bitr3i 
 |-  ( ( g Fn 1o /\ ( g ` (/) ) = _pred ( x , A , R ) /\ A. i e. _om ( suc i e. 1o -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) <-> [. g / f ]. ( f Fn 1o /\ ( f ` (/) ) = _pred ( x , A , R ) /\ A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) )
62 biid 
 |-  ( [. g / f ]. ( f ` (/) ) = _pred ( x , A , R ) <-> [. g / f ]. ( f ` (/) ) = _pred ( x , A , R ) )
63 biid 
 |-  ( [. g / f ]. A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> [. g / f ]. A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
64 1 2 3 4 5 6 9 12 13 14 15 26 27 28 29 44 45 61 62 63 bnj151 
 |-  ( n = 1o -> ( ( n e. D /\ ta ) -> th ) )