Metamath Proof Explorer


Theorem iscref

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 iscref.x 𝑋 = 𝐽
Assertion iscref ( 𝐽 ∈ CovHasRef 𝐴 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝐽 ( 𝑋 = 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝐽𝐴 ) 𝑧 Ref 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 iscref.x 𝑋 = 𝐽
2 pweq ( 𝑗 = 𝐽 → 𝒫 𝑗 = 𝒫 𝐽 )
3 unieq ( 𝑗 = 𝐽 𝑗 = 𝐽 )
4 3 1 eqtr4di ( 𝑗 = 𝐽 𝑗 = 𝑋 )
5 4 eqeq1d ( 𝑗 = 𝐽 → ( 𝑗 = 𝑦𝑋 = 𝑦 ) )
6 2 ineq1d ( 𝑗 = 𝐽 → ( 𝒫 𝑗𝐴 ) = ( 𝒫 𝐽𝐴 ) )
7 6 rexeqdv ( 𝑗 = 𝐽 → ( ∃ 𝑧 ∈ ( 𝒫 𝑗𝐴 ) 𝑧 Ref 𝑦 ↔ ∃ 𝑧 ∈ ( 𝒫 𝐽𝐴 ) 𝑧 Ref 𝑦 ) )
8 5 7 imbi12d ( 𝑗 = 𝐽 → ( ( 𝑗 = 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗𝐴 ) 𝑧 Ref 𝑦 ) ↔ ( 𝑋 = 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝐽𝐴 ) 𝑧 Ref 𝑦 ) ) )
9 2 8 raleqbidv ( 𝑗 = 𝐽 → ( ∀ 𝑦 ∈ 𝒫 𝑗 ( 𝑗 = 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗𝐴 ) 𝑧 Ref 𝑦 ) ↔ ∀ 𝑦 ∈ 𝒫 𝐽 ( 𝑋 = 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝐽𝐴 ) 𝑧 Ref 𝑦 ) ) )
10 df-cref CovHasRef 𝐴 = { 𝑗 ∈ Top ∣ ∀ 𝑦 ∈ 𝒫 𝑗 ( 𝑗 = 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗𝐴 ) 𝑧 Ref 𝑦 ) }
11 9 10 elrab2 ( 𝐽 ∈ CovHasRef 𝐴 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝐽 ( 𝑋 = 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝐽𝐴 ) 𝑧 Ref 𝑦 ) ) )