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 )