Theorem crefdf

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

	Ref	Expression
Hypotheses	crefi.x	⊢ 𝑋 = ∪ 𝐽
	crefdf.b	⊢ 𝐵 = CovHasRef 𝐴
	crefdf.p	⊢ ( 𝑧 ∈ 𝐴 → 𝜑 )
Assertion	crefdf	⊢ ( ( 𝐽 ∈ 𝐵 ∧ 𝐶 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝐶 ) → ∃ 𝑧 ∈ 𝒫 𝐽 ( 𝜑 ∧ 𝑧 Ref 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		crefi.x	⊢ 𝑋 = ∪ 𝐽
2		crefdf.b	⊢ 𝐵 = CovHasRef 𝐴
3		crefdf.p	⊢ ( 𝑧 ∈ 𝐴 → 𝜑 )
4	2	eleq2i	⊢ ( 𝐽 ∈ 𝐵 ↔ 𝐽 ∈ CovHasRef 𝐴 )
5	1	crefi	⊢ ( ( 𝐽 ∈ CovHasRef 𝐴 ∧ 𝐶 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝐶 ) → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ 𝐴 ) 𝑧 Ref 𝐶 )
6	4 5	syl3an1b	⊢ ( ( 𝐽 ∈ 𝐵 ∧ 𝐶 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝐶 ) → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ 𝐴 ) 𝑧 Ref 𝐶 )
7		elin	⊢ ( 𝑧 ∈ ( 𝒫 𝐽 ∩ 𝐴 ) ↔ ( 𝑧 ∈ 𝒫 𝐽 ∧ 𝑧 ∈ 𝐴 ) )
8	3	anim2i	⊢ ( ( 𝑧 ∈ 𝒫 𝐽 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑧 ∈ 𝒫 𝐽 ∧ 𝜑 ) )
9	7 8	sylbi	⊢ ( 𝑧 ∈ ( 𝒫 𝐽 ∩ 𝐴 ) → ( 𝑧 ∈ 𝒫 𝐽 ∧ 𝜑 ) )
10	9	anim1i	⊢ ( ( 𝑧 ∈ ( 𝒫 𝐽 ∩ 𝐴 ) ∧ 𝑧 Ref 𝐶 ) → ( ( 𝑧 ∈ 𝒫 𝐽 ∧ 𝜑 ) ∧ 𝑧 Ref 𝐶 ) )
11		anass	⊢ ( ( ( 𝑧 ∈ 𝒫 𝐽 ∧ 𝜑 ) ∧ 𝑧 Ref 𝐶 ) ↔ ( 𝑧 ∈ 𝒫 𝐽 ∧ ( 𝜑 ∧ 𝑧 Ref 𝐶 ) ) )
12	10 11	sylib	⊢ ( ( 𝑧 ∈ ( 𝒫 𝐽 ∩ 𝐴 ) ∧ 𝑧 Ref 𝐶 ) → ( 𝑧 ∈ 𝒫 𝐽 ∧ ( 𝜑 ∧ 𝑧 Ref 𝐶 ) ) )
13	12	reximi2	⊢ ( ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ 𝐴 ) 𝑧 Ref 𝐶 → ∃ 𝑧 ∈ 𝒫 𝐽 ( 𝜑 ∧ 𝑧 Ref 𝐶 ) )
14	6 13	syl	⊢ ( ( 𝐽 ∈ 𝐵 ∧ 𝐶 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝐶 ) → ∃ 𝑧 ∈ 𝒫 𝐽 ( 𝜑 ∧ 𝑧 Ref 𝐶 ) )