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

Metamath Proof Explorer

Theorem prtlem15

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

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

Proof

Step Hyp Ref Expression
1 anabs7 
 |-  ( ( ( w e. x /\ w e. y ) /\ ( ( u e. x /\ v e. y ) /\ ( w e. x /\ w e. y ) ) ) <-> ( ( u e. x /\ v e. y ) /\ ( w e. x /\ w e. y ) ) )
2 an43 
 |-  ( ( ( u e. x /\ w e. x ) /\ ( w e. y /\ v e. y ) ) <-> ( ( u e. x /\ v e. y ) /\ ( w e. x /\ w e. y ) ) )
3 2 anbi2i 
 |-  ( ( ( w e. x /\ w e. y ) /\ ( ( u e. x /\ w e. x ) /\ ( w e. y /\ v e. y ) ) ) <-> ( ( w e. x /\ w e. y ) /\ ( ( u e. x /\ v e. y ) /\ ( w e. x /\ w e. y ) ) ) )
4 1 3 2 3bitr4ri 
 |-  ( ( ( u e. x /\ w e. x ) /\ ( w e. y /\ v e. y ) ) <-> ( ( w e. x /\ w e. y ) /\ ( ( u e. x /\ w e. x ) /\ ( w e. y /\ v e. y ) ) ) )
5 prtlem14 
 |-  ( Prt A -> ( ( x e. A /\ y e. A ) -> ( ( w e. x /\ w e. y ) -> x = y ) ) )
6 an3 
 |-  ( ( ( u e. x /\ w e. x ) /\ ( w e. y /\ v e. y ) ) -> ( u e. x /\ v e. y ) )
7 elequ2 
 |-  ( x = y -> ( v e. x <-> v e. y ) )
8 7 anbi2d 
 |-  ( x = y -> ( ( u e. x /\ v e. x ) <-> ( u e. x /\ v e. y ) ) )
9 6 8 imbitrrid 
 |-  ( x = y -> ( ( ( u e. x /\ w e. x ) /\ ( w e. y /\ v e. y ) ) -> ( u e. x /\ v e. x ) ) )
10 5 9 syl8 
 |-  ( Prt A -> ( ( x e. A /\ y e. A ) -> ( ( w e. x /\ w e. y ) -> ( ( ( u e. x /\ w e. x ) /\ ( w e. y /\ v e. y ) ) -> ( u e. x /\ v e. x ) ) ) ) )
11 10 imp4a 
 |-  ( Prt A -> ( ( x e. A /\ y e. A ) -> ( ( ( w e. x /\ w e. y ) /\ ( ( u e. x /\ w e. x ) /\ ( w e. y /\ v e. y ) ) ) -> ( u e. x /\ v e. x ) ) ) )
12 4 11 syl7bi 
 |-  ( Prt A -> ( ( x e. A /\ y e. A ) -> ( ( ( u e. x /\ w e. x ) /\ ( w e. y /\ v e. y ) ) -> ( u e. x /\ v e. x ) ) ) )
13 12 expdimp 
 |-  ( ( Prt A /\ x e. A ) -> ( y e. A -> ( ( ( u e. x /\ w e. x ) /\ ( w e. y /\ v e. y ) ) -> ( u e. x /\ v e. x ) ) ) )
14 13 rexlimdv 
 |-  ( ( Prt A /\ x e. A ) -> ( E. y e. A ( ( u e. x /\ w e. x ) /\ ( w e. y /\ v e. y ) ) -> ( u e. x /\ v e. x ) ) )
15 14 reximdva 
 |-  ( Prt A -> ( E. x e. A E. y e. A ( ( u e. x /\ w e. x ) /\ ( w e. y /\ v e. y ) ) -> E. x e. A ( u e. x /\ v e. x ) ) )
16 elequ2 
 |-  ( x = z -> ( u e. x <-> u e. z ) )
17 elequ2 
 |-  ( x = z -> ( v e. x <-> v e. z ) )
18 16 17 anbi12d 
 |-  ( x = z -> ( ( u e. x /\ v e. x ) <-> ( u e. z /\ v e. z ) ) )
19 18 cbvrexvw 
 |-  ( E. x e. A ( u e. x /\ v e. x ) <-> E. z e. A ( u e. z /\ v e. z ) )
20 15 19 imbitrdi 
 |-  ( Prt A -> ( E. x e. A E. y e. A ( ( u e. x /\ w e. x ) /\ ( w e. y /\ v e. y ) ) -> E. z e. A ( u e. z /\ v e. z ) ) )