Metamath Proof Explorer

Theorem bnj571

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 bnj571.3 
|- D = ( _om \ { (/) } )
bnj571.16 
|- G = ( f u. { <. m , U_ y e. ( f ` p ) _pred ( y , A , R ) >. } )
bnj571.17 
|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) )
bnj571.18 
|- ( si <-> ( m e. D /\ n = suc m /\ p e. m ) )
bnj571.19 
|- ( et <-> ( m e. D /\ n = suc m /\ p e. _om /\ m = suc p ) )
bnj571.20 
|- ( ze <-> ( i e. _om /\ suc i e. n /\ m = suc i ) )
bnj571.22 
|- B = U_ y e. ( f ` i ) _pred ( y , A , R )
bnj571.23 
|- C = U_ y e. ( f ` p ) _pred ( y , A , R )
bnj571.24 
|- K = U_ y e. ( G ` i ) _pred ( y , A , R )
bnj571.25 
|- L = U_ y e. ( G ` p ) _pred ( y , A , R )
bnj571.26 
|- G = ( f u. { <. m , C >. } )
bnj571.29 
|- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) )
bnj571.30 
|- ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj571.38 
|- ( ( R _FrSe A /\ ta /\ si ) -> G Fn n )
bnj571.21 
|- ( rh <-> ( i e. _om /\ suc i e. n /\ m =/= suc i ) )
bnj571.40 
|- ( ( R _FrSe A /\ ta /\ et ) -> G Fn n )
bnj571.33 
|- ( ps" <-> A. i e. _om ( suc i e. n -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) )
Assertion bnj571 
|- ( ( R _FrSe A /\ ta /\ et ) -> ps" )

Proof

Step Hyp Ref Expression
1 bnj571.3 
 |-  D = ( _om \ { (/) } )
2 bnj571.16 
 |-  G = ( f u. { <. m , U_ y e. ( f ` p ) _pred ( y , A , R ) >. } )
3 bnj571.17 
 |-  ( ta <-> ( f Fn m /\ ph' /\ ps' ) )
4 bnj571.18 
 |-  ( si <-> ( m e. D /\ n = suc m /\ p e. m ) )
5 bnj571.19 
 |-  ( et <-> ( m e. D /\ n = suc m /\ p e. _om /\ m = suc p ) )
6 bnj571.20 
 |-  ( ze <-> ( i e. _om /\ suc i e. n /\ m = suc i ) )
7 bnj571.22 
 |-  B = U_ y e. ( f ` i ) _pred ( y , A , R )
8 bnj571.23 
 |-  C = U_ y e. ( f ` p ) _pred ( y , A , R )
9 bnj571.24 
 |-  K = U_ y e. ( G ` i ) _pred ( y , A , R )
10 bnj571.25 
 |-  L = U_ y e. ( G ` p ) _pred ( y , A , R )
11 bnj571.26 
 |-  G = ( f u. { <. m , C >. } )
12 bnj571.29 
 |-  ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) )
13 bnj571.30 
 |-  ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
14 bnj571.38 
 |-  ( ( R _FrSe A /\ ta /\ si ) -> G Fn n )
15 bnj571.21 
 |-  ( rh <-> ( i e. _om /\ suc i e. n /\ m =/= suc i ) )
16 bnj571.40 
 |-  ( ( R _FrSe A /\ ta /\ et ) -> G Fn n )
17 bnj571.33 
 |-  ( ps" <-> A. i e. _om ( suc i e. n -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) )
18 nfv 
 |-  F/ i R _FrSe A
19 nfv 
 |-  F/ i f Fn m
20 nfv 
 |-  F/ i ph'
21 nfra1 
 |-  F/ i A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) )
22 13 21 nfxfr 
 |-  F/ i ps'
23 19 20 22 nf3an 
 |-  F/ i ( f Fn m /\ ph' /\ ps' )
24 3 23 nfxfr 
 |-  F/ i ta
25 nfv 
 |-  F/ i et
26 18 24 25 nf3an 
 |-  F/ i ( R _FrSe A /\ ta /\ et )
27 df-bnj17 
 |-  ( ( R _FrSe A /\ ta /\ et /\ ze ) <-> ( ( R _FrSe A /\ ta /\ et ) /\ ze ) )
28 3anass 
 |-  ( ( ( R _FrSe A /\ ta /\ et ) /\ ( i e. _om /\ suc i e. n ) /\ m = suc i ) <-> ( ( R _FrSe A /\ ta /\ et ) /\ ( ( i e. _om /\ suc i e. n ) /\ m = suc i ) ) )
29 3anrot 
 |-  ( ( m = suc i /\ ( R _FrSe A /\ ta /\ et ) /\ ( i e. _om /\ suc i e. n ) ) <-> ( ( R _FrSe A /\ ta /\ et ) /\ ( i e. _om /\ suc i e. n ) /\ m = suc i ) )
30 df-3an 
 |-  ( ( i e. _om /\ suc i e. n /\ m = suc i ) <-> ( ( i e. _om /\ suc i e. n ) /\ m = suc i ) )
