Metamath Proof Explorer

Theorem 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 ∈ A → φ
Assertion crefdf ⊢ J ∈ B ∧ C ⊆ J ∧ X = ⋃ C → ∃ z ∈ 𝒫 J φ ∧ z Ref C

Proof

Step Hyp Ref Expression
1 crefi.x ⊢ X = ⋃ J
2 crefdf.b ⊢ B = CovHasRef A
3 crefdf.p ⊢ z ∈ A → φ
4 2 eleq2i ⊢ J ∈ B ↔ J ∈ CovHasRef A
5 1 crefi ⊢ J ∈ CovHasRef A ∧ C ⊆ J ∧ X = ⋃ C → ∃ z ∈ 𝒫 J ∩ A z Ref C
6 4 5 syl3an1b ⊢ J ∈ B ∧ C ⊆ J ∧ X = ⋃ C → ∃ z ∈ 𝒫 J ∩ A z Ref C
7 elin ⊢ z ∈ 𝒫 J ∩ A ↔ z ∈ 𝒫 J ∧ z ∈ A
8 3 anim2i ⊢ z ∈ 𝒫 J ∧ z ∈ A → z ∈ 𝒫 J ∧ φ
9 7 8 sylbi ⊢ z ∈ 𝒫 J ∩ A → z ∈ 𝒫 J ∧ φ
10 9 anim1i ⊢ z ∈ 𝒫 J ∩ A ∧ z Ref C → z ∈ 𝒫 J ∧ φ ∧ z Ref C
11 anass ⊢ z ∈ 𝒫 J ∧ φ ∧ z Ref C ↔ z ∈ 𝒫 J ∧ φ ∧ z Ref C
12 10 11 sylib ⊢ z ∈ 𝒫 J ∩ A ∧ z Ref C → z ∈ 𝒫 J ∧ φ ∧ z Ref C
13 12 reximi2 ⊢ ∃ z ∈ 𝒫 J ∩ A z Ref C → ∃ z ∈ 𝒫 J φ ∧ z Ref C
14 6 13 syl ⊢ J ∈ B ∧ C ⊆ J ∧ X = ⋃ C → ∃ z ∈ 𝒫 J φ ∧ z Ref C