This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prtlem14

Description: Lemma for prter1 , prter2 and prtex . (Contributed by Rodolfo Medina, 13-Oct-2010)

Ref Expression
Assertion prtlem14 
|- ( Prt A -> ( ( x e. A /\ y e. A ) -> ( ( w e. x /\ w e. y ) -> x = y ) ) )

Proof

Step Hyp Ref Expression
1 df-prt 
 |-  ( Prt A <-> A. x e. A A. y e. A ( x = y \/ ( x i^i y ) = (/) ) )
2 rsp2 
 |-  ( A. x e. A A. y e. A ( x = y \/ ( x i^i y ) = (/) ) -> ( ( x e. A /\ y e. A ) -> ( x = y \/ ( x i^i y ) = (/) ) ) )
3 1 2 sylbi 
 |-  ( Prt A -> ( ( x e. A /\ y e. A ) -> ( x = y \/ ( x i^i y ) = (/) ) ) )
4 elin 
 |-  ( w e. ( x i^i y ) <-> ( w e. x /\ w e. y ) )
5 eq0 
 |-  ( ( x i^i y ) = (/) <-> A. w -. w e. ( x i^i y ) )
6 sp 
 |-  ( A. w -. w e. ( x i^i y ) -> -. w e. ( x i^i y ) )
7 5 6 sylbi 
 |-  ( ( x i^i y ) = (/) -> -. w e. ( x i^i y ) )
8 7 pm2.21d 
 |-  ( ( x i^i y ) = (/) -> ( w e. ( x i^i y ) -> x = y ) )
9 4 8 biimtrrid 
 |-  ( ( x i^i y ) = (/) -> ( ( w e. x /\ w e. y ) -> x = y ) )
10 9 jao1i 
 |-  ( ( x = y \/ ( x i^i y ) = (/) ) -> ( ( w e. x /\ w e. y ) -> x = y ) )
11 3 10 syl6 
 |-  ( Prt A -> ( ( x e. A /\ y e. A ) -> ( ( w e. x /\ w e. y ) -> x = y ) ) )