31 6 30 bitri 
 |-  ( ze <-> ( ( i e. _om /\ suc i e. n ) /\ m = suc i ) )
32 31 anbi2i 
 |-  ( ( ( R _FrSe A /\ ta /\ et ) /\ ze ) <-> ( ( R _FrSe A /\ ta /\ et ) /\ ( ( i e. _om /\ suc i e. n ) /\ m = suc i ) ) )
33 28 29 32 3bitr4ri 
 |-  ( ( ( R _FrSe A /\ ta /\ et ) /\ ze ) <-> ( m = suc i /\ ( R _FrSe A /\ ta /\ et ) /\ ( i e. _om /\ suc i e. n ) ) )
34 27 33 bitri 
 |-  ( ( R _FrSe A /\ ta /\ et /\ ze ) <-> ( m = suc i /\ ( R _FrSe A /\ ta /\ et ) /\ ( i e. _om /\ suc i e. n ) ) )
35 1 2 3 4 5 6 7 8 9 10 11 12 13 14 bnj558 
 |-  ( ( R _FrSe A /\ ta /\ et /\ ze ) -> ( G ` suc i ) = K )
36 34 35 sylbir 
 |-  ( ( m = suc i /\ ( R _FrSe A /\ ta /\ et ) /\ ( i e. _om /\ suc i e. n ) ) -> ( G ` suc i ) = K )
37 36 3expib 
 |-  ( m = suc i -> ( ( ( R _FrSe A /\ ta /\ et ) /\ ( i e. _om /\ suc i e. n ) ) -> ( G ` suc i ) = K ) )
38 df-bnj17 
 |-  ( ( R _FrSe A /\ ta /\ et /\ rh ) <-> ( ( R _FrSe A /\ ta /\ et ) /\ rh ) )
39 3anass 
 |-  ( ( ( R _FrSe A /\ ta /\ et ) /\ ( i e. _om /\ suc i e. n ) /\ m =/= suc i ) <-> ( ( R _FrSe A /\ ta /\ et ) /\ ( ( i e. _om /\ suc i e. n ) /\ m =/= suc i ) ) )
40 3anrot 
 |-  ( ( m =/= suc i /\ ( R _FrSe A /\ ta /\ et ) /\ ( i e. _om /\ suc i e. n ) ) <-> ( ( R _FrSe A /\ ta /\ et ) /\ ( i e. _om /\ suc i e. n ) /\ m =/= suc i ) )
41 df-3an 
 |-  ( ( i e. _om /\ suc i e. n /\ m =/= suc i ) <-> ( ( i e. _om /\ suc i e. n ) /\ m =/= suc i ) )
42 15 41 bitri 
 |-  ( rh <-> ( ( i e. _om /\ suc i e. n ) /\ m =/= suc i ) )
43 42 anbi2i 
 |-  ( ( ( R _FrSe A /\ ta /\ et ) /\ rh ) <-> ( ( R _FrSe A /\ ta /\ et ) /\ ( ( i e. _om /\ suc i e. n ) /\ m =/= suc i ) ) )
44 39 40 43 3bitr4ri 
 |-  ( ( ( R _FrSe A /\ ta /\ et ) /\ rh ) <-> ( m =/= suc i /\ ( R _FrSe A /\ ta /\ et ) /\ ( i e. _om /\ suc i e. n ) ) )
45 38 44 bitri 
 |-  ( ( R _FrSe A /\ ta /\ et /\ rh ) <-> ( m =/= suc i /\ ( R _FrSe A /\ ta /\ et ) /\ ( i e. _om /\ suc i e. n ) ) )
46 1 3 5 15 9 2 16 13 bnj570 
 |-  ( ( R _FrSe A /\ ta /\ et /\ rh ) -> ( G ` suc i ) = K )
47 45 46 sylbir 
 |-  ( ( m =/= suc i /\ ( R _FrSe A /\ ta /\ et ) /\ ( i e. _om /\ suc i e. n ) ) -> ( G ` suc i ) = K )
48 47 3expib 
 |-  ( m =/= suc i -> ( ( ( R _FrSe A /\ ta /\ et ) /\ ( i e. _om /\ suc i e. n ) ) -> ( G ` suc i ) = K ) )
49 37 48 pm2.61ine 
 |-  ( ( ( R _FrSe A /\ ta /\ et ) /\ ( i e. _om /\ suc i e. n ) ) -> ( G ` suc i ) = K )
50 49 9 eqtrdi 
 |-  ( ( ( R _FrSe A /\ ta /\ et ) /\ ( i e. _om /\ suc i e. n ) ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) )
51 50 exp32 
 |-  ( ( R _FrSe A /\ ta /\ et ) -> ( i e. _om -> ( suc i e. n -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) )
52 26 51 alrimi 
 |-  ( ( R _FrSe A /\ ta /\ et ) -> A. i ( i e. _om -> ( suc i e. n -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) )
53 17 bnj946 
 |-  ( ps" <-> A. i ( i e. _om -> ( suc i e. n -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) )
54 52 53 sylibr 
 |-  ( ( R _FrSe A /\ ta /\ et ) -> ps" )