Metamath Proof Explorer

Theorem bnj548

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 bnj548.1 
|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) )
bnj548.2 
|- B = U_ y e. ( f ` i ) _pred ( y , A , R )
bnj548.3 
|- K = U_ y e. ( G ` i ) _pred ( y , A , R )
bnj548.4 
|- G = ( f u. { <. m , C >. } )
bnj548.5 
|- ( ( R _FrSe A /\ ta /\ si ) -> G Fn n )
Assertion bnj548 
|- ( ( ( R _FrSe A /\ ta /\ si ) /\ i e. m ) -> B = K )

Proof

Step Hyp Ref Expression
1 bnj548.1 
 |-  ( ta <-> ( f Fn m /\ ph' /\ ps' ) )
2 bnj548.2 
 |-  B = U_ y e. ( f ` i ) _pred ( y , A , R )
3 bnj548.3 
 |-  K = U_ y e. ( G ` i ) _pred ( y , A , R )
4 bnj548.4 
 |-  G = ( f u. { <. m , C >. } )
5 bnj548.5 
 |-  ( ( R _FrSe A /\ ta /\ si ) -> G Fn n )
6 5 fnfund 
 |-  ( ( R _FrSe A /\ ta /\ si ) -> Fun G )
7 6 adantr 
 |-  ( ( ( R _FrSe A /\ ta /\ si ) /\ i e. m ) -> Fun G )
8 1 simp1bi 
 |-  ( ta -> f Fn m )
9 fndm 
 |-  ( f Fn m -> dom f = m )
10 eleq2 
 |-  ( dom f = m -> ( i e. dom f <-> i e. m ) )
11 10 biimpar 
 |-  ( ( dom f = m /\ i e. m ) -> i e. dom f )
12 9 11 sylan 
 |-  ( ( f Fn m /\ i e. m ) -> i e. dom f )
13 8 12 sylan 
 |-  ( ( ta /\ i e. m ) -> i e. dom f )
14 13 3ad2antl2 
 |-  ( ( ( R _FrSe A /\ ta /\ si ) /\ i e. m ) -> i e. dom f )
15 7 14 jca 
 |-  ( ( ( R _FrSe A /\ ta /\ si ) /\ i e. m ) -> ( Fun G /\ i e. dom f ) )
16 4 bnj931 
 |-  f C_ G
17 15 16 jctil 
 |-  ( ( ( R _FrSe A /\ ta /\ si ) /\ i e. m ) -> ( f C_ G /\ ( Fun G /\ i e. dom f ) ) )
18 3anan12 
 |-  ( ( Fun G /\ f C_ G /\ i e. dom f ) <-> ( f C_ G /\ ( Fun G /\ i e. dom f ) ) )
19 17 18 sylibr 
 |-  ( ( ( R _FrSe A /\ ta /\ si ) /\ i e. m ) -> ( Fun G /\ f C_ G /\ i e. dom f ) )
20 funssfv 
 |-  ( ( Fun G /\ f C_ G /\ i e. dom f ) -> ( G ` i ) = ( f ` i ) )
21 iuneq1 
 |-  ( ( G ` i ) = ( f ` i ) -> U_ y e. ( G ` i ) _pred ( y , A , R ) = U_ y e. ( f ` i ) _pred ( y , A , R ) )
22 21 eqcomd 
 |-  ( ( G ` i ) = ( f ` i ) -> U_ y e. ( f ` i ) _pred ( y , A , R ) = U_ y e. ( G ` i ) _pred ( y , A , R ) )
23 22 2 3 3eqtr4g 
 |-  ( ( G ` i ) = ( f ` i ) -> B = K )
24 19 20 23 3syl 
 |-  ( ( ( R _FrSe A /\ ta /\ si ) /\ i e. m ) -> B = K )