Step |
Hyp |
Ref |
Expression |
1 |
|
simp22 |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) |
2 |
|
simp1 |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → 𝐽 ∈ Top ) |
3 |
|
eqidd |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → ∪ 𝐽 = ∪ 𝐽 ) |
4 |
|
simp21 |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → 𝑍 ∈ 𝒫 ∪ 𝐽 ) |
5 |
4
|
elpwid |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → 𝑍 ⊆ ∪ 𝐽 ) |
6 |
|
eqidd |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → ( 𝐽 ↾t 𝑍 ) = ( 𝐽 ↾t 𝑍 ) ) |
7 |
2 3 5 6 1
|
restcls2lem |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → 𝐶 ⊆ 𝑍 ) |
8 |
7 5
|
sstrd |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → 𝐶 ⊆ ∪ 𝐽 ) |
9 |
1 8
|
elpwd |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → 𝐶 ∈ 𝒫 ∪ 𝐽 ) |
10 |
|
simp23 |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) |
11 |
2 3 5 6 10
|
restcls2lem |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → 𝐷 ⊆ 𝑍 ) |
12 |
11 5
|
sstrd |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → 𝐷 ⊆ ∪ 𝐽 ) |
13 |
10 12
|
elpwd |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → 𝐷 ∈ 𝒫 ∪ 𝐽 ) |
14 |
9 13
|
jca |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → ( 𝐶 ∈ 𝒫 ∪ 𝐽 ∧ 𝐷 ∈ 𝒫 ∪ 𝐽 ) ) |