Metamath Proof Explorer

Theorem bnj545

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

Proof

Step Hyp Ref Expression
1 bnj545.1 
 |-  ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) )
2 bnj545.2 
 |-  D = ( _om \ { (/) } )
3 bnj545.3 
 |-  G = ( f u. { <. m , U_ y e. ( f ` p ) _pred ( y , A , R ) >. } )
4 bnj545.4 
 |-  ( ta <-> ( f Fn m /\ ph' /\ ps' ) )
5 bnj545.5 
 |-  ( si <-> ( m e. D /\ n = suc m /\ p e. m ) )
6 bnj545.6 
 |-  ( ( R _FrSe A /\ ta /\ si ) -> G Fn n )
7 bnj545.7 
 |-  ( ph" <-> ( G ` (/) ) = _pred ( x , A , R ) )
8 4 simp1bi 
 |-  ( ta -> f Fn m )
9 5 simp1bi 
 |-  ( si -> m e. D )
10 8 9 anim12i 
 |-  ( ( ta /\ si ) -> ( f Fn m /\ m e. D ) )
11 10 3adant1 
 |-  ( ( R _FrSe A /\ ta /\ si ) -> ( f Fn m /\ m e. D ) )
12 2 bnj529 
 |-  ( m e. D -> (/) e. m )
13 fndm 
 |-  ( f Fn m -> dom f = m )
14 eleq2 
 |-  ( dom f = m -> ( (/) e. dom f <-> (/) e. m ) )
15 14 biimparc 
 |-  ( ( (/) e. m /\ dom f = m ) -> (/) e. dom f )
16 12 13 15 syl2anr 
 |-  ( ( f Fn m /\ m e. D ) -> (/) e. dom f )
17 11 16 syl 
 |-  ( ( R _FrSe A /\ ta /\ si ) -> (/) e. dom f )
18 6 fnfund 
 |-  ( ( R _FrSe A /\ ta /\ si ) -> Fun G )
19 17 18 jca 
 |-  ( ( R _FrSe A /\ ta /\ si ) -> ( (/) e. dom f /\ Fun G ) )
20 3 bnj931 
 |-  f C_ G
21 19 20 jctil 
 |-  ( ( R _FrSe A /\ ta /\ si ) -> ( f C_ G /\ ( (/) e. dom f /\ Fun G ) ) )
22 df-3an 
 |-  ( ( (/) e. dom f /\ Fun G /\ f C_ G ) <-> ( ( (/) e. dom f /\ Fun G ) /\ f C_ G ) )
23 3anrot 
 |-  ( ( (/) e. dom f /\ Fun G /\ f C_ G ) <-> ( Fun G /\ f C_ G /\ (/) e. dom f ) )
24 ancom 
 |-  ( ( ( (/) e. dom f /\ Fun G ) /\ f C_ G ) <-> ( f C_ G /\ ( (/) e. dom f /\ Fun G ) ) )
25 22 23 24 3bitr3i 
 |-  ( ( Fun G /\ f C_ G /\ (/) e. dom f ) <-> ( f C_ G /\ ( (/) e. dom f /\ Fun G ) ) )
26 21 25 sylibr 
 |-  ( ( R _FrSe A /\ ta /\ si ) -> ( Fun G /\ f C_ G /\ (/) e. dom f ) )
27 funssfv 
 |-  ( ( Fun G /\ f C_ G /\ (/) e. dom f ) -> ( G ` (/) ) = ( f ` (/) ) )
28 26 27 syl 
 |-  ( ( R _FrSe A /\ ta /\ si ) -> ( G ` (/) ) = ( f ` (/) ) )
29 4 simp2bi 
 |-  ( ta -> ph' )
30 29 3ad2ant2 
 |-  ( ( R _FrSe A /\ ta /\ si ) -> ph' )
31 eqtr 
 |-  ( ( ( G ` (/) ) = ( f ` (/) ) /\ ( f ` (/) ) = _pred ( x , A , R ) ) -> ( G ` (/) ) = _pred ( x , A , R ) )
32 1 31 sylan2b 
 |-  ( ( ( G ` (/) ) = ( f ` (/) ) /\ ph' ) -> ( G ` (/) ) = _pred ( x , A , R ) )
33 32 7 sylibr 
 |-  ( ( ( G ` (/) ) = ( f ` (/) ) /\ ph' ) -> ph" )
34 28 30 33 syl2anc 
 |-  ( ( R _FrSe A /\ ta /\ si ) -> ph" )