Metamath Proof Explorer

Theorem prtlem17

Description: Lemma for prter2 . (Contributed by Rodolfo Medina, 15-Oct-2010)

Ref Expression
Assertion prtlem17 
|- ( Prt A -> ( ( x e. A /\ z e. x ) -> ( E. y e. A ( z e. y /\ w e. y ) -> w e. x ) ) )

Proof

Step Hyp Ref Expression
1 df-rex 
 |-  ( E. y e. A ( z e. y /\ w e. y ) <-> E. y ( y e. A /\ ( z e. y /\ w e. y ) ) )
2 an32 
 |-  ( ( ( x e. A /\ y e. A ) /\ z e. x ) <-> ( ( x e. A /\ z e. x ) /\ y e. A ) )
3 prtlem14 
 |-  ( Prt A -> ( ( x e. A /\ y e. A ) -> ( ( z e. x /\ z e. y ) -> x = y ) ) )
4 elequ2 
 |-  ( x = y -> ( w e. x <-> w e. y ) )
5 4 biimprd 
 |-  ( x = y -> ( w e. y -> w e. x ) )
6 3 5 syl8 
 |-  ( Prt A -> ( ( x e. A /\ y e. A ) -> ( ( z e. x /\ z e. y ) -> ( w e. y -> w e. x ) ) ) )
7 6 exp4a 
 |-  ( Prt A -> ( ( x e. A /\ y e. A ) -> ( z e. x -> ( z e. y -> ( w e. y -> w e. x ) ) ) ) )
8 7 impd 
 |-  ( Prt A -> ( ( ( x e. A /\ y e. A ) /\ z e. x ) -> ( z e. y -> ( w e. y -> w e. x ) ) ) )
9 2 8 syl5bir 
 |-  ( Prt A -> ( ( ( x e. A /\ z e. x ) /\ y e. A ) -> ( z e. y -> ( w e. y -> w e. x ) ) ) )
10 9 expd 
 |-  ( Prt A -> ( ( x e. A /\ z e. x ) -> ( y e. A -> ( z e. y -> ( w e. y -> w e. x ) ) ) ) )
11 10 imp5a 
 |-  ( Prt A -> ( ( x e. A /\ z e. x ) -> ( y e. A -> ( ( z e. y /\ w e. y ) -> w e. x ) ) ) )
12 11 imp4b 
 |-  ( ( Prt A /\ ( x e. A /\ z e. x ) ) -> ( ( y e. A /\ ( z e. y /\ w e. y ) ) -> w e. x ) )
13 12 exlimdv 
 |-  ( ( Prt A /\ ( x e. A /\ z e. x ) ) -> ( E. y ( y e. A /\ ( z e. y /\ w e. y ) ) -> w e. x ) )
14 1 13 syl5bi 
 |-  ( ( Prt A /\ ( x e. A /\ z e. x ) ) -> ( E. y e. A ( z e. y /\ w e. y ) -> w e. x ) )
15 14 ex 
 |-  ( Prt A -> ( ( x e. A /\ z e. x ) -> ( E. y e. A ( z e. y /\ w e. y ) -> w e. x ) ) )