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

Metamath Proof Explorer

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 )