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	syl5bir	|- ( ( 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 ) ) )