crefdf

Description: A formulation of crefi easier to use for definitions. (Contributed by Thierry Arnoux, 7-Jan-2020)

	Ref	Expression
Hypotheses	crefi.x	$⊢ X = ⋃ J$
	crefdf.b	$⊢ B = CovHasRef A$
	crefdf.p	$⊢ z \in A \to φ$
Assertion	crefdf	$⊢ (J \in B \land C \subseteq J \land X = ⋃ C) \to \exists z \in 𝒫 J (φ \land z Ref C)$

Step	Hyp	Ref	Expression
1		crefi.x	$⊢ X = ⋃ J$
2		crefdf.b	$⊢ B = CovHasRef A$
3		crefdf.p	$⊢ z \in A \to φ$
4	2	eleq2i	$⊢ J \in B \leftrightarrow J \in CovHasRef A$
5	1	crefi	$⊢ (J \in CovHasRef A \land C \subseteq J \land X = ⋃ C) \to \exists z \in (𝒫 J \cap A) z Ref C$
6	4 5	syl3an1b	$⊢ (J \in B \land C \subseteq J \land X = ⋃ C) \to \exists z \in (𝒫 J \cap A) z Ref C$
7		elin	$⊢ z \in (𝒫 J \cap A) \leftrightarrow (z \in 𝒫 J \land z \in A)$
8	3	anim2i	$⊢ (z \in 𝒫 J \land z \in A) \to (z \in 𝒫 J \land φ)$
9	7 8	sylbi	$⊢ z \in (𝒫 J \cap A) \to (z \in 𝒫 J \land φ)$
10	9	anim1i	$⊢ (z \in (𝒫 J \cap A) \land z Ref C) \to ((z \in 𝒫 J \land φ) \land z Ref C)$
11		anass	$⊢ ((z \in 𝒫 J \land φ) \land z Ref C) \leftrightarrow (z \in 𝒫 J \land (φ \land z Ref C))$
12	10 11	sylib	$⊢ (z \in (𝒫 J \cap A) \land z Ref C) \to (z \in 𝒫 J \land (φ \land z Ref C))$
13	12	reximi2	$⊢ \exists z \in (𝒫 J \cap A) z Ref C \to \exists z \in 𝒫 J (φ \land z Ref C)$
14	6 13	syl	$⊢ (J \in B \land C \subseteq J \land X = ⋃ C) \to \exists z \in 𝒫 J (φ \land z Ref C)$

Metamath Proof Explorer