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

Metamath Proof Explorer

Theorem prtlem16

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

Ref Expression
Hypothesis prtlem13.1 
|- .~ = { <. x , y >. | E. u e. A ( x e. u /\ y e. u ) }
Assertion prtlem16 
|- dom .~ = U. A

Proof

Step Hyp Ref Expression
1 prtlem13.1 
 |-  .~ = { <. x , y >. | E. u e. A ( x e. u /\ y e. u ) }
2 vex 
 |-  z e. _V
3 2 eldm 
 |-  ( z e. dom .~ <-> E. w z .~ w )
4 1 prtlem13 
 |-  ( z .~ w <-> E. v e. A ( z e. v /\ w e. v ) )
5 4 exbii 
 |-  ( E. w z .~ w <-> E. w E. v e. A ( z e. v /\ w e. v ) )
6 elunii 
 |-  ( ( z e. v /\ v e. A ) -> z e. U. A )
7 6 ancoms 
 |-  ( ( v e. A /\ z e. v ) -> z e. U. A )
8 7 adantrr 
 |-  ( ( v e. A /\ ( z e. v /\ w e. v ) ) -> z e. U. A )
9 8 rexlimiva 
 |-  ( E. v e. A ( z e. v /\ w e. v ) -> z e. U. A )
10 9 exlimiv 
 |-  ( E. w E. v e. A ( z e. v /\ w e. v ) -> z e. U. A )
11 eluni2 
 |-  ( z e. U. A <-> E. v e. A z e. v )
12 elequ1 
 |-  ( w = z -> ( w e. v <-> z e. v ) )
13 12 anbi2d 
 |-  ( w = z -> ( ( z e. v /\ w e. v ) <-> ( z e. v /\ z e. v ) ) )
14 pm4.24 
 |-  ( z e. v <-> ( z e. v /\ z e. v ) )
15 13 14 bitr4di 
 |-  ( w = z -> ( ( z e. v /\ w e. v ) <-> z e. v ) )
16 15 rexbidv 
 |-  ( w = z -> ( E. v e. A ( z e. v /\ w e. v ) <-> E. v e. A z e. v ) )
17 2 16 spcev 
 |-  ( E. v e. A z e. v -> E. w E. v e. A ( z e. v /\ w e. v ) )
18 11 17 sylbi 
 |-  ( z e. U. A -> E. w E. v e. A ( z e. v /\ w e. v ) )
19 10 18 impbii 
 |-  ( E. w E. v e. A ( z e. v /\ w e. v ) <-> z e. U. A )
20 3 5 19 3bitri 
 |-  ( z e. dom .~ <-> z e. U. A )
21 20 eqriv 
 |-  dom .~ = U. A