Step |
Hyp |
Ref |
Expression |
1 |
|
lmmo.1 |
|- ( ph -> J e. Haus ) |
2 |
|
lmmo.4 |
|- ( ph -> F ( ~~>t ` J ) A ) |
3 |
|
lmmo.5 |
|- ( ph -> F ( ~~>t ` J ) B ) |
4 |
|
an4 |
|- ( ( ( x e. J /\ y e. J ) /\ ( A e. x /\ B e. y ) ) <-> ( ( x e. J /\ A e. x ) /\ ( y e. J /\ B e. y ) ) ) |
5 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
6 |
|
simprr |
|- ( ( ph /\ ( x e. J /\ A e. x ) ) -> A e. x ) |
7 |
|
1zzd |
|- ( ( ph /\ ( x e. J /\ A e. x ) ) -> 1 e. ZZ ) |
8 |
2
|
adantr |
|- ( ( ph /\ ( x e. J /\ A e. x ) ) -> F ( ~~>t ` J ) A ) |
9 |
|
simprl |
|- ( ( ph /\ ( x e. J /\ A e. x ) ) -> x e. J ) |
10 |
5 6 7 8 9
|
lmcvg |
|- ( ( ph /\ ( x e. J /\ A e. x ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( F ` k ) e. x ) |
11 |
10
|
ex |
|- ( ph -> ( ( x e. J /\ A e. x ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( F ` k ) e. x ) ) |
12 |
|
simprr |
|- ( ( ph /\ ( y e. J /\ B e. y ) ) -> B e. y ) |
13 |
|
1zzd |
|- ( ( ph /\ ( y e. J /\ B e. y ) ) -> 1 e. ZZ ) |
14 |
3
|
adantr |
|- ( ( ph /\ ( y e. J /\ B e. y ) ) -> F ( ~~>t ` J ) B ) |
15 |
|
simprl |
|- ( ( ph /\ ( y e. J /\ B e. y ) ) -> y e. J ) |
16 |
5 12 13 14 15
|
lmcvg |
|- ( ( ph /\ ( y e. J /\ B e. y ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( F ` k ) e. y ) |
17 |
16
|
ex |
|- ( ph -> ( ( y e. J /\ B e. y ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( F ` k ) e. y ) ) |
18 |
11 17
|
anim12d |
|- ( ph -> ( ( ( x e. J /\ A e. x ) /\ ( y e. J /\ B e. y ) ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( F ` k ) e. x /\ E. j e. NN A. k e. ( ZZ>= ` j ) ( F ` k ) e. y ) ) ) |
19 |
5
|
rexanuz2 |
|- ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. x /\ ( F ` k ) e. y ) <-> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( F ` k ) e. x /\ E. j e. NN A. k e. ( ZZ>= ` j ) ( F ` k ) e. y ) ) |
20 |
|
nnz |
|- ( j e. NN -> j e. ZZ ) |
21 |
|
uzid |
|- ( j e. ZZ -> j e. ( ZZ>= ` j ) ) |
22 |
|
ne0i |
|- ( j e. ( ZZ>= ` j ) -> ( ZZ>= ` j ) =/= (/) ) |
23 |
20 21 22
|
3syl |
|- ( j e. NN -> ( ZZ>= ` j ) =/= (/) ) |
24 |
|
r19.2z |
|- ( ( ( ZZ>= ` j ) =/= (/) /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. x /\ ( F ` k ) e. y ) ) -> E. k e. ( ZZ>= ` j ) ( ( F ` k ) e. x /\ ( F ` k ) e. y ) ) |
25 |
|
elin |
|- ( ( F ` k ) e. ( x i^i y ) <-> ( ( F ` k ) e. x /\ ( F ` k ) e. y ) ) |
26 |
|
n0i |
|- ( ( F ` k ) e. ( x i^i y ) -> -. ( x i^i y ) = (/) ) |
27 |
25 26
|
sylbir |
|- ( ( ( F ` k ) e. x /\ ( F ` k ) e. y ) -> -. ( x i^i y ) = (/) ) |
28 |
27
|
rexlimivw |
|- ( E. k e. ( ZZ>= ` j ) ( ( F ` k ) e. x /\ ( F ` k ) e. y ) -> -. ( x i^i y ) = (/) ) |
29 |
24 28
|
syl |
|- ( ( ( ZZ>= ` j ) =/= (/) /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. x /\ ( F ` k ) e. y ) ) -> -. ( x i^i y ) = (/) ) |
30 |
23 29
|
sylan |
|- ( ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. x /\ ( F ` k ) e. y ) ) -> -. ( x i^i y ) = (/) ) |
31 |
30
|
rexlimiva |
|- ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. x /\ ( F ` k ) e. y ) -> -. ( x i^i y ) = (/) ) |
32 |
19 31
|
sylbir |
|- ( ( E. j e. NN A. k e. ( ZZ>= ` j ) ( F ` k ) e. x /\ E. j e. NN A. k e. ( ZZ>= ` j ) ( F ` k ) e. y ) -> -. ( x i^i y ) = (/) ) |
33 |
18 32
|
syl6 |
|- ( ph -> ( ( ( x e. J /\ A e. x ) /\ ( y e. J /\ B e. y ) ) -> -. ( x i^i y ) = (/) ) ) |
34 |
4 33
|
syl5bi |
|- ( ph -> ( ( ( x e. J /\ y e. J ) /\ ( A e. x /\ B e. y ) ) -> -. ( x i^i y ) = (/) ) ) |
35 |
34
|
expdimp |
|- ( ( ph /\ ( x e. J /\ y e. J ) ) -> ( ( A e. x /\ B e. y ) -> -. ( x i^i y ) = (/) ) ) |
36 |
|
imnan |
|- ( ( ( A e. x /\ B e. y ) -> -. ( x i^i y ) = (/) ) <-> -. ( ( A e. x /\ B e. y ) /\ ( x i^i y ) = (/) ) ) |
37 |
35 36
|
sylib |
|- ( ( ph /\ ( x e. J /\ y e. J ) ) -> -. ( ( A e. x /\ B e. y ) /\ ( x i^i y ) = (/) ) ) |
38 |
|
df-3an |
|- ( ( A e. x /\ B e. y /\ ( x i^i y ) = (/) ) <-> ( ( A e. x /\ B e. y ) /\ ( x i^i y ) = (/) ) ) |
39 |
37 38
|
sylnibr |
|- ( ( ph /\ ( x e. J /\ y e. J ) ) -> -. ( A e. x /\ B e. y /\ ( x i^i y ) = (/) ) ) |
40 |
39
|
anassrs |
|- ( ( ( ph /\ x e. J ) /\ y e. J ) -> -. ( A e. x /\ B e. y /\ ( x i^i y ) = (/) ) ) |
41 |
40
|
nrexdv |
|- ( ( ph /\ x e. J ) -> -. E. y e. J ( A e. x /\ B e. y /\ ( x i^i y ) = (/) ) ) |
42 |
41
|
nrexdv |
|- ( ph -> -. E. x e. J E. y e. J ( A e. x /\ B e. y /\ ( x i^i y ) = (/) ) ) |
43 |
|
haustop |
|- ( J e. Haus -> J e. Top ) |
44 |
1 43
|
syl |
|- ( ph -> J e. Top ) |
45 |
|
toptopon2 |
|- ( J e. Top <-> J e. ( TopOn ` U. J ) ) |
46 |
44 45
|
sylib |
|- ( ph -> J e. ( TopOn ` U. J ) ) |
47 |
|
lmcl |
|- ( ( J e. ( TopOn ` U. J ) /\ F ( ~~>t ` J ) A ) -> A e. U. J ) |
48 |
46 2 47
|
syl2anc |
|- ( ph -> A e. U. J ) |
49 |
|
lmcl |
|- ( ( J e. ( TopOn ` U. J ) /\ F ( ~~>t ` J ) B ) -> B e. U. J ) |
50 |
46 3 49
|
syl2anc |
|- ( ph -> B e. U. J ) |
51 |
|
eqid |
|- U. J = U. J |
52 |
51
|
hausnei |
|- ( ( J e. Haus /\ ( A e. U. J /\ B e. U. J /\ A =/= B ) ) -> E. x e. J E. y e. J ( A e. x /\ B e. y /\ ( x i^i y ) = (/) ) ) |
53 |
52
|
3exp2 |
|- ( J e. Haus -> ( A e. U. J -> ( B e. U. J -> ( A =/= B -> E. x e. J E. y e. J ( A e. x /\ B e. y /\ ( x i^i y ) = (/) ) ) ) ) ) |
54 |
1 48 50 53
|
syl3c |
|- ( ph -> ( A =/= B -> E. x e. J E. y e. J ( A e. x /\ B e. y /\ ( x i^i y ) = (/) ) ) ) |
55 |
54
|
necon1bd |
|- ( ph -> ( -. E. x e. J E. y e. J ( A e. x /\ B e. y /\ ( x i^i y ) = (/) ) -> A = B ) ) |
56 |
42 55
|
mpd |
|- ( ph -> A = B ) |