| Step |
Hyp |
Ref |
Expression |
| 1 |
|
mopni.1 |
|- J = ( MetOpen ` D ) |
| 2 |
1
|
elmopn |
|- ( D e. ( *Met ` X ) -> ( A e. J <-> ( A C_ X /\ A. y e. A E. x e. ran ( ball ` D ) ( y e. x /\ x C_ A ) ) ) ) |
| 3 |
2
|
simplbda |
|- ( ( D e. ( *Met ` X ) /\ A e. J ) -> A. y e. A E. x e. ran ( ball ` D ) ( y e. x /\ x C_ A ) ) |
| 4 |
|
eleq1 |
|- ( y = P -> ( y e. x <-> P e. x ) ) |
| 5 |
4
|
anbi1d |
|- ( y = P -> ( ( y e. x /\ x C_ A ) <-> ( P e. x /\ x C_ A ) ) ) |
| 6 |
5
|
rexbidv |
|- ( y = P -> ( E. x e. ran ( ball ` D ) ( y e. x /\ x C_ A ) <-> E. x e. ran ( ball ` D ) ( P e. x /\ x C_ A ) ) ) |
| 7 |
6
|
rspccv |
|- ( A. y e. A E. x e. ran ( ball ` D ) ( y e. x /\ x C_ A ) -> ( P e. A -> E. x e. ran ( ball ` D ) ( P e. x /\ x C_ A ) ) ) |
| 8 |
3 7
|
syl |
|- ( ( D e. ( *Met ` X ) /\ A e. J ) -> ( P e. A -> E. x e. ran ( ball ` D ) ( P e. x /\ x C_ A ) ) ) |
| 9 |
8
|
3impia |
|- ( ( D e. ( *Met ` X ) /\ A e. J /\ P e. A ) -> E. x e. ran ( ball ` D ) ( P e. x /\ x C_ A ) ) |