Theorem bnj1133

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	bnj1133.3	|- D = ( _om \ { (/) } )
	bnj1133.5	|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
	bnj1133.7	|- ( ta <-> A. j e. n ( j _E i -> [. j / i ]. th ) )
	bnj1133.8	|- ( ( i e. n /\ ta ) -> th )
Assertion	bnj1133	|- ( ch -> A. i e. n th )

Proof

Step	Hyp	Ref	Expression
1		bnj1133.3	|- D = ( _om \ { (/) } )
2		bnj1133.5	|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
3		bnj1133.7	|- ( ta <-> A. j e. n ( j _E i -> [. j / i ]. th ) )
4		bnj1133.8	|- ( ( i e. n /\ ta ) -> th )
5	1	bnj1071	|- ( n e. D -> _E Fr n )
6	2 5	bnj769	|- ( ch -> _E Fr n )
7		impexp	|- ( ( ( i e. n /\ ta ) -> th ) <-> ( i e. n -> ( ta -> th ) ) )
8	7	bicomi	|- ( ( i e. n -> ( ta -> th ) ) <-> ( ( i e. n /\ ta ) -> th ) )
9	8	albii	|- ( A. i ( i e. n -> ( ta -> th ) ) <-> A. i ( ( i e. n /\ ta ) -> th ) )
10	9 4	mpgbir	|- A. i ( i e. n -> ( ta -> th ) )
11		df-ral	|- ( A. i e. n ( ta -> th ) <-> A. i ( i e. n -> ( ta -> th ) ) )
12	10 11	mpbir	|- A. i e. n ( ta -> th )
13		vex	|- n e. _V
14	13 3	bnj110	|- ( ( _E Fr n /\ A. i e. n ( ta -> th ) ) -> A. i e. n th )
15	6 12 14	sylancl	|- ( ch -> A. i e. n th )