Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
⊢ ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } ) = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } ) |
2 |
|
eqid |
⊢ ∪ 𝐽 = ∪ 𝐽 |
3 |
1 2
|
iscvm |
⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ↔ ( ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ∧ 𝐹 ∈ ( 𝐶 Cn 𝐽 ) ) ∧ ∀ 𝑥 ∈ ∪ 𝐽 ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ( ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } ) ‘ 𝑘 ) ≠ ∅ ) ) ) |
4 |
3
|
simplbi |
⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ∧ 𝐹 ∈ ( 𝐶 Cn 𝐽 ) ) ) |
5 |
4
|
simp3d |
⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐹 ∈ ( 𝐶 Cn 𝐽 ) ) |