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	$⊢ X = ⋃ J$
	Assertion	iscref	$⊢ J \in CovHasRef A \leftrightarrow (J \in Top \land \forall y \in 𝒫 J (X = ⋃ y \to \exists z \in (𝒫 J \cap A) z Ref y))$

Step	Hyp	Ref	Expression
1		iscref.x	$⊢ X = ⋃ J$
2		pweq	$⊢ j = J \to 𝒫 j = 𝒫 J$
3		unieq	$⊢ j = J \to ⋃ j = ⋃ J$
4	3 1	eqtr4di	$⊢ j = J \to ⋃ j = X$
5	4	eqeq1d	$⊢ j = J \to (⋃ j = ⋃ y \leftrightarrow X = ⋃ y)$
6	2	ineq1d	$⊢ j = J \to 𝒫 j \cap A = 𝒫 J \cap A$
7	6	rexeqdv	$⊢ j = J \to (\exists z \in (𝒫 j \cap A) z Ref y \leftrightarrow \exists z \in (𝒫 J \cap A) z Ref y)$
8	5 7	imbi12d	$⊢ j = J \to ((⋃ j = ⋃ y \to \exists z \in (𝒫 j \cap A) z Ref y) \leftrightarrow (X = ⋃ y \to \exists z \in (𝒫 J \cap A) z Ref y))$
9	2 8	raleqbidv	$⊢ j = J \to (\forall y \in 𝒫 j (⋃ j = ⋃ y \to \exists z \in (𝒫 j \cap A) z Ref y) \leftrightarrow \forall y \in 𝒫 J (X = ⋃ y \to \exists z \in (𝒫 J \cap A) z Ref y))$
10		df-cref	$⊢ CovHasRef A = \{j \in Top \| \forall y \in 𝒫 j (⋃ j = ⋃ y \to \exists z \in (𝒫 j \cap A) z Ref y)\}$
11	9 10	elrab2	$⊢ J \in CovHasRef A \leftrightarrow (J \in Top \land \forall y \in 𝒫 J (X = ⋃ y \to \exists z \in (𝒫 J \cap A) z Ref y))$

Metamath Proof Explorer