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