Step |
Hyp |
Ref |
Expression |
1 |
|
nrmtop |
|- ( J e. Nrm -> J e. Top ) |
2 |
1
|
ad2antrr |
|- ( ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) /\ ( x e. J /\ ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) ) -> J e. Top ) |
3 |
|
elssuni |
|- ( x e. J -> x C_ U. J ) |
4 |
3
|
ad2antrl |
|- ( ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) /\ ( x e. J /\ ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) ) -> x C_ U. J ) |
5 |
|
eqid |
|- U. J = U. J |
6 |
5
|
clscld |
|- ( ( J e. Top /\ x C_ U. J ) -> ( ( cls ` J ) ` x ) e. ( Clsd ` J ) ) |
7 |
2 4 6
|
syl2anc |
|- ( ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) /\ ( x e. J /\ ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) ) -> ( ( cls ` J ) ` x ) e. ( Clsd ` J ) ) |
8 |
5
|
cldopn |
|- ( ( ( cls ` J ) ` x ) e. ( Clsd ` J ) -> ( U. J \ ( ( cls ` J ) ` x ) ) e. J ) |
9 |
7 8
|
syl |
|- ( ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) /\ ( x e. J /\ ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) ) -> ( U. J \ ( ( cls ` J ) ` x ) ) e. J ) |
10 |
|
simprrl |
|- ( ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) /\ ( x e. J /\ ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) ) -> C C_ x ) |
11 |
|
incom |
|- ( D i^i ( ( cls ` J ) ` x ) ) = ( ( ( cls ` J ) ` x ) i^i D ) |
12 |
|
simprrr |
|- ( ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) /\ ( x e. J /\ ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) ) -> ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) |
13 |
11 12
|
eqtrid |
|- ( ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) /\ ( x e. J /\ ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) ) -> ( D i^i ( ( cls ` J ) ` x ) ) = (/) ) |
14 |
|
simplr2 |
|- ( ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) /\ ( x e. J /\ ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) ) -> D e. ( Clsd ` J ) ) |
15 |
5
|
cldss |
|- ( D e. ( Clsd ` J ) -> D C_ U. J ) |
16 |
|
reldisj |
|- ( D C_ U. J -> ( ( D i^i ( ( cls ` J ) ` x ) ) = (/) <-> D C_ ( U. J \ ( ( cls ` J ) ` x ) ) ) ) |
17 |
14 15 16
|
3syl |
|- ( ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) /\ ( x e. J /\ ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) ) -> ( ( D i^i ( ( cls ` J ) ` x ) ) = (/) <-> D C_ ( U. J \ ( ( cls ` J ) ` x ) ) ) ) |
18 |
13 17
|
mpbid |
|- ( ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) /\ ( x e. J /\ ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) ) -> D C_ ( U. J \ ( ( cls ` J ) ` x ) ) ) |
19 |
5
|
sscls |
|- ( ( J e. Top /\ x C_ U. J ) -> x C_ ( ( cls ` J ) ` x ) ) |
20 |
2 4 19
|
syl2anc |
|- ( ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) /\ ( x e. J /\ ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) ) -> x C_ ( ( cls ` J ) ` x ) ) |
21 |
20
|
ssrind |
|- ( ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) /\ ( x e. J /\ ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) ) -> ( x i^i ( U. J \ ( ( cls ` J ) ` x ) ) ) C_ ( ( ( cls ` J ) ` x ) i^i ( U. J \ ( ( cls ` J ) ` x ) ) ) ) |
22 |
|
disjdif |
|- ( ( ( cls ` J ) ` x ) i^i ( U. J \ ( ( cls ` J ) ` x ) ) ) = (/) |
23 |
|
sseq0 |
|- ( ( ( x i^i ( U. J \ ( ( cls ` J ) ` x ) ) ) C_ ( ( ( cls ` J ) ` x ) i^i ( U. J \ ( ( cls ` J ) ` x ) ) ) /\ ( ( ( cls ` J ) ` x ) i^i ( U. J \ ( ( cls ` J ) ` x ) ) ) = (/) ) -> ( x i^i ( U. J \ ( ( cls ` J ) ` x ) ) ) = (/) ) |
24 |
21 22 23
|
sylancl |
|- ( ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) /\ ( x e. J /\ ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) ) -> ( x i^i ( U. J \ ( ( cls ` J ) ` x ) ) ) = (/) ) |
25 |
|
sseq2 |
|- ( y = ( U. J \ ( ( cls ` J ) ` x ) ) -> ( D C_ y <-> D C_ ( U. J \ ( ( cls ` J ) ` x ) ) ) ) |
26 |
|
ineq2 |
|- ( y = ( U. J \ ( ( cls ` J ) ` x ) ) -> ( x i^i y ) = ( x i^i ( U. J \ ( ( cls ` J ) ` x ) ) ) ) |
27 |
26
|
eqeq1d |
|- ( y = ( U. J \ ( ( cls ` J ) ` x ) ) -> ( ( x i^i y ) = (/) <-> ( x i^i ( U. J \ ( ( cls ` J ) ` x ) ) ) = (/) ) ) |
28 |
25 27
|
3anbi23d |
|- ( y = ( U. J \ ( ( cls ` J ) ` x ) ) -> ( ( C C_ x /\ D C_ y /\ ( x i^i y ) = (/) ) <-> ( C C_ x /\ D C_ ( U. J \ ( ( cls ` J ) ` x ) ) /\ ( x i^i ( U. J \ ( ( cls ` J ) ` x ) ) ) = (/) ) ) ) |
29 |
28
|
rspcev |
|- ( ( ( U. J \ ( ( cls ` J ) ` x ) ) e. J /\ ( C C_ x /\ D C_ ( U. J \ ( ( cls ` J ) ` x ) ) /\ ( x i^i ( U. J \ ( ( cls ` J ) ` x ) ) ) = (/) ) ) -> E. y e. J ( C C_ x /\ D C_ y /\ ( x i^i y ) = (/) ) ) |
30 |
9 10 18 24 29
|
syl13anc |
|- ( ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) /\ ( x e. J /\ ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) ) -> E. y e. J ( C C_ x /\ D C_ y /\ ( x i^i y ) = (/) ) ) |
31 |
|
nrmsep2 |
|- ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) -> E. x e. J ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) |
32 |
30 31
|
reximddv |
|- ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) -> E. x e. J E. y e. J ( C C_ x /\ D C_ y /\ ( x i^i y ) = (/) ) ) |