Metamath Proof Explorer

Theorem bnj543

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 bnj543.1 
|- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) )
bnj543.2 
|- ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj543.3 
|- G = ( f u. { <. m , U_ y e. ( f ` p ) _pred ( y , A , R ) >. } )
bnj543.4 
|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) )
bnj543.5 
|- ( si <-> ( m e. _om /\ n = suc m /\ p e. m ) )
Assertion bnj543 
|- ( ( R _FrSe A /\ ta /\ si ) -> G Fn n )

Proof

Step Hyp Ref Expression
1 bnj543.1 
 |-  ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) )
2 bnj543.2 
 |-  ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
3 bnj543.3 
 |-  G = ( f u. { <. m , U_ y e. ( f ` p ) _pred ( y , A , R ) >. } )
4 bnj543.4 
 |-  ( ta <-> ( f Fn m /\ ph' /\ ps' ) )
5 bnj543.5 
 |-  ( si <-> ( m e. _om /\ n = suc m /\ p e. m ) )
6 bnj257 
 |-  ( ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) <-> ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) /\ f Fn m /\ n = suc m ) )
7 bnj268 
 |-  ( ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) /\ f Fn m /\ n = suc m ) <-> ( ( ph' /\ ps' ) /\ f Fn m /\ ( m e. _om /\ p e. m ) /\ n = suc m ) )
8 6 7 bitri 
 |-  ( ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) <-> ( ( ph' /\ ps' ) /\ f Fn m /\ ( m e. _om /\ p e. m ) /\ n = suc m ) )
9 bnj253 
 |-  ( ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) <-> ( ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) ) /\ n = suc m /\ f Fn m ) )
10 bnj256 
 |-  ( ( ( ph' /\ ps' ) /\ f Fn m /\ ( m e. _om /\ p e. m ) /\ n = suc m ) <-> ( ( ( ph' /\ ps' ) /\ f Fn m ) /\ ( ( m e. _om /\ p e. m ) /\ n = suc m ) ) )
11 8 9 10 3bitr3i 
 |-  ( ( ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) ) /\ n = suc m /\ f Fn m ) <-> ( ( ( ph' /\ ps' ) /\ f Fn m ) /\ ( ( m e. _om /\ p e. m ) /\ n = suc m ) ) )
12 bnj256 
 |-  ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) <-> ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) ) )
13 12 3anbi1i 
 |-  ( ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) <-> ( ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) ) /\ n = suc m /\ f Fn m ) )
14 bnj170 
 |-  ( ( f Fn m /\ ph' /\ ps' ) <-> ( ( ph' /\ ps' ) /\ f Fn m ) )
15 4 14 bitri 
 |-  ( ta <-> ( ( ph' /\ ps' ) /\ f Fn m ) )
16 3anan32 
 |-  ( ( m e. _om /\ n = suc m /\ p e. m ) <-> ( ( m e. _om /\ p e. m ) /\ n = suc m ) )
17 5 16 bitri 
 |-  ( si <-> ( ( m e. _om /\ p e. m ) /\ n = suc m ) )
18 15 17 anbi12i 
 |-  ( ( ta /\ si ) <-> ( ( ( ph' /\ ps' ) /\ f Fn m ) /\ ( ( m e. _om /\ p e. m ) /\ n = suc m ) ) )
19 11 13 18 3bitr4ri 
 |-  ( ( ta /\ si ) <-> ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) )
20 19 anbi2i 
 |-  ( ( R _FrSe A /\ ( ta /\ si ) ) <-> ( R _FrSe A /\ ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) ) )
21 3anass 
 |-  ( ( R _FrSe A /\ ta /\ si ) <-> ( R _FrSe A /\ ( ta /\ si ) ) )
22 bnj252 
 |-  ( ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) <-> ( R _FrSe A /\ ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) ) )
23 20 21 22 3bitr4i 
 |-  ( ( R _FrSe A /\ ta /\ si ) <-> ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) )
24 df-suc 
 |-  suc m = ( m u. { m } )
25 24 eqeq2i 
 |-  ( n = suc m <-> n = ( m u. { m } ) )
26 25 3anbi2i 
 |-  ( ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) <-> ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = ( m u. { m } ) /\ f Fn m ) )
27 26 anbi2i 
 |-  ( ( R _FrSe A /\ ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) ) <-> ( R _FrSe A /\ ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = ( m u. { m } ) /\ f Fn m ) ) )
28 bnj252 
 |-  ( ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = ( m u. { m } ) /\ f Fn m ) <-> ( R _FrSe A /\ ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = ( m u. { m } ) /\ f Fn m ) ) )
29 27 22 28 3bitr4i 
 |-  ( ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) <-> ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = ( m u. { m } ) /\ f Fn m ) )
30 biid 
 |-  ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) <-> ( ph' /\ ps' /\ m e. _om /\ p e. m ) )
31 1 2 3 30 bnj535 
 |-  ( ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = ( m u. { m } ) /\ f Fn m ) -> G Fn n )
32 29 31 sylbi 
 |-  ( ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) -> G Fn n )
33 23 32 sylbi 
 |-  ( ( R _FrSe A /\ ta /\ si ) -> G Fn n )