Theorem bnj1093

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	bnj1093.1	|- E. j ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( f ` i ) C_ B )
	bnj1093.2	|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
	bnj1093.3	|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
Assertion	bnj1093	|- ( ( th /\ ta /\ ch /\ ze ) -> A. i E. j ( ph0 -> ( f ` i ) C_ B ) )

Proof

Step	Hyp	Ref	Expression
1		bnj1093.1	|- E. j ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( f ` i ) C_ B )
2		bnj1093.2	|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
3		bnj1093.3	|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
4	2	bnj1095	|- ( ps -> A. i ps )
5	4 3	bnj1096	|- ( ch -> A. i ch )
6	5	bnj1350	|- ( ( th /\ ta /\ ch ) -> A. i ( th /\ ta /\ ch ) )
7		impexp	|- ( ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( f ` i ) C_ B ) <-> ( ( th /\ ta /\ ch ) -> ( ph0 -> ( f ` i ) C_ B ) ) )
8	7	exbii	|- ( E. j ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( f ` i ) C_ B ) <-> E. j ( ( th /\ ta /\ ch ) -> ( ph0 -> ( f ` i ) C_ B ) ) )
9	1 8	mpbi	|- E. j ( ( th /\ ta /\ ch ) -> ( ph0 -> ( f ` i ) C_ B ) )
10	9	19.37iv	|- ( ( th /\ ta /\ ch ) -> E. j ( ph0 -> ( f ` i ) C_ B ) )
11	6 10	alrimih	|- ( ( th /\ ta /\ ch ) -> A. i E. j ( ph0 -> ( f ` i ) C_ B ) )
12	11	bnj721	|- ( ( th /\ ta /\ ch /\ ze ) -> A. i E. j ( ph0 -> ( f ` i ) C_ B ) )