Metamath Proof Explorer

Theorem bnj570

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 bnj570.3 
|- D = ( _om \ { (/) } )
bnj570.17 
|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) )
bnj570.19 
|- ( et <-> ( m e. D /\ n = suc m /\ p e. _om /\ m = suc p ) )
bnj570.21 
|- ( rh <-> ( i e. _om /\ suc i e. n /\ m =/= suc i ) )
bnj570.24 
|- K = U_ y e. ( G ` i ) _pred ( y , A , R )
bnj570.26 
|- G = ( f u. { <. m , C >. } )
bnj570.40 
|- ( ( R _FrSe A /\ ta /\ et ) -> G Fn n )
bnj570.30 
|- ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
Assertion bnj570 
|- ( ( R _FrSe A /\ ta /\ et /\ rh ) -> ( G ` suc i ) = K )

Proof

Step Hyp Ref Expression
1 bnj570.3 
 |-  D = ( _om \ { (/) } )
2 bnj570.17 
 |-  ( ta <-> ( f Fn m /\ ph' /\ ps' ) )
3 bnj570.19 
 |-  ( et <-> ( m e. D /\ n = suc m /\ p e. _om /\ m = suc p ) )
4 bnj570.21 
 |-  ( rh <-> ( i e. _om /\ suc i e. n /\ m =/= suc i ) )
5 bnj570.24 
 |-  K = U_ y e. ( G ` i ) _pred ( y , A , R )
6 bnj570.26 
 |-  G = ( f u. { <. m , C >. } )
7 bnj570.40 
 |-  ( ( R _FrSe A /\ ta /\ et ) -> G Fn n )
8 bnj570.30 
 |-  ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
9 bnj251 
 |-  ( ( R _FrSe A /\ ta /\ et /\ rh ) <-> ( R _FrSe A /\ ( ta /\ ( et /\ rh ) ) ) )
10 2 simp3bi 
 |-  ( ta -> ps' )
11 4 simp1bi 
 |-  ( rh -> i e. _om )
12 11 adantl 
 |-  ( ( et /\ rh ) -> i e. _om )
13 3 4 bnj563 
 |-  ( ( et /\ rh ) -> suc i e. m )
14 12 13 jca 
 |-  ( ( et /\ rh ) -> ( i e. _om /\ suc i e. m ) )
15 8 bnj946 
 |-  ( ps' <-> A. i ( i e. _om -> ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) )
16 sp 
 |-  ( A. i ( i e. _om -> ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) -> ( i e. _om -> ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) )
17 15 16 sylbi 
 |-  ( ps' -> ( i e. _om -> ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) )
18 17 imp32 
 |-  ( ( ps' /\ ( i e. _om /\ suc i e. m ) ) -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) )
19 10 14 18 syl2an 
 |-  ( ( ta /\ ( et /\ rh ) ) -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) )
20 9 19 simplbiim 
 |-  ( ( R _FrSe A /\ ta /\ et /\ rh ) -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) )
21 7 fnfund 
 |-  ( ( R _FrSe A /\ ta /\ et ) -> Fun G )
22 21 bnj721 
 |-  ( ( R _FrSe A /\ ta /\ et /\ rh ) -> Fun G )
23 6 bnj931 
 |-  f C_ G
24 23 a1i 
 |-  ( ( R _FrSe A /\ ta /\ et /\ rh ) -> f C_ G )
25 bnj667 
 |-  ( ( R _FrSe A /\ ta /\ et /\ rh ) -> ( ta /\ et /\ rh ) )
26 2 bnj564 
 |-  ( ta -> dom f = m )
27 eleq2 
 |-  ( dom f = m -> ( suc i e. dom f <-> suc i e. m ) )
28 27 biimpar 
 |-  ( ( dom f = m /\ suc i e. m ) -> suc i e. dom f )
29 26 13 28 syl2an 
 |-  ( ( ta /\ ( et /\ rh ) ) -> suc i e. dom f )
30 29 3impb 
 |-  ( ( ta /\ et /\ rh ) -> suc i e. dom f )
31 25 30 syl 
 |-  ( ( R _FrSe A /\ ta /\ et /\ rh ) -> suc i e. dom f )
32 22 24 31 bnj1502 
 |-  ( ( R _FrSe A /\ ta /\ et /\ rh ) -> ( G ` suc i ) = ( f ` suc i ) )
33 2 simp1bi 
 |-  ( ta -> f Fn m )
34 bnj252 
 |-  ( ( m e. D /\ n = suc m /\ p e. _om /\ m = suc p ) <-> ( m e. D /\ ( n = suc m /\ p e. _om /\ m = suc p ) ) )
35 34 simplbi 
 |-  ( ( m e. D /\ n = suc m /\ p e. _om /\ m = suc p ) -> m e. D )
36 3 35 sylbi 
 |-  ( et -> m e. D )
37 eldifi 
 |-  ( m e. ( _om \ { (/) } ) -> m e. _om )
38 37 1 eleq2s 
 |-  ( m e. D -> m e. _om )
39 nnord 
 |-  ( m e. _om -> Ord m )
40 36 38 39 3syl 
 |-  ( et -> Ord m )
41 40 adantr 
 |-  ( ( et /\ rh ) -> Ord m )
42 41 13 jca 
 |-  ( ( et /\ rh ) -> ( Ord m /\ suc i e. m ) )
43 33 42 anim12i 
 |-  ( ( ta /\ ( et /\ rh ) ) -> ( f Fn m /\ ( Ord m /\ suc i e. m ) ) )
44 fndm 
 |-  ( f Fn m -> dom f = m )
45 elelsuc 
 |-  ( suc i e. m -> suc i e. suc m )
46 ordsucelsuc 
 |-  ( Ord m -> ( i e. m <-> suc i e. suc m ) )
47 46 biimpar 
 |-  ( ( Ord m /\ suc i e. suc m ) -> i e. m )
48 45 47 sylan2 
 |-  ( ( Ord m /\ suc i e. m ) -> i e. m )
49 44 48 anim12i 
 |-  ( ( f Fn m /\ ( Ord m /\ suc i e. m ) ) -> ( dom f = m /\ i e. m ) )
50 eleq2 
 |-  ( dom f = m -> ( i e. dom f <-> i e. m ) )
51 50 biimpar 
 |-  ( ( dom f = m /\ i e. m ) -> i e. dom f )
52 43 49 51 3syl 
 |-  ( ( ta /\ ( et /\ rh ) ) -> i e. dom f )
53 52 3impb 
 |-  ( ( ta /\ et /\ rh ) -> i e. dom f )
54 25 53 syl 
 |-  ( ( R _FrSe A /\ ta /\ et /\ rh ) -> i e. dom f )
55 22 24 54 bnj1502 
 |-  ( ( R _FrSe A /\ ta /\ et /\ rh ) -> ( G ` i ) = ( f ` i ) )
56 55 iuneq1d 
 |-  ( ( R _FrSe A /\ ta /\ et /\ rh ) -> U_ y e. ( G ` i ) _pred ( y , A , R ) = U_ y e. ( f ` i ) _pred ( y , A , R ) )
57 20 32 56 3eqtr4d 
 |-  ( ( R _FrSe A /\ ta /\ et /\ rh ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) )
58 57 5 eqtr4di 
 |-  ( ( R _FrSe A /\ ta /\ et /\ rh ) -> ( G ` suc i ) = K )