Step |
Hyp |
Ref |
Expression |
1 |
|
topontop |
|- ( J e. ( TopOn ` X ) -> J e. Top ) |
2 |
|
eqid |
|- U. J = U. J |
3 |
2
|
ist1 |
|- ( J e. Fre <-> ( J e. Top /\ A. y e. U. J { y } e. ( Clsd ` J ) ) ) |
4 |
3
|
baib |
|- ( J e. Top -> ( J e. Fre <-> A. y e. U. J { y } e. ( Clsd ` J ) ) ) |
5 |
1 4
|
syl |
|- ( J e. ( TopOn ` X ) -> ( J e. Fre <-> A. y e. U. J { y } e. ( Clsd ` J ) ) ) |
6 |
|
toponuni |
|- ( J e. ( TopOn ` X ) -> X = U. J ) |
7 |
6
|
raleqdv |
|- ( J e. ( TopOn ` X ) -> ( A. y e. X { y } e. ( Clsd ` J ) <-> A. y e. U. J { y } e. ( Clsd ` J ) ) ) |
8 |
1
|
adantr |
|- ( ( J e. ( TopOn ` X ) /\ y e. X ) -> J e. Top ) |
9 |
|
eltop2 |
|- ( J e. Top -> ( ( U. J \ { y } ) e. J <-> A. x e. ( U. J \ { y } ) E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) ) |
10 |
8 9
|
syl |
|- ( ( J e. ( TopOn ` X ) /\ y e. X ) -> ( ( U. J \ { y } ) e. J <-> A. x e. ( U. J \ { y } ) E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) ) |
11 |
6
|
eleq2d |
|- ( J e. ( TopOn ` X ) -> ( y e. X <-> y e. U. J ) ) |
12 |
11
|
biimpa |
|- ( ( J e. ( TopOn ` X ) /\ y e. X ) -> y e. U. J ) |
13 |
12
|
snssd |
|- ( ( J e. ( TopOn ` X ) /\ y e. X ) -> { y } C_ U. J ) |
14 |
2
|
iscld2 |
|- ( ( J e. Top /\ { y } C_ U. J ) -> ( { y } e. ( Clsd ` J ) <-> ( U. J \ { y } ) e. J ) ) |
15 |
8 13 14
|
syl2anc |
|- ( ( J e. ( TopOn ` X ) /\ y e. X ) -> ( { y } e. ( Clsd ` J ) <-> ( U. J \ { y } ) e. J ) ) |
16 |
6
|
adantr |
|- ( ( J e. ( TopOn ` X ) /\ y e. X ) -> X = U. J ) |
17 |
16
|
eleq2d |
|- ( ( J e. ( TopOn ` X ) /\ y e. X ) -> ( x e. X <-> x e. U. J ) ) |
18 |
17
|
imbi1d |
|- ( ( J e. ( TopOn ` X ) /\ y e. X ) -> ( ( x e. X -> ( x =/= y -> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) ) <-> ( x e. U. J -> ( x =/= y -> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) ) ) ) |
19 |
|
con1b |
|- ( ( -. x = y -> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) <-> ( -. E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) -> x = y ) ) |
20 |
|
df-ne |
|- ( x =/= y <-> -. x = y ) |
21 |
20
|
imbi1i |
|- ( ( x =/= y -> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) <-> ( -. x = y -> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) ) |
22 |
|
disjsn |
|- ( ( o i^i { y } ) = (/) <-> -. y e. o ) |
23 |
|
elssuni |
|- ( o e. J -> o C_ U. J ) |
24 |
|
reldisj |
|- ( o C_ U. J -> ( ( o i^i { y } ) = (/) <-> o C_ ( U. J \ { y } ) ) ) |
25 |
23 24
|
syl |
|- ( o e. J -> ( ( o i^i { y } ) = (/) <-> o C_ ( U. J \ { y } ) ) ) |
26 |
22 25
|
bitr3id |
|- ( o e. J -> ( -. y e. o <-> o C_ ( U. J \ { y } ) ) ) |
27 |
26
|
anbi2d |
|- ( o e. J -> ( ( x e. o /\ -. y e. o ) <-> ( x e. o /\ o C_ ( U. J \ { y } ) ) ) ) |
28 |
27
|
rexbiia |
|- ( E. o e. J ( x e. o /\ -. y e. o ) <-> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) |
29 |
|
rexanali |
|- ( E. o e. J ( x e. o /\ -. y e. o ) <-> -. A. o e. J ( x e. o -> y e. o ) ) |
30 |
28 29
|
bitr3i |
|- ( E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) <-> -. A. o e. J ( x e. o -> y e. o ) ) |
31 |
30
|
con2bii |
|- ( A. o e. J ( x e. o -> y e. o ) <-> -. E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) |
32 |
31
|
imbi1i |
|- ( ( A. o e. J ( x e. o -> y e. o ) -> x = y ) <-> ( -. E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) -> x = y ) ) |
33 |
19 21 32
|
3bitr4ri |
|- ( ( A. o e. J ( x e. o -> y e. o ) -> x = y ) <-> ( x =/= y -> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) ) |
34 |
33
|
imbi2i |
|- ( ( x e. X -> ( A. o e. J ( x e. o -> y e. o ) -> x = y ) ) <-> ( x e. X -> ( x =/= y -> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) ) ) |
35 |
|
eldifsn |
|- ( x e. ( U. J \ { y } ) <-> ( x e. U. J /\ x =/= y ) ) |
36 |
35
|
imbi1i |
|- ( ( x e. ( U. J \ { y } ) -> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) <-> ( ( x e. U. J /\ x =/= y ) -> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) ) |
37 |
|
impexp |
|- ( ( ( x e. U. J /\ x =/= y ) -> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) <-> ( x e. U. J -> ( x =/= y -> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) ) ) |
38 |
36 37
|
bitri |
|- ( ( x e. ( U. J \ { y } ) -> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) <-> ( x e. U. J -> ( x =/= y -> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) ) ) |
39 |
18 34 38
|
3bitr4g |
|- ( ( J e. ( TopOn ` X ) /\ y e. X ) -> ( ( x e. X -> ( A. o e. J ( x e. o -> y e. o ) -> x = y ) ) <-> ( x e. ( U. J \ { y } ) -> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) ) ) |
40 |
39
|
ralbidv2 |
|- ( ( J e. ( TopOn ` X ) /\ y e. X ) -> ( A. x e. X ( A. o e. J ( x e. o -> y e. o ) -> x = y ) <-> A. x e. ( U. J \ { y } ) E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) ) |
41 |
10 15 40
|
3bitr4d |
|- ( ( J e. ( TopOn ` X ) /\ y e. X ) -> ( { y } e. ( Clsd ` J ) <-> A. x e. X ( A. o e. J ( x e. o -> y e. o ) -> x = y ) ) ) |
42 |
41
|
ralbidva |
|- ( J e. ( TopOn ` X ) -> ( A. y e. X { y } e. ( Clsd ` J ) <-> A. y e. X A. x e. X ( A. o e. J ( x e. o -> y e. o ) -> x = y ) ) ) |
43 |
|
ralcom |
|- ( A. y e. X A. x e. X ( A. o e. J ( x e. o -> y e. o ) -> x = y ) <-> A. x e. X A. y e. X ( A. o e. J ( x e. o -> y e. o ) -> x = y ) ) |
44 |
42 43
|
bitrdi |
|- ( J e. ( TopOn ` X ) -> ( A. y e. X { y } e. ( Clsd ` J ) <-> A. x e. X A. y e. X ( A. o e. J ( x e. o -> y e. o ) -> x = y ) ) ) |
45 |
5 7 44
|
3bitr2d |
|- ( J e. ( TopOn ` X ) -> ( J e. Fre <-> A. x e. X A. y e. X ( A. o e. J ( x e. o -> y e. o ) -> x = y ) ) ) |