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 \subseteq B \to CovHasRef A \subseteq CovHasRef B$

Step	Hyp	Ref	Expression
1		sslin	$⊢ A \subseteq B \to 𝒫 j \cap A \subseteq 𝒫 j \cap B$
2		ssrexv	$⊢ 𝒫 j \cap A \subseteq 𝒫 j \cap B \to (\exists z \in (𝒫 j \cap A) z Ref y \to \exists z \in (𝒫 j \cap B) z Ref y)$
3	1 2	syl	$⊢ A \subseteq B \to (\exists z \in (𝒫 j \cap A) z Ref y \to \exists z \in (𝒫 j \cap B) z Ref y)$
4	3	imim2d	$⊢ A \subseteq B \to ((⋃ j = ⋃ y \to \exists z \in (𝒫 j \cap A) z Ref y) \to (⋃ j = ⋃ y \to \exists z \in (𝒫 j \cap B) z Ref y))$
5	4	ralimdv	$⊢ A \subseteq B \to (\forall y \in 𝒫 j (⋃ j = ⋃ y \to \exists z \in (𝒫 j \cap A) z Ref y) \to \forall y \in 𝒫 j (⋃ j = ⋃ y \to \exists z \in (𝒫 j \cap B) z Ref y))$
6	5	anim2d	$⊢ A \subseteq B \to ((j \in Top \land \forall y \in 𝒫 j (⋃ j = ⋃ y \to \exists z \in (𝒫 j \cap A) z Ref y)) \to (j \in Top \land \forall y \in 𝒫 j (⋃ j = ⋃ y \to \exists z \in (𝒫 j \cap B) z Ref y)))$
7		eqid	$⊢ ⋃ j = ⋃ j$
8	7	iscref	$⊢ j \in CovHasRef A \leftrightarrow (j \in Top \land \forall y \in 𝒫 j (⋃ j = ⋃ y \to \exists z \in (𝒫 j \cap A) z Ref y))$
9	7	iscref	$⊢ j \in CovHasRef B \leftrightarrow (j \in Top \land \forall y \in 𝒫 j (⋃ j = ⋃ y \to \exists z \in (𝒫 j \cap B) z Ref y))$
10	6 8 9	3imtr4g	$⊢ A \subseteq B \to (j \in CovHasRef A \to j \in CovHasRef B)$
11	10	ssrdv	$⊢ A \subseteq B \to CovHasRef A \subseteq CovHasRef B$

Metamath Proof Explorer