Metamath Proof Explorer

Theorem prtlem18

Description: Lemma for prter2 . (Contributed by Rodolfo Medina, 15-Oct-2010) (Revised by Mario Carneiro, 12-Aug-2015)

Ref Expression
Hypothesis prtlem18.1 
|- .~ = { <. x , y >. | E. u e. A ( x e. u /\ y e. u ) }
Assertion prtlem18 
|- ( Prt A -> ( ( v e. A /\ z e. v ) -> ( w e. v <-> z .~ w ) ) )

Proof

Step Hyp Ref Expression
1 prtlem18.1 
 |-  .~ = { <. x , y >. | E. u e. A ( x e. u /\ y e. u ) }
2 rspe 
 |-  ( ( v e. A /\ ( z e. v /\ w e. v ) ) -> E. v e. A ( z e. v /\ w e. v ) )
3 2 expr 
 |-  ( ( v e. A /\ z e. v ) -> ( w e. v -> E. v e. A ( z e. v /\ w e. v ) ) )
4 1 prtlem13 
 |-  ( z .~ w <-> E. v e. A ( z e. v /\ w e. v ) )
5 3 4 imbitrrdi 
 |-  ( ( v e. A /\ z e. v ) -> ( w e. v -> z .~ w ) )
6 5 a1i 
 |-  ( Prt A -> ( ( v e. A /\ z e. v ) -> ( w e. v -> z .~ w ) ) )
7 1 prtlem13 
 |-  ( z .~ w <-> E. p e. A ( z e. p /\ w e. p ) )
8 prtlem17 
 |-  ( Prt A -> ( ( v e. A /\ z e. v ) -> ( E. p e. A ( z e. p /\ w e. p ) -> w e. v ) ) )
9 7 8 syl7bi 
 |-  ( Prt A -> ( ( v e. A /\ z e. v ) -> ( z .~ w -> w e. v ) ) )
10 6 9 impbidd 
 |-  ( Prt A -> ( ( v e. A /\ z e. v ) -> ( w e. v <-> z .~ w ) ) )