Metamath Proof Explorer

Theorem bnj966

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) (New usage is discouraged.)

Ref Expression
Hypotheses bnj966.3 
|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
bnj966.10 
|- D = ( _om \ { (/) } )
bnj966.12 
|- C = U_ y e. ( f ` m ) _pred ( y , A , R )
bnj966.13 
|- G = ( f u. { <. n , C >. } )
bnj966.44 
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> C e. _V )
bnj966.53 
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> G Fn p )
Assertion bnj966 
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) )

Proof

Step Hyp Ref Expression
1 bnj966.3 
 |-  ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
2 bnj966.10 
 |-  D = ( _om \ { (/) } )
3 bnj966.12 
 |-  C = U_ y e. ( f ` m ) _pred ( y , A , R )
4 bnj966.13 
 |-  G = ( f u. { <. n , C >. } )
5 bnj966.44 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> C e. _V )
6 bnj966.53 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> G Fn p )
7 6 fnfund 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> Fun G )
8 7 3adant3 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> Fun G )
9 opex 
 |-  <. n , C >. e. _V
10 9 snid 
 |-  <. n , C >. e. { <. n , C >. }
11 elun2 
 |-  ( <. n , C >. e. { <. n , C >. } -> <. n , C >. e. ( f u. { <. n , C >. } ) )
12 10 11 ax-mp 
 |-  <. n , C >. e. ( f u. { <. n , C >. } )
13 12 4 eleqtrri 
 |-  <. n , C >. e. G
14 funopfv 
 |-  ( Fun G -> ( <. n , C >. e. G -> ( G ` n ) = C ) )
15 8 13 14 mpisyl 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> ( G ` n ) = C )
16 simp22 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> n = suc m )
17 simp33 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> n = suc i )
18 bnj551 
 |-  ( ( n = suc m /\ n = suc i ) -> m = i )
19 16 17 18 syl2anc 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> m = i )
20 suceq 
 |-  ( m = i -> suc m = suc i )
21 20 eqeq2d 
 |-  ( m = i -> ( n = suc m <-> n = suc i ) )
22 21 biimpac 
 |-  ( ( n = suc m /\ m = i ) -> n = suc i )
23 22 fveq2d 
 |-  ( ( n = suc m /\ m = i ) -> ( G ` n ) = ( G ` suc i ) )
24 fveq2 
 |-  ( m = i -> ( f ` m ) = ( f ` i ) )
25 24 bnj1113 
 |-  ( m = i -> U_ y e. ( f ` m ) _pred ( y , A , R ) = U_ y e. ( f ` i ) _pred ( y , A , R ) )
26 3 25 eqtrid 
 |-  ( m = i -> C = U_ y e. ( f ` i ) _pred ( y , A , R ) )
27 26 adantl 
 |-  ( ( n = suc m /\ m = i ) -> C = U_ y e. ( f ` i ) _pred ( y , A , R ) )
28 23 27 eqeq12d 
 |-  ( ( n = suc m /\ m = i ) -> ( ( G ` n ) = C <-> ( G ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
29 16 19 28 syl2anc 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> ( ( G ` n ) = C <-> ( G ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
30 15 29 mpbid 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> ( G ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) )
31 5 3adant3 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> C e. _V )
32 1 bnj1235 
 |-  ( ch -> f Fn n )
33 32 3ad2ant1 
 |-  ( ( ch /\ n = suc m /\ p = suc n ) -> f Fn n )
34 33 3ad2ant2 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> f Fn n )
35 simp23 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> p = suc n )
36 31 34 35 17 bnj951 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> ( C e. _V /\ f Fn n /\ p = suc n /\ n = suc i ) )
37 2 bnj923 
 |-  ( n e. D -> n e. _om )
38 1 37 bnj769 
 |-  ( ch -> n e. _om )
39 38 3ad2ant1 
 |-  ( ( ch /\ n = suc m /\ p = suc n ) -> n e. _om )
40 simp3 
 |-  ( ( i e. _om /\ suc i e. p /\ n = suc i ) -> n = suc i )
41 39 40 bnj240 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> ( n e. _om /\ n = suc i ) )
42 vex 
 |-  i e. _V
43 42 bnj216 
 |-  ( n = suc i -> i e. n )
44 43 adantl 
 |-  ( ( n e. _om /\ n = suc i ) -> i e. n )
45 41 44 syl 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> i e. n )
46 bnj658 
 |-  ( ( C e. _V /\ f Fn n /\ p = suc n /\ n = suc i ) -> ( C e. _V /\ f Fn n /\ p = suc n ) )
47 46 anim1i 
 |-  ( ( ( C e. _V /\ f Fn n /\ p = suc n /\ n = suc i ) /\ i e. n ) -> ( ( C e. _V /\ f Fn n /\ p = suc n ) /\ i e. n ) )
48 df-bnj17 
 |-  ( ( C e. _V /\ f Fn n /\ p = suc n /\ i e. n ) <-> ( ( C e. _V /\ f Fn n /\ p = suc n ) /\ i e. n ) )
49 47 48 sylibr 
 |-  ( ( ( C e. _V /\ f Fn n /\ p = suc n /\ n = suc i ) /\ i e. n ) -> ( C e. _V /\ f Fn n /\ p = suc n /\ i e. n ) )
50 4 bnj945 
 |-  ( ( C e. _V /\ f Fn n /\ p = suc n /\ i e. n ) -> ( G ` i ) = ( f ` i ) )
51 49 50 syl 
 |-  ( ( ( C e. _V /\ f Fn n /\ p = suc n /\ n = suc i ) /\ i e. n ) -> ( G ` i ) = ( f ` i ) )
52 36 45 51 syl2anc 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> ( G ` i ) = ( f ` i ) )
53 3 4 bnj958 
 |-  ( ( G ` i ) = ( f ` i ) -> A. y ( G ` i ) = ( f ` i ) )
54 53 bnj956 
 |-  ( ( G ` i ) = ( f ` i ) -> U_ y e. ( G ` i ) _pred ( y , A , R ) = U_ y e. ( f ` i ) _pred ( y , A , R ) )
55 54 eqeq2d 
 |-  ( ( G ` i ) = ( f ` i ) -> ( ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) <-> ( G ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
56 52 55 syl 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> ( ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) <-> ( G ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
57 30 56 mpbird 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) )