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 | u A x u y u
Assertion prtlem16 dom ˙ = A

Proof

Step Hyp Ref Expression
1 prtlem13.1 ˙ = x y | u A x u y u
2 vex z V
3 2 eldm z dom ˙ w z ˙ w
4 1 prtlem13 z ˙ w v A z v w v
5 4 exbii w z ˙ w w v A z v w v
6 elunii z v v A z A
7 6 ancoms v A z v z A
8 7 adantrr v A z v w v z A
9 8 rexlimiva v A z v w v z A
10 9 exlimiv w v A z v w v z A
11 eluni2 z A v A z v
12 elequ1 w = z w v z v
13 12 anbi2d w = z z v w v z v z v
14 pm4.24 z v z v z v
15 13 14 bitr4di w = z z v w v z v
16 15 rexbidv w = z v A z v w v v A z v
17 2 16 spcev v A z v w v A z v w v
18 11 17 sylbi z A w v A z v w v
19 10 18 impbii w v A z v w v z A
20 3 5 19 3bitri z dom ˙ z A
21 20 eqriv dom ˙ = A