Metamath Proof Explorer

Theorem bnj945

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
Hypothesis bnj945.1 
|- G = ( f u. { <. n , C >. } )
Assertion bnj945 
|- ( ( C e. _V /\ f Fn n /\ p = suc n /\ A e. n ) -> ( G ` A ) = ( f ` A ) )

Proof

Step Hyp Ref Expression
1 bnj945.1 
 |-  G = ( f u. { <. n , C >. } )
2 fndm 
 |-  ( f Fn n -> dom f = n )
3 2 ad2antll 
 |-  ( ( C e. _V /\ ( p = suc n /\ f Fn n ) ) -> dom f = n )
4 3 eleq2d 
 |-  ( ( C e. _V /\ ( p = suc n /\ f Fn n ) ) -> ( A e. dom f <-> A e. n ) )
5 4 pm5.32i 
 |-  ( ( ( C e. _V /\ ( p = suc n /\ f Fn n ) ) /\ A e. dom f ) <-> ( ( C e. _V /\ ( p = suc n /\ f Fn n ) ) /\ A e. n ) )
6 1 bnj941 
 |-  ( C e. _V -> ( ( p = suc n /\ f Fn n ) -> G Fn p ) )
7 6 imp 
 |-  ( ( C e. _V /\ ( p = suc n /\ f Fn n ) ) -> G Fn p )
8 7 fnfund 
 |-  ( ( C e. _V /\ ( p = suc n /\ f Fn n ) ) -> Fun G )
9 1 bnj931 
 |-  f C_ G
10 8 9 jctir 
 |-  ( ( C e. _V /\ ( p = suc n /\ f Fn n ) ) -> ( Fun G /\ f C_ G ) )
11 10 anim1i 
 |-  ( ( ( C e. _V /\ ( p = suc n /\ f Fn n ) ) /\ A e. dom f ) -> ( ( Fun G /\ f C_ G ) /\ A e. dom f ) )
12 5 11 sylbir 
 |-  ( ( ( C e. _V /\ ( p = suc n /\ f Fn n ) ) /\ A e. n ) -> ( ( Fun G /\ f C_ G ) /\ A e. dom f ) )
13 df-bnj17 
 |-  ( ( C e. _V /\ f Fn n /\ p = suc n /\ A e. n ) <-> ( ( C e. _V /\ f Fn n /\ p = suc n ) /\ A e. n ) )
14 3ancomb 
 |-  ( ( C e. _V /\ f Fn n /\ p = suc n ) <-> ( C e. _V /\ p = suc n /\ f Fn n ) )
15 3anass 
 |-  ( ( C e. _V /\ p = suc n /\ f Fn n ) <-> ( C e. _V /\ ( p = suc n /\ f Fn n ) ) )
16 14 15 bitri 
 |-  ( ( C e. _V /\ f Fn n /\ p = suc n ) <-> ( C e. _V /\ ( p = suc n /\ f Fn n ) ) )
17 16 anbi1i 
 |-  ( ( ( C e. _V /\ f Fn n /\ p = suc n ) /\ A e. n ) <-> ( ( C e. _V /\ ( p = suc n /\ f Fn n ) ) /\ A e. n ) )
18 13 17 bitri 
 |-  ( ( C e. _V /\ f Fn n /\ p = suc n /\ A e. n ) <-> ( ( C e. _V /\ ( p = suc n /\ f Fn n ) ) /\ A e. n ) )
19 df-3an 
 |-  ( ( Fun G /\ f C_ G /\ A e. dom f ) <-> ( ( Fun G /\ f C_ G ) /\ A e. dom f ) )
20 12 18 19 3imtr4i 
 |-  ( ( C e. _V /\ f Fn n /\ p = suc n /\ A e. n ) -> ( Fun G /\ f C_ G /\ A e. dom f ) )
21 funssfv 
 |-  ( ( Fun G /\ f C_ G /\ A e. dom f ) -> ( G ` A ) = ( f ` A ) )
22 20 21 syl 
 |-  ( ( C e. _V /\ f Fn n /\ p = suc n /\ A e. n ) -> ( G ` A ) = ( f ` A ) )