Step |
Hyp |
Ref |
Expression |
1 |
|
ist1-2 |
|- ( 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 ) ) ) |
2 |
|
toponmax |
|- ( J e. ( TopOn ` X ) -> X e. J ) |
3 |
|
eleq2 |
|- ( o = X -> ( x e. o <-> x e. X ) ) |
4 |
3
|
intminss |
|- ( ( X e. J /\ x e. X ) -> |^| { o e. J | x e. o } C_ X ) |
5 |
2 4
|
sylan |
|- ( ( J e. ( TopOn ` X ) /\ x e. X ) -> |^| { o e. J | x e. o } C_ X ) |
6 |
5
|
sselda |
|- ( ( ( J e. ( TopOn ` X ) /\ x e. X ) /\ y e. |^| { o e. J | x e. o } ) -> y e. X ) |
7 |
|
biimt |
|- ( y e. X -> ( y e. { x } <-> ( y e. X -> y e. { x } ) ) ) |
8 |
6 7
|
syl |
|- ( ( ( J e. ( TopOn ` X ) /\ x e. X ) /\ y e. |^| { o e. J | x e. o } ) -> ( y e. { x } <-> ( y e. X -> y e. { x } ) ) ) |
9 |
8
|
ralbidva |
|- ( ( J e. ( TopOn ` X ) /\ x e. X ) -> ( A. y e. |^| { o e. J | x e. o } y e. { x } <-> A. y e. |^| { o e. J | x e. o } ( y e. X -> y e. { x } ) ) ) |
10 |
|
id |
|- ( x e. o -> x e. o ) |
11 |
10
|
rgenw |
|- A. o e. J ( x e. o -> x e. o ) |
12 |
|
vex |
|- x e. _V |
13 |
12
|
elintrab |
|- ( x e. |^| { o e. J | x e. o } <-> A. o e. J ( x e. o -> x e. o ) ) |
14 |
11 13
|
mpbir |
|- x e. |^| { o e. J | x e. o } |
15 |
|
snssi |
|- ( x e. |^| { o e. J | x e. o } -> { x } C_ |^| { o e. J | x e. o } ) |
16 |
14 15
|
ax-mp |
|- { x } C_ |^| { o e. J | x e. o } |
17 |
|
eqss |
|- ( |^| { o e. J | x e. o } = { x } <-> ( |^| { o e. J | x e. o } C_ { x } /\ { x } C_ |^| { o e. J | x e. o } ) ) |
18 |
16 17
|
mpbiran2 |
|- ( |^| { o e. J | x e. o } = { x } <-> |^| { o e. J | x e. o } C_ { x } ) |
19 |
|
dfss3 |
|- ( |^| { o e. J | x e. o } C_ { x } <-> A. y e. |^| { o e. J | x e. o } y e. { x } ) |
20 |
18 19
|
bitri |
|- ( |^| { o e. J | x e. o } = { x } <-> A. y e. |^| { o e. J | x e. o } y e. { x } ) |
21 |
|
vex |
|- y e. _V |
22 |
21
|
elintrab |
|- ( y e. |^| { o e. J | x e. o } <-> A. o e. J ( x e. o -> y e. o ) ) |
23 |
|
velsn |
|- ( y e. { x } <-> y = x ) |
24 |
|
equcom |
|- ( y = x <-> x = y ) |
25 |
23 24
|
bitri |
|- ( y e. { x } <-> x = y ) |
26 |
22 25
|
imbi12i |
|- ( ( y e. |^| { o e. J | x e. o } -> y e. { x } ) <-> ( A. o e. J ( x e. o -> y e. o ) -> x = y ) ) |
27 |
26
|
ralbii |
|- ( A. y e. X ( y e. |^| { o e. J | x e. o } -> y e. { x } ) <-> A. y e. X ( A. o e. J ( x e. o -> y e. o ) -> x = y ) ) |
28 |
|
ralcom3 |
|- ( A. y e. X ( y e. |^| { o e. J | x e. o } -> y e. { x } ) <-> A. y e. |^| { o e. J | x e. o } ( y e. X -> y e. { x } ) ) |
29 |
27 28
|
bitr3i |
|- ( A. y e. X ( A. o e. J ( x e. o -> y e. o ) -> x = y ) <-> A. y e. |^| { o e. J | x e. o } ( y e. X -> y e. { x } ) ) |
30 |
9 20 29
|
3bitr4g |
|- ( ( J e. ( TopOn ` X ) /\ x e. X ) -> ( |^| { o e. J | x e. o } = { x } <-> A. y e. X ( A. o e. J ( x e. o -> y e. o ) -> x = y ) ) ) |
31 |
30
|
ralbidva |
|- ( J e. ( TopOn ` X ) -> ( A. x e. X |^| { o e. J | x e. o } = { x } <-> A. x e. X A. y e. X ( A. o e. J ( x e. o -> y e. o ) -> x = y ) ) ) |
32 |
1 31
|
bitr4d |
|- ( J e. ( TopOn ` X ) -> ( J e. Fre <-> A. x e. X |^| { o e. J | x e. o } = { x } ) ) |