Metamath Proof Explorer

Theorem crefi

Description: The property that every open cover has an A refinement for the topological space J . (Contributed by Thierry Arnoux, 7-Jan-2020)

Ref Expression
Hypothesis crefi.x ⊢ X = ⋃ J
Assertion crefi ⊢ J ∈ CovHasRef A ∧ C ⊆ J ∧ X = ⋃ C → ∃ z ∈ 𝒫 J ∩ A z Ref C

Proof

Step Hyp Ref Expression
1 crefi.x ⊢ X = ⋃ J
2 simp1 ⊢ J ∈ CovHasRef A ∧ C ⊆ J ∧ X = ⋃ C → J ∈ CovHasRef A
3 simp2 ⊢ J ∈ CovHasRef A ∧ C ⊆ J ∧ X = ⋃ C → C ⊆ J
4 2 3 sselpwd ⊢ J ∈ CovHasRef A ∧ C ⊆ J ∧ X = ⋃ C → C ∈ 𝒫 J
5 1 iscref ⊢ J ∈ CovHasRef A ↔ J ∈ Top ∧ ∀ y ∈ 𝒫 J X = ⋃ y → ∃ z ∈ 𝒫 J ∩ A z Ref y
6 5 simprbi ⊢ J ∈ CovHasRef A → ∀ y ∈ 𝒫 J X = ⋃ y → ∃ z ∈ 𝒫 J ∩ A z Ref y
7 6 3ad2ant1 ⊢ J ∈ CovHasRef A ∧ C ⊆ J ∧ X = ⋃ C → ∀ y ∈ 𝒫 J X = ⋃ y → ∃ z ∈ 𝒫 J ∩ A z Ref y
8 simp3 ⊢ J ∈ CovHasRef A ∧ C ⊆ J ∧ X = ⋃ C → X = ⋃ C
9 unieq ⊢ y = C → ⋃ y = ⋃ C
10 9 eqeq2d ⊢ y = C → X = ⋃ y ↔ X = ⋃ C
11 breq2 ⊢ y = C → z Ref y ↔ z Ref C
12 11 rexbidv ⊢ y = C → ∃ z ∈ 𝒫 J ∩ A z Ref y ↔ ∃ z ∈ 𝒫 J ∩ A z Ref C
13 10 12 imbi12d ⊢ y = C → X = ⋃ y → ∃ z ∈ 𝒫 J ∩ A z Ref y ↔ X = ⋃ C → ∃ z ∈ 𝒫 J ∩ A z Ref C
14 13 rspcv ⊢ C ∈ 𝒫 J → ∀ y ∈ 𝒫 J X = ⋃ y → ∃ z ∈ 𝒫 J ∩ A z Ref y → X = ⋃ C → ∃ z ∈ 𝒫 J ∩ A z Ref C
15 4 7 8 14 syl3c ⊢ J ∈ CovHasRef A ∧ C ⊆ J ∧ X = ⋃ C → ∃ z ∈ 𝒫 J ∩ A z Ref C