Step |
Hyp |
Ref |
Expression |
1 |
|
topontop |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top ) |
2 |
|
eqid |
⊢ ∪ 𝐽 = ∪ 𝐽 |
3 |
2
|
ist0 |
⊢ ( 𝐽 ∈ Kol2 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ ∪ 𝐽 ∀ 𝑦 ∈ ∪ 𝐽 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) ) |
4 |
3
|
baib |
⊢ ( 𝐽 ∈ Top → ( 𝐽 ∈ Kol2 ↔ ∀ 𝑥 ∈ ∪ 𝐽 ∀ 𝑦 ∈ ∪ 𝐽 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) ) |
5 |
1 4
|
syl |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Kol2 ↔ ∀ 𝑥 ∈ ∪ 𝐽 ∀ 𝑦 ∈ ∪ 𝐽 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) ) |
6 |
|
toponuni |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 ) |
7 |
6
|
raleqdv |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ∀ 𝑦 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ∈ ∪ 𝐽 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) ) |
8 |
6 7
|
raleqbidv |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ ∪ 𝐽 ∀ 𝑦 ∈ ∪ 𝐽 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) ) |
9 |
5 8
|
bitr4d |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Kol2 ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) ) |