Step |
Hyp |
Ref |
Expression |
1 |
|
ist0.1 |
|- X = U. J |
2 |
|
iunid |
|- U_ x e. A { x } = A |
3 |
1
|
ist1 |
|- ( J e. Fre <-> ( J e. Top /\ A. x e. X { x } e. ( Clsd ` J ) ) ) |
4 |
3
|
simplbi |
|- ( J e. Fre -> J e. Top ) |
5 |
4
|
3ad2ant1 |
|- ( ( J e. Fre /\ A C_ X /\ A e. Fin ) -> J e. Top ) |
6 |
|
simp3 |
|- ( ( J e. Fre /\ A C_ X /\ A e. Fin ) -> A e. Fin ) |
7 |
3
|
simprbi |
|- ( J e. Fre -> A. x e. X { x } e. ( Clsd ` J ) ) |
8 |
|
ssralv |
|- ( A C_ X -> ( A. x e. X { x } e. ( Clsd ` J ) -> A. x e. A { x } e. ( Clsd ` J ) ) ) |
9 |
7 8
|
mpan9 |
|- ( ( J e. Fre /\ A C_ X ) -> A. x e. A { x } e. ( Clsd ` J ) ) |
10 |
9
|
3adant3 |
|- ( ( J e. Fre /\ A C_ X /\ A e. Fin ) -> A. x e. A { x } e. ( Clsd ` J ) ) |
11 |
1
|
iuncld |
|- ( ( J e. Top /\ A e. Fin /\ A. x e. A { x } e. ( Clsd ` J ) ) -> U_ x e. A { x } e. ( Clsd ` J ) ) |
12 |
5 6 10 11
|
syl3anc |
|- ( ( J e. Fre /\ A C_ X /\ A e. Fin ) -> U_ x e. A { x } e. ( Clsd ` J ) ) |
13 |
2 12
|
eqeltrrid |
|- ( ( J e. Fre /\ A C_ X /\ A e. Fin ) -> A e. ( Clsd ` J ) ) |