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