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 ) )