Step |
Hyp |
Ref |
Expression |
1 |
|
axprlem4.1 |
|- E. s A. n ph |
2 |
|
axprlem4.2 |
|- ( ph -> ( n e. s -> A. t -. t e. n ) ) |
3 |
|
axprlem4.3 |
|- ( A. n ph -> ( if- ( E. n n e. s , w = x , w = y ) <-> w = v ) ) |
4 |
2
|
alimi |
|- ( A. n ph -> A. n ( n e. s -> A. t -. t e. n ) ) |
5 |
|
df-ral |
|- ( A. n e. s A. t -. t e. n <-> A. n ( n e. s -> A. t -. t e. n ) ) |
6 |
4 5
|
sylibr |
|- ( A. n ph -> A. n e. s A. t -. t e. n ) |
7 |
6
|
imim1i |
|- ( ( A. n e. s A. t -. t e. n -> s e. p ) -> ( A. n ph -> s e. p ) ) |
8 |
7
|
ancrd |
|- ( ( A. n e. s A. t -. t e. n -> s e. p ) -> ( A. n ph -> ( s e. p /\ A. n ph ) ) ) |
9 |
8
|
aleximi |
|- ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) -> ( E. s A. n ph -> E. s ( s e. p /\ A. n ph ) ) ) |
10 |
1 9
|
mpi |
|- ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) -> E. s ( s e. p /\ A. n ph ) ) |
11 |
3
|
biimprcd |
|- ( w = v -> ( A. n ph -> if- ( E. n n e. s , w = x , w = y ) ) ) |
12 |
11
|
anim2d |
|- ( w = v -> ( ( s e. p /\ A. n ph ) -> ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) ) |
13 |
12
|
eximdv |
|- ( w = v -> ( E. s ( s e. p /\ A. n ph ) -> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) ) |
14 |
10 13
|
syl5com |
|- ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) -> ( w = v -> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) ) |