Step |
Hyp |
Ref |
Expression |
0 |
|
cha |
|- Haus |
1 |
|
vj |
|- j |
2 |
|
ctop |
|- Top |
3 |
|
vx |
|- x |
4 |
1
|
cv |
|- j |
5 |
4
|
cuni |
|- U. j |
6 |
|
vy |
|- y |
7 |
3
|
cv |
|- x |
8 |
6
|
cv |
|- y |
9 |
7 8
|
wne |
|- x =/= y |
10 |
|
vn |
|- n |
11 |
|
vm |
|- m |
12 |
10
|
cv |
|- n |
13 |
7 12
|
wcel |
|- x e. n |
14 |
11
|
cv |
|- m |
15 |
8 14
|
wcel |
|- y e. m |
16 |
12 14
|
cin |
|- ( n i^i m ) |
17 |
|
c0 |
|- (/) |
18 |
16 17
|
wceq |
|- ( n i^i m ) = (/) |
19 |
13 15 18
|
w3a |
|- ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) |
20 |
19 11 4
|
wrex |
|- E. m e. j ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) |
21 |
20 10 4
|
wrex |
|- E. n e. j E. m e. j ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) |
22 |
9 21
|
wi |
|- ( x =/= y -> E. n e. j E. m e. j ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) |
23 |
22 6 5
|
wral |
|- A. y e. U. j ( x =/= y -> E. n e. j E. m e. j ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) |
24 |
23 3 5
|
wral |
|- A. x e. U. j A. y e. U. j ( x =/= y -> E. n e. j E. m e. j ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) |
25 |
24 1 2
|
crab |
|- { j e. Top | A. x e. U. j A. y e. U. j ( x =/= y -> E. n e. j E. m e. j ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) } |
26 |
0 25
|
wceq |
|- Haus = { j e. Top | A. x e. U. j A. y e. U. j ( x =/= y -> E. n e. j E. m e. j ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) } |