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 \in CovHasRef A \land C \subseteq J \land X = ⋃ C) \to \exists z \in (𝒫 J \cap A) z Ref C$

Proof

Step	Hyp	Ref	Expression
1		crefi.x	$⊢ X = ⋃ J$
2		simp1	$⊢ (J \in CovHasRef A \land C \subseteq J \land X = ⋃ C) \to J \in CovHasRef A$
3		simp2	$⊢ (J \in CovHasRef A \land C \subseteq J \land X = ⋃ C) \to C \subseteq J$
4	2 3	sselpwd	$⊢ (J \in CovHasRef A \land C \subseteq J \land X = ⋃ C) \to C \in 𝒫 J$
5	1	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))$
6	5	simprbi	$⊢ J \in CovHasRef A \to \forall y \in 𝒫 J (X = ⋃ y \to \exists z \in (𝒫 J \cap A) z Ref y)$
7	6	3ad2ant1	$⊢ (J \in CovHasRef A \land C \subseteq J \land X = ⋃ C) \to \forall y \in 𝒫 J (X = ⋃ y \to \exists z \in (𝒫 J \cap A) z Ref y)$
8		simp3	$⊢ (J \in CovHasRef A \land C \subseteq J \land X = ⋃ C) \to X = ⋃ C$
9		unieq	$⊢ y = C \to ⋃ y = ⋃ C$
10	9	eqeq2d	$⊢ y = C \to (X = ⋃ y \leftrightarrow X = ⋃ C)$
11		breq2	$⊢ y = C \to (z Ref y \leftrightarrow z Ref C)$
12	11	rexbidv	$⊢ y = C \to (\exists z \in (𝒫 J \cap A) z Ref y \leftrightarrow \exists z \in (𝒫 J \cap A) z Ref C)$
13	10 12	imbi12d	$⊢ y = C \to ((X = ⋃ y \to \exists z \in (𝒫 J \cap A) z Ref y) \leftrightarrow (X = ⋃ C \to \exists z \in (𝒫 J \cap A) z Ref C))$
14	13	rspcv	$⊢ C \in 𝒫 J \to (\forall y \in 𝒫 J (X = ⋃ y \to \exists z \in (𝒫 J \cap A) z Ref y) \to (X = ⋃ C \to \exists z \in (𝒫 J \cap A) z Ref C))$
15	4 7 8 14	syl3c	$⊢ (J \in CovHasRef A \land C \subseteq J \land X = ⋃ C) \to \exists z \in (𝒫 J \cap A) z Ref C$