| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ist0.1 |
|- X = U. J |
| 2 |
1
|
ishaus |
|- ( J e. Haus <-> ( J e. Top /\ A. x e. X A. y e. X ( x =/= y -> E. n e. J E. m e. J ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) ) ) |
| 3 |
2
|
simprbi |
|- ( J e. Haus -> A. x e. X A. y e. X ( x =/= y -> E. n e. J E. m e. J ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) ) |
| 4 |
|
neeq1 |
|- ( x = P -> ( x =/= y <-> P =/= y ) ) |
| 5 |
|
eleq1 |
|- ( x = P -> ( x e. n <-> P e. n ) ) |
| 6 |
5
|
3anbi1d |
|- ( x = P -> ( ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) <-> ( P e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) ) |
| 7 |
6
|
2rexbidv |
|- ( x = P -> ( E. n e. J E. m e. J ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) <-> E. n e. J E. m e. J ( P e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) ) |
| 8 |
4 7
|
imbi12d |
|- ( x = P -> ( ( x =/= y -> E. n e. J E. m e. J ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) <-> ( P =/= y -> E. n e. J E. m e. J ( P e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) ) ) |
| 9 |
|
neeq2 |
|- ( y = Q -> ( P =/= y <-> P =/= Q ) ) |
| 10 |
|
eleq1 |
|- ( y = Q -> ( y e. m <-> Q e. m ) ) |
| 11 |
10
|
3anbi2d |
|- ( y = Q -> ( ( P e. n /\ y e. m /\ ( n i^i m ) = (/) ) <-> ( P e. n /\ Q e. m /\ ( n i^i m ) = (/) ) ) ) |
| 12 |
11
|
2rexbidv |
|- ( y = Q -> ( E. n e. J E. m e. J ( P e. n /\ y e. m /\ ( n i^i m ) = (/) ) <-> E. n e. J E. m e. J ( P e. n /\ Q e. m /\ ( n i^i m ) = (/) ) ) ) |
| 13 |
9 12
|
imbi12d |
|- ( y = Q -> ( ( P =/= y -> E. n e. J E. m e. J ( P e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) <-> ( P =/= Q -> E. n e. J E. m e. J ( P e. n /\ Q e. m /\ ( n i^i m ) = (/) ) ) ) ) |
| 14 |
8 13
|
rspc2v |
|- ( ( P e. X /\ Q e. X ) -> ( A. x e. X A. y e. X ( x =/= y -> E. n e. J E. m e. J ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) -> ( P =/= Q -> E. n e. J E. m e. J ( P e. n /\ Q e. m /\ ( n i^i m ) = (/) ) ) ) ) |
| 15 |
3 14
|
syl5 |
|- ( ( P e. X /\ Q e. X ) -> ( J e. Haus -> ( P =/= Q -> E. n e. J E. m e. J ( P e. n /\ Q e. m /\ ( n i^i m ) = (/) ) ) ) ) |
| 16 |
15
|
ex |
|- ( P e. X -> ( Q e. X -> ( J e. Haus -> ( P =/= Q -> E. n e. J E. m e. J ( P e. n /\ Q e. m /\ ( n i^i m ) = (/) ) ) ) ) ) |
| 17 |
16
|
com3r |
|- ( J e. Haus -> ( P e. X -> ( Q e. X -> ( P =/= Q -> E. n e. J E. m e. J ( P e. n /\ Q e. m /\ ( n i^i m ) = (/) ) ) ) ) ) |
| 18 |
17
|
3imp2 |
|- ( ( J e. Haus /\ ( P e. X /\ Q e. X /\ P =/= Q ) ) -> E. n e. J E. m e. J ( P e. n /\ Q e. m /\ ( n i^i m ) = (/) ) ) |