Metamath Proof Explorer

Theorem bnj535

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

Proof

Step Hyp Ref Expression
1 bnj535.1 
 |-  ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) )
2 bnj535.2 
 |-  ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
3 bnj535.3 
 |-  G = ( f u. { <. m , U_ y e. ( f ` p ) _pred ( y , A , R ) >. } )
4 bnj535.4 
 |-  ( ta <-> ( ph' /\ ps' /\ m e. _om /\ p e. m ) )
5 bnj422 
 |-  ( ( R _FrSe A /\ ta /\ n = ( m u. { m } ) /\ f Fn m ) <-> ( n = ( m u. { m } ) /\ f Fn m /\ R _FrSe A /\ ta ) )
6 bnj251 
 |-  ( ( n = ( m u. { m } ) /\ f Fn m /\ R _FrSe A /\ ta ) <-> ( n = ( m u. { m } ) /\ ( f Fn m /\ ( R _FrSe A /\ ta ) ) ) )
7 5 6 bitri 
 |-  ( ( R _FrSe A /\ ta /\ n = ( m u. { m } ) /\ f Fn m ) <-> ( n = ( m u. { m } ) /\ ( f Fn m /\ ( R _FrSe A /\ ta ) ) ) )
8 fvex 
 |-  ( f ` p ) e. _V
9 1 2 4 bnj518 
 |-  ( ( R _FrSe A /\ ta ) -> A. y e. ( f ` p ) _pred ( y , A , R ) e. _V )
10 iunexg 
 |-  ( ( ( f ` p ) e. _V /\ A. y e. ( f ` p ) _pred ( y , A , R ) e. _V ) -> U_ y e. ( f ` p ) _pred ( y , A , R ) e. _V )
11 8 9 10 sylancr 
 |-  ( ( R _FrSe A /\ ta ) -> U_ y e. ( f ` p ) _pred ( y , A , R ) e. _V )
12 vex 
 |-  m e. _V
13 12 bnj519 
 |-  ( U_ y e. ( f ` p ) _pred ( y , A , R ) e. _V -> Fun { <. m , U_ y e. ( f ` p ) _pred ( y , A , R ) >. } )
14 11 13 syl 
 |-  ( ( R _FrSe A /\ ta ) -> Fun { <. m , U_ y e. ( f ` p ) _pred ( y , A , R ) >. } )
15 dmsnopg 
 |-  ( U_ y e. ( f ` p ) _pred ( y , A , R ) e. _V -> dom { <. m , U_ y e. ( f ` p ) _pred ( y , A , R ) >. } = { m } )
16 11 15 syl 
 |-  ( ( R _FrSe A /\ ta ) -> dom { <. m , U_ y e. ( f ` p ) _pred ( y , A , R ) >. } = { m } )
17 14 16 bnj1422 
 |-  ( ( R _FrSe A /\ ta ) -> { <. m , U_ y e. ( f ` p ) _pred ( y , A , R ) >. } Fn { m } )
18 disjcsn 
 |-  ( m i^i { m } ) = (/)
19 fnun 
 |-  ( ( ( f Fn m /\ { <. m , U_ y e. ( f ` p ) _pred ( y , A , R ) >. } Fn { m } ) /\ ( m i^i { m } ) = (/) ) -> ( f u. { <. m , U_ y e. ( f ` p ) _pred ( y , A , R ) >. } ) Fn ( m u. { m } ) )
20 18 19 mpan2 
 |-  ( ( f Fn m /\ { <. m , U_ y e. ( f ` p ) _pred ( y , A , R ) >. } Fn { m } ) -> ( f u. { <. m , U_ y e. ( f ` p ) _pred ( y , A , R ) >. } ) Fn ( m u. { m } ) )
21 17 20 sylan2 
 |-  ( ( f Fn m /\ ( R _FrSe A /\ ta ) ) -> ( f u. { <. m , U_ y e. ( f ` p ) _pred ( y , A , R ) >. } ) Fn ( m u. { m } ) )
22 3 fneq1i 
 |-  ( G Fn ( m u. { m } ) <-> ( f u. { <. m , U_ y e. ( f ` p ) _pred ( y , A , R ) >. } ) Fn ( m u. { m } ) )
23 21 22 sylibr 
 |-  ( ( f Fn m /\ ( R _FrSe A /\ ta ) ) -> G Fn ( m u. { m } ) )
24 fneq2 
 |-  ( n = ( m u. { m } ) -> ( G Fn n <-> G Fn ( m u. { m } ) ) )
25 23 24 imbitrrid 
 |-  ( n = ( m u. { m } ) -> ( ( f Fn m /\ ( R _FrSe A /\ ta ) ) -> G Fn n ) )
26 25 imp 
 |-  ( ( n = ( m u. { m } ) /\ ( f Fn m /\ ( R _FrSe A /\ ta ) ) ) -> G Fn n )
27 7 26 sylbi 
 |-  ( ( R _FrSe A /\ ta /\ n = ( m u. { m } ) /\ f Fn m ) -> G Fn n )