Step |
Hyp |
Ref |
Expression |
1 |
|
toponcom |
⊢ ( ( 𝐾 ∈ Top ∧ 𝐽 ∈ ( TopOn ‘ ∪ 𝐾 ) ) → 𝐾 ∈ ( TopOn ‘ ∪ 𝐽 ) ) |
2 |
1
|
ex |
⊢ ( 𝐾 ∈ Top → ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐾 ) → 𝐾 ∈ ( TopOn ‘ ∪ 𝐽 ) ) ) |
3 |
2
|
adantl |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐾 ) → 𝐾 ∈ ( TopOn ‘ ∪ 𝐽 ) ) ) |
4 |
|
toponcom |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ ( TopOn ‘ ∪ 𝐽 ) ) → 𝐽 ∈ ( TopOn ‘ ∪ 𝐾 ) ) |
5 |
4
|
ex |
⊢ ( 𝐽 ∈ Top → ( 𝐾 ∈ ( TopOn ‘ ∪ 𝐽 ) → 𝐽 ∈ ( TopOn ‘ ∪ 𝐾 ) ) ) |
6 |
5
|
adantr |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐾 ∈ ( TopOn ‘ ∪ 𝐽 ) → 𝐽 ∈ ( TopOn ‘ ∪ 𝐾 ) ) ) |
7 |
3 6
|
impbid |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐾 ) ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐽 ) ) ) |