| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ellimciota.f |
|- ( ph -> F : A --> CC ) |
| 2 |
|
ellimciota.a |
|- ( ph -> A C_ CC ) |
| 3 |
|
ellimciota.b |
|- ( ph -> B e. ( ( limPt ` K ) ` A ) ) |
| 4 |
|
ellimciota.4 |
|- ( ph -> ( F limCC B ) =/= (/) ) |
| 5 |
|
ellimciota.k |
|- K = ( TopOpen ` CCfld ) |
| 6 |
|
eleq1 |
|- ( x = y -> ( x e. ( F limCC B ) <-> y e. ( F limCC B ) ) ) |
| 7 |
6
|
cbviotavw |
|- ( iota x x e. ( F limCC B ) ) = ( iota y y e. ( F limCC B ) ) |
| 8 |
|
iotaex |
|- ( iota y y e. ( F limCC B ) ) e. _V |
| 9 |
|
n0 |
|- ( ( F limCC B ) =/= (/) <-> E. x x e. ( F limCC B ) ) |
| 10 |
4 9
|
sylib |
|- ( ph -> E. x x e. ( F limCC B ) ) |
| 11 |
1 2 3 5
|
limcmo |
|- ( ph -> E* x x e. ( F limCC B ) ) |
| 12 |
|
df-eu |
|- ( E! x x e. ( F limCC B ) <-> ( E. x x e. ( F limCC B ) /\ E* x x e. ( F limCC B ) ) ) |
| 13 |
10 11 12
|
sylanbrc |
|- ( ph -> E! x x e. ( F limCC B ) ) |
| 14 |
|
eleq1 |
|- ( x = ( iota y y e. ( F limCC B ) ) -> ( x e. ( F limCC B ) <-> ( iota y y e. ( F limCC B ) ) e. ( F limCC B ) ) ) |
| 15 |
14
|
iota2 |
|- ( ( ( iota y y e. ( F limCC B ) ) e. _V /\ E! x x e. ( F limCC B ) ) -> ( ( iota y y e. ( F limCC B ) ) e. ( F limCC B ) <-> ( iota x x e. ( F limCC B ) ) = ( iota y y e. ( F limCC B ) ) ) ) |
| 16 |
8 13 15
|
sylancr |
|- ( ph -> ( ( iota y y e. ( F limCC B ) ) e. ( F limCC B ) <-> ( iota x x e. ( F limCC B ) ) = ( iota y y e. ( F limCC B ) ) ) ) |
| 17 |
7 16
|
mpbiri |
|- ( ph -> ( iota y y e. ( F limCC B ) ) e. ( F limCC B ) ) |
| 18 |
7 17
|
eqeltrid |
|- ( ph -> ( iota x x e. ( F limCC B ) ) e. ( F limCC B ) ) |