Step |
Hyp |
Ref |
Expression |
1 |
|
hauscmp.1 |
|- X = U. J |
2 |
|
simp2 |
|- ( ( J e. Haus /\ S C_ X /\ ( J |`t S ) e. Comp ) -> S C_ X ) |
3 |
|
eqid |
|- { y e. J | E. w e. J ( x e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) } = { y e. J | E. w e. J ( x e. w /\ ( ( cls ` J ) ` w ) C_ ( X \ y ) ) } |
4 |
|
simpl1 |
|- ( ( ( J e. Haus /\ S C_ X /\ ( J |`t S ) e. Comp ) /\ x e. ( X \ S ) ) -> J e. Haus ) |
5 |
|
simpl2 |
|- ( ( ( J e. Haus /\ S C_ X /\ ( J |`t S ) e. Comp ) /\ x e. ( X \ S ) ) -> S C_ X ) |
6 |
|
simpl3 |
|- ( ( ( J e. Haus /\ S C_ X /\ ( J |`t S ) e. Comp ) /\ x e. ( X \ S ) ) -> ( J |`t S ) e. Comp ) |
7 |
|
simpr |
|- ( ( ( J e. Haus /\ S C_ X /\ ( J |`t S ) e. Comp ) /\ x e. ( X \ S ) ) -> x e. ( X \ S ) ) |
8 |
1 3 4 5 6 7
|
hauscmplem |
|- ( ( ( J e. Haus /\ S C_ X /\ ( J |`t S ) e. Comp ) /\ x e. ( X \ S ) ) -> E. z e. J ( x e. z /\ ( ( cls ` J ) ` z ) C_ ( X \ S ) ) ) |
9 |
|
haustop |
|- ( J e. Haus -> J e. Top ) |
10 |
9
|
3ad2ant1 |
|- ( ( J e. Haus /\ S C_ X /\ ( J |`t S ) e. Comp ) -> J e. Top ) |
11 |
|
elssuni |
|- ( z e. J -> z C_ U. J ) |
12 |
11 1
|
sseqtrrdi |
|- ( z e. J -> z C_ X ) |
13 |
1
|
sscls |
|- ( ( J e. Top /\ z C_ X ) -> z C_ ( ( cls ` J ) ` z ) ) |
14 |
10 12 13
|
syl2an |
|- ( ( ( J e. Haus /\ S C_ X /\ ( J |`t S ) e. Comp ) /\ z e. J ) -> z C_ ( ( cls ` J ) ` z ) ) |
15 |
|
sstr2 |
|- ( z C_ ( ( cls ` J ) ` z ) -> ( ( ( cls ` J ) ` z ) C_ ( X \ S ) -> z C_ ( X \ S ) ) ) |
16 |
14 15
|
syl |
|- ( ( ( J e. Haus /\ S C_ X /\ ( J |`t S ) e. Comp ) /\ z e. J ) -> ( ( ( cls ` J ) ` z ) C_ ( X \ S ) -> z C_ ( X \ S ) ) ) |
17 |
16
|
anim2d |
|- ( ( ( J e. Haus /\ S C_ X /\ ( J |`t S ) e. Comp ) /\ z e. J ) -> ( ( x e. z /\ ( ( cls ` J ) ` z ) C_ ( X \ S ) ) -> ( x e. z /\ z C_ ( X \ S ) ) ) ) |
18 |
17
|
reximdva |
|- ( ( J e. Haus /\ S C_ X /\ ( J |`t S ) e. Comp ) -> ( E. z e. J ( x e. z /\ ( ( cls ` J ) ` z ) C_ ( X \ S ) ) -> E. z e. J ( x e. z /\ z C_ ( X \ S ) ) ) ) |
19 |
18
|
adantr |
|- ( ( ( J e. Haus /\ S C_ X /\ ( J |`t S ) e. Comp ) /\ x e. ( X \ S ) ) -> ( E. z e. J ( x e. z /\ ( ( cls ` J ) ` z ) C_ ( X \ S ) ) -> E. z e. J ( x e. z /\ z C_ ( X \ S ) ) ) ) |
20 |
8 19
|
mpd |
|- ( ( ( J e. Haus /\ S C_ X /\ ( J |`t S ) e. Comp ) /\ x e. ( X \ S ) ) -> E. z e. J ( x e. z /\ z C_ ( X \ S ) ) ) |
21 |
20
|
ralrimiva |
|- ( ( J e. Haus /\ S C_ X /\ ( J |`t S ) e. Comp ) -> A. x e. ( X \ S ) E. z e. J ( x e. z /\ z C_ ( X \ S ) ) ) |
22 |
|
eltop2 |
|- ( J e. Top -> ( ( X \ S ) e. J <-> A. x e. ( X \ S ) E. z e. J ( x e. z /\ z C_ ( X \ S ) ) ) ) |
23 |
10 22
|
syl |
|- ( ( J e. Haus /\ S C_ X /\ ( J |`t S ) e. Comp ) -> ( ( X \ S ) e. J <-> A. x e. ( X \ S ) E. z e. J ( x e. z /\ z C_ ( X \ S ) ) ) ) |
24 |
21 23
|
mpbird |
|- ( ( J e. Haus /\ S C_ X /\ ( J |`t S ) e. Comp ) -> ( X \ S ) e. J ) |
25 |
1
|
iscld |
|- ( J e. Top -> ( S e. ( Clsd ` J ) <-> ( S C_ X /\ ( X \ S ) e. J ) ) ) |
26 |
10 25
|
syl |
|- ( ( J e. Haus /\ S C_ X /\ ( J |`t S ) e. Comp ) -> ( S e. ( Clsd ` J ) <-> ( S C_ X /\ ( X \ S ) e. J ) ) ) |
27 |
2 24 26
|
mpbir2and |
|- ( ( J e. Haus /\ S C_ X /\ ( J |`t S ) e. Comp ) -> S e. ( Clsd ` J ) ) |