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 = U. J
crefdf.b 
|- B = CovHasRef A
crefdf.p 
|- ( z e. A -> ph )
Assertion crefdf 
|- ( ( J e. B /\ C C_ J /\ X = U. C ) -> E. z e. ~P J ( ph /\ z Ref C ) )

Proof

Step Hyp Ref Expression
1 crefi.x 
 |-  X = U. J
2 crefdf.b 
 |-  B = CovHasRef A
3 crefdf.p 
 |-  ( z e. A -> ph )
4 2 eleq2i 
 |-  ( J e. B <-> J e. CovHasRef A )
5 1 crefi 
 |-  ( ( J e. CovHasRef A /\ C C_ J /\ X = U. C ) -> E. z e. ( ~P J i^i A ) z Ref C )
6 4 5 syl3an1b 
 |-  ( ( J e. B /\ C C_ J /\ X = U. C ) -> E. z e. ( ~P J i^i A ) z Ref C )
7 elin 
 |-  ( z e. ( ~P J i^i A ) <-> ( z e. ~P J /\ z e. A ) )
8 3 anim2i 
 |-  ( ( z e. ~P J /\ z e. A ) -> ( z e. ~P J /\ ph ) )
9 7 8 sylbi 
 |-  ( z e. ( ~P J i^i A ) -> ( z e. ~P J /\ ph ) )
10 9 anim1i 
 |-  ( ( z e. ( ~P J i^i A ) /\ z Ref C ) -> ( ( z e. ~P J /\ ph ) /\ z Ref C ) )
11 anass 
 |-  ( ( ( z e. ~P J /\ ph ) /\ z Ref C ) <-> ( z e. ~P J /\ ( ph /\ z Ref C ) ) )
12 10 11 sylib 
 |-  ( ( z e. ( ~P J i^i A ) /\ z Ref C ) -> ( z e. ~P J /\ ( ph /\ z Ref C ) ) )
13 12 reximi2 
 |-  ( E. z e. ( ~P J i^i A ) z Ref C -> E. z e. ~P J ( ph /\ z Ref C ) )
14 6 13 syl 
 |-  ( ( J e. B /\ C C_ J /\ X = U. C ) -> E. z e. ~P J ( ph /\ z Ref C ) )