This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj1015

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 bnj1015.1 
|- ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
bnj1015.2 
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj1015.13 
|- D = ( _om \ { (/) } )
bnj1015.14 
|- B = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
bnj1015.15 
|- G e. V
bnj1015.16 
|- J e. V
Assertion bnj1015 
|- ( ( G e. B /\ J e. dom G ) -> ( G ` J ) C_ _trCl ( X , A , R ) )

Proof

Step Hyp Ref Expression
1 bnj1015.1 
 |-  ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
2 bnj1015.2 
 |-  ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
3 bnj1015.13 
 |-  D = ( _om \ { (/) } )
4 bnj1015.14 
 |-  B = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
5 bnj1015.15 
 |-  G e. V
6 bnj1015.16 
 |-  J e. V
7 6 elexi 
 |-  J e. _V
8 eleq1 
 |-  ( j = J -> ( j e. dom G <-> J e. dom G ) )
9 8 anbi2d 
 |-  ( j = J -> ( ( G e. B /\ j e. dom G ) <-> ( G e. B /\ J e. dom G ) ) )
10 fveq2 
 |-  ( j = J -> ( G ` j ) = ( G ` J ) )
11 10 sseq1d 
 |-  ( j = J -> ( ( G ` j ) C_ _trCl ( X , A , R ) <-> ( G ` J ) C_ _trCl ( X , A , R ) ) )
12 9 11 imbi12d 
 |-  ( j = J -> ( ( ( G e. B /\ j e. dom G ) -> ( G ` j ) C_ _trCl ( X , A , R ) ) <-> ( ( G e. B /\ J e. dom G ) -> ( G ` J ) C_ _trCl ( X , A , R ) ) ) )
13 5 elexi 
 |-  G e. _V
14 eleq1 
 |-  ( g = G -> ( g e. B <-> G e. B ) )
15 dmeq 
 |-  ( g = G -> dom g = dom G )
16 15 eleq2d 
 |-  ( g = G -> ( j e. dom g <-> j e. dom G ) )
17 14 16 anbi12d 
 |-  ( g = G -> ( ( g e. B /\ j e. dom g ) <-> ( G e. B /\ j e. dom G ) ) )
18 fveq1 
 |-  ( g = G -> ( g ` j ) = ( G ` j ) )
19 18 sseq1d 
 |-  ( g = G -> ( ( g ` j ) C_ _trCl ( X , A , R ) <-> ( G ` j ) C_ _trCl ( X , A , R ) ) )
20 17 19 imbi12d 
 |-  ( g = G -> ( ( ( g e. B /\ j e. dom g ) -> ( g ` j ) C_ _trCl ( X , A , R ) ) <-> ( ( G e. B /\ j e. dom G ) -> ( G ` j ) C_ _trCl ( X , A , R ) ) ) )
21 1 2 3 4 bnj1014 
 |-  ( ( g e. B /\ j e. dom g ) -> ( g ` j ) C_ _trCl ( X , A , R ) )
22 13 20 21 vtocl 
 |-  ( ( G e. B /\ j e. dom G ) -> ( G ` j ) C_ _trCl ( X , A , R ) )
23 7 12 22 vtocl 
 |-  ( ( G e. B /\ J e. dom G ) -> ( G ` J ) C_ _trCl ( X , A , R ) )