Step |
Hyp |
Ref |
Expression |
1 |
|
ishaus2 |
|- ( J e. ( TopOn ` X ) -> ( J e. Haus <-> A. x e. X A. y e. X ( x =/= y -> E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) ) |
2 |
|
topontop |
|- ( J e. ( TopOn ` X ) -> J e. Top ) |
3 |
|
simp1 |
|- ( ( J e. Top /\ m e. J /\ n e. J ) -> J e. Top ) |
4 |
|
simp2 |
|- ( ( J e. Top /\ m e. J /\ n e. J ) -> m e. J ) |
5 |
|
simp1 |
|- ( ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) -> x e. m ) |
6 |
|
opnneip |
|- ( ( J e. Top /\ m e. J /\ x e. m ) -> m e. ( ( nei ` J ) ` { x } ) ) |
7 |
3 4 5 6
|
syl2an3an |
|- ( ( ( J e. Top /\ m e. J /\ n e. J ) /\ ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) -> m e. ( ( nei ` J ) ` { x } ) ) |
8 |
|
simp3 |
|- ( ( J e. Top /\ m e. J /\ n e. J ) -> n e. J ) |
9 |
|
simp2 |
|- ( ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) -> y e. n ) |
10 |
|
opnneip |
|- ( ( J e. Top /\ n e. J /\ y e. n ) -> n e. ( ( nei ` J ) ` { y } ) ) |
11 |
3 8 9 10
|
syl2an3an |
|- ( ( ( J e. Top /\ m e. J /\ n e. J ) /\ ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) -> n e. ( ( nei ` J ) ` { y } ) ) |
12 |
|
simpr3 |
|- ( ( ( J e. Top /\ m e. J /\ n e. J ) /\ ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) -> ( m i^i n ) = (/) ) |
13 |
|
ineq1 |
|- ( u = m -> ( u i^i v ) = ( m i^i v ) ) |
14 |
13
|
eqeq1d |
|- ( u = m -> ( ( u i^i v ) = (/) <-> ( m i^i v ) = (/) ) ) |
15 |
|
ineq2 |
|- ( v = n -> ( m i^i v ) = ( m i^i n ) ) |
16 |
15
|
eqeq1d |
|- ( v = n -> ( ( m i^i v ) = (/) <-> ( m i^i n ) = (/) ) ) |
17 |
14 16
|
rspc2ev |
|- ( ( m e. ( ( nei ` J ) ` { x } ) /\ n e. ( ( nei ` J ) ` { y } ) /\ ( m i^i n ) = (/) ) -> E. u e. ( ( nei ` J ) ` { x } ) E. v e. ( ( nei ` J ) ` { y } ) ( u i^i v ) = (/) ) |
18 |
7 11 12 17
|
syl3anc |
|- ( ( ( J e. Top /\ m e. J /\ n e. J ) /\ ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) -> E. u e. ( ( nei ` J ) ` { x } ) E. v e. ( ( nei ` J ) ` { y } ) ( u i^i v ) = (/) ) |
19 |
18
|
ex |
|- ( ( J e. Top /\ m e. J /\ n e. J ) -> ( ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) -> E. u e. ( ( nei ` J ) ` { x } ) E. v e. ( ( nei ` J ) ` { y } ) ( u i^i v ) = (/) ) ) |
20 |
19
|
3expib |
|- ( J e. Top -> ( ( m e. J /\ n e. J ) -> ( ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) -> E. u e. ( ( nei ` J ) ` { x } ) E. v e. ( ( nei ` J ) ` { y } ) ( u i^i v ) = (/) ) ) ) |
21 |
20
|
rexlimdvv |
|- ( J e. Top -> ( E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) -> E. u e. ( ( nei ` J ) ` { x } ) E. v e. ( ( nei ` J ) ` { y } ) ( u i^i v ) = (/) ) ) |
22 |
|
neii2 |
|- ( ( J e. Top /\ u e. ( ( nei ` J ) ` { x } ) ) -> E. m e. J ( { x } C_ m /\ m C_ u ) ) |
23 |
22
|
ex |
|- ( J e. Top -> ( u e. ( ( nei ` J ) ` { x } ) -> E. m e. J ( { x } C_ m /\ m C_ u ) ) ) |
24 |
|
neii2 |
|- ( ( J e. Top /\ v e. ( ( nei ` J ) ` { y } ) ) -> E. n e. J ( { y } C_ n /\ n C_ v ) ) |
25 |
24
|
ex |
|- ( J e. Top -> ( v e. ( ( nei ` J ) ` { y } ) -> E. n e. J ( { y } C_ n /\ n C_ v ) ) ) |
26 |
|
vex |
|- x e. _V |
27 |
26
|
snss |
|- ( x e. m <-> { x } C_ m ) |
28 |
27
|
anbi1i |
|- ( ( x e. m /\ m C_ u ) <-> ( { x } C_ m /\ m C_ u ) ) |
29 |
|
vex |
|- y e. _V |
30 |
29
|
snss |
|- ( y e. n <-> { y } C_ n ) |
31 |
30
|
anbi1i |
|- ( ( y e. n /\ n C_ v ) <-> ( { y } C_ n /\ n C_ v ) ) |
32 |
|
simp1l |
|- ( ( ( x e. m /\ m C_ u ) /\ ( y e. n /\ n C_ v ) /\ ( u i^i v ) = (/) ) -> x e. m ) |
33 |
|
simp2l |
|- ( ( ( x e. m /\ m C_ u ) /\ ( y e. n /\ n C_ v ) /\ ( u i^i v ) = (/) ) -> y e. n ) |
34 |
|
ss2in |
|- ( ( m C_ u /\ n C_ v ) -> ( m i^i n ) C_ ( u i^i v ) ) |
35 |
|
ssn0 |
|- ( ( ( m i^i n ) C_ ( u i^i v ) /\ ( m i^i n ) =/= (/) ) -> ( u i^i v ) =/= (/) ) |
36 |
35
|
ex |
|- ( ( m i^i n ) C_ ( u i^i v ) -> ( ( m i^i n ) =/= (/) -> ( u i^i v ) =/= (/) ) ) |
37 |
36
|
necon4d |
|- ( ( m i^i n ) C_ ( u i^i v ) -> ( ( u i^i v ) = (/) -> ( m i^i n ) = (/) ) ) |
38 |
34 37
|
syl |
|- ( ( m C_ u /\ n C_ v ) -> ( ( u i^i v ) = (/) -> ( m i^i n ) = (/) ) ) |
39 |
38
|
ad2ant2l |
|- ( ( ( x e. m /\ m C_ u ) /\ ( y e. n /\ n C_ v ) ) -> ( ( u i^i v ) = (/) -> ( m i^i n ) = (/) ) ) |
40 |
39
|
3impia |
|- ( ( ( x e. m /\ m C_ u ) /\ ( y e. n /\ n C_ v ) /\ ( u i^i v ) = (/) ) -> ( m i^i n ) = (/) ) |
41 |
32 33 40
|
3jca |
|- ( ( ( x e. m /\ m C_ u ) /\ ( y e. n /\ n C_ v ) /\ ( u i^i v ) = (/) ) -> ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) |
42 |
41
|
3exp |
|- ( ( x e. m /\ m C_ u ) -> ( ( y e. n /\ n C_ v ) -> ( ( u i^i v ) = (/) -> ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) ) |
43 |
31 42
|
syl5bir |
|- ( ( x e. m /\ m C_ u ) -> ( ( { y } C_ n /\ n C_ v ) -> ( ( u i^i v ) = (/) -> ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) ) |
44 |
43
|
com3r |
|- ( ( u i^i v ) = (/) -> ( ( x e. m /\ m C_ u ) -> ( ( { y } C_ n /\ n C_ v ) -> ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) ) |
45 |
44
|
imp |
|- ( ( ( u i^i v ) = (/) /\ ( x e. m /\ m C_ u ) ) -> ( ( { y } C_ n /\ n C_ v ) -> ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) |
46 |
45
|
3adant1 |
|- ( ( J e. Top /\ ( u i^i v ) = (/) /\ ( x e. m /\ m C_ u ) ) -> ( ( { y } C_ n /\ n C_ v ) -> ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) |
47 |
46
|
reximdv |
|- ( ( J e. Top /\ ( u i^i v ) = (/) /\ ( x e. m /\ m C_ u ) ) -> ( E. n e. J ( { y } C_ n /\ n C_ v ) -> E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) |
48 |
47
|
3exp |
|- ( J e. Top -> ( ( u i^i v ) = (/) -> ( ( x e. m /\ m C_ u ) -> ( E. n e. J ( { y } C_ n /\ n C_ v ) -> E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) ) ) |
49 |
48
|
com34 |
|- ( J e. Top -> ( ( u i^i v ) = (/) -> ( E. n e. J ( { y } C_ n /\ n C_ v ) -> ( ( x e. m /\ m C_ u ) -> E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) ) ) |
50 |
49
|
3imp |
|- ( ( J e. Top /\ ( u i^i v ) = (/) /\ E. n e. J ( { y } C_ n /\ n C_ v ) ) -> ( ( x e. m /\ m C_ u ) -> E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) |
51 |
28 50
|
syl5bir |
|- ( ( J e. Top /\ ( u i^i v ) = (/) /\ E. n e. J ( { y } C_ n /\ n C_ v ) ) -> ( ( { x } C_ m /\ m C_ u ) -> E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) |
52 |
51
|
reximdv |
|- ( ( J e. Top /\ ( u i^i v ) = (/) /\ E. n e. J ( { y } C_ n /\ n C_ v ) ) -> ( E. m e. J ( { x } C_ m /\ m C_ u ) -> E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) |
53 |
52
|
3exp |
|- ( J e. Top -> ( ( u i^i v ) = (/) -> ( E. n e. J ( { y } C_ n /\ n C_ v ) -> ( E. m e. J ( { x } C_ m /\ m C_ u ) -> E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) ) ) |
54 |
53
|
com24 |
|- ( J e. Top -> ( E. m e. J ( { x } C_ m /\ m C_ u ) -> ( E. n e. J ( { y } C_ n /\ n C_ v ) -> ( ( u i^i v ) = (/) -> E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) ) ) |
55 |
54
|
impd |
|- ( J e. Top -> ( ( E. m e. J ( { x } C_ m /\ m C_ u ) /\ E. n e. J ( { y } C_ n /\ n C_ v ) ) -> ( ( u i^i v ) = (/) -> E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) ) |
56 |
23 25 55
|
syl2and |
|- ( J e. Top -> ( ( u e. ( ( nei ` J ) ` { x } ) /\ v e. ( ( nei ` J ) ` { y } ) ) -> ( ( u i^i v ) = (/) -> E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) ) |
57 |
56
|
rexlimdvv |
|- ( J e. Top -> ( E. u e. ( ( nei ` J ) ` { x } ) E. v e. ( ( nei ` J ) ` { y } ) ( u i^i v ) = (/) -> E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) |
58 |
21 57
|
impbid |
|- ( J e. Top -> ( E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) <-> E. u e. ( ( nei ` J ) ` { x } ) E. v e. ( ( nei ` J ) ` { y } ) ( u i^i v ) = (/) ) ) |
59 |
58
|
imbi2d |
|- ( J e. Top -> ( ( x =/= y -> E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) <-> ( x =/= y -> E. u e. ( ( nei ` J ) ` { x } ) E. v e. ( ( nei ` J ) ` { y } ) ( u i^i v ) = (/) ) ) ) |
60 |
59
|
2ralbidv |
|- ( J e. Top -> ( A. x e. X A. y e. X ( x =/= y -> E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) <-> A. x e. X A. y e. X ( x =/= y -> E. u e. ( ( nei ` J ) ` { x } ) E. v e. ( ( nei ` J ) ` { y } ) ( u i^i v ) = (/) ) ) ) |
61 |
2 60
|
syl |
|- ( J e. ( TopOn ` X ) -> ( A. x e. X A. y e. X ( x =/= y -> E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) <-> A. x e. X A. y e. X ( x =/= y -> E. u e. ( ( nei ` J ) ` { x } ) E. v e. ( ( nei ` J ) ` { y } ) ( u i^i v ) = (/) ) ) ) |
62 |
1 61
|
bitrd |
|- ( J e. ( TopOn ` X ) -> ( J e. Haus <-> A. x e. X A. y e. X ( x =/= y -> E. u e. ( ( nei ` J ) ` { x } ) E. v e. ( ( nei ` J ) ` { y } ) ( u i^i v ) = (/) ) ) ) |