Metamath Proof Explorer

Theorem crefss

Description: The "every open cover has an A refinement" predicate respects inclusion. (Contributed by Thierry Arnoux, 7-Jan-2020)

Ref Expression
Assertion crefss ⊢ A ⊆ B → CovHasRef A ⊆ CovHasRef B

Proof

Step Hyp Ref Expression
1 sslin ⊢ A ⊆ B → 𝒫 j ∩ A ⊆ 𝒫 j ∩ B
2 ssrexv ⊢ 𝒫 j ∩ A ⊆ 𝒫 j ∩ B → ∃ z ∈ 𝒫 j ∩ A z Ref y → ∃ z ∈ 𝒫 j ∩ B z Ref y
3 1 2 syl ⊢ A ⊆ B → ∃ z ∈ 𝒫 j ∩ A z Ref y → ∃ z ∈ 𝒫 j ∩ B z Ref y
4 3 imim2d ⊢ A ⊆ B → ⋃ j = ⋃ y → ∃ z ∈ 𝒫 j ∩ A z Ref y → ⋃ j = ⋃ y → ∃ z ∈ 𝒫 j ∩ B z Ref y
5 4 ralimdv ⊢ A ⊆ B → ∀ y ∈ 𝒫 j ⋃ j = ⋃ y → ∃ z ∈ 𝒫 j ∩ A z Ref y → ∀ y ∈ 𝒫 j ⋃ j = ⋃ y → ∃ z ∈ 𝒫 j ∩ B z Ref y
6 5 anim2d ⊢ A ⊆ B → j ∈ Top ∧ ∀ y ∈ 𝒫 j ⋃ j = ⋃ y → ∃ z ∈ 𝒫 j ∩ A z Ref y → j ∈ Top ∧ ∀ y ∈ 𝒫 j ⋃ j = ⋃ y → ∃ z ∈ 𝒫 j ∩ B z Ref y
7 eqid ⊢ ⋃ j = ⋃ j
8 7 iscref ⊢ j ∈ CovHasRef A ↔ j ∈ Top ∧ ∀ y ∈ 𝒫 j ⋃ j = ⋃ y → ∃ z ∈ 𝒫 j ∩ A z Ref y
9 7 iscref ⊢ j ∈ CovHasRef B ↔ j ∈ Top ∧ ∀ y ∈ 𝒫 j ⋃ j = ⋃ y → ∃ z ∈ 𝒫 j ∩ B z Ref y
10 6 8 9 3imtr4g ⊢ A ⊆ B → j ∈ CovHasRef A → j ∈ CovHasRef B
11 10 ssrdv ⊢ A ⊆ B → CovHasRef A ⊆ CovHasRef B