Metamath Proof Explorer


Theorem prter3

Description: For every partition there exists a unique equivalence relation whose quotient set equals the partition. (Contributed by Rodolfo Medina, 19-Oct-2010) (Proof shortened by Mario Carneiro, 12-Aug-2015)

Ref Expression
Hypothesis prtlem18.1 ˙ = x y | u A x u y u
Assertion prter3 S Er A A / S = A ˙ = S

Proof

Step Hyp Ref Expression
1 prtlem18.1 ˙ = x y | u A x u y u
2 errel S Er A Rel S
3 2 adantr S Er A A / S = A Rel S
4 1 relopabiv Rel ˙
5 1 prtlem13 z ˙ w v A z v w v
6 simpll S Er A A / S = A v A z v S Er A
7 simprl S Er A A / S = A v A z v v A
8 ne0i z v v
9 8 ad2antll S Er A A / S = A v A z v v
10 eldifsn v A v A v
11 7 9 10 sylanbrc S Er A A / S = A v A z v v A
12 simplr S Er A A / S = A v A z v A / S = A
13 11 12 eleqtrrd S Er A A / S = A v A z v v A / S
14 simprr S Er A A / S = A v A z v z v
15 qsel S Er A v A / S z v v = z S
16 6 13 14 15 syl3anc S Er A A / S = A v A z v v = z S
17 16 eleq2d S Er A A / S = A v A z v w v w z S
18 vex w V
19 vex z V
20 18 19 elec w z S z S w
21 17 20 bitrdi S Er A A / S = A v A z v w v z S w
22 21 anassrs S Er A A / S = A v A z v w v z S w
23 22 pm5.32da S Er A A / S = A v A z v w v z v z S w
24 23 rexbidva S Er A A / S = A v A z v w v v A z v z S w
25 simpll S Er A A / S = A z S w S Er A
26 simpr S Er A A / S = A z S w z S w
27 25 26 ercl S Er A A / S = A z S w z A
28 eluni2 z A v A z v
29 27 28 sylib S Er A A / S = A z S w v A z v
30 29 ex S Er A A / S = A z S w v A z v
31 30 pm4.71rd S Er A A / S = A z S w v A z v z S w
32 r19.41v v A z v z S w v A z v z S w
33 31 32 bitr4di S Er A A / S = A z S w v A z v z S w
34 24 33 bitr4d S Er A A / S = A v A z v w v z S w
35 5 34 syl5bb S Er A A / S = A z ˙ w z S w
36 35 adantl Rel ˙ Rel S S Er A A / S = A z ˙ w z S w
37 36 eqbrrdv2 Rel ˙ Rel S S Er A A / S = A ˙ = S
38 4 37 mpanl1 Rel S S Er A A / S = A ˙ = S
39 3 38 mpancom S Er A A / S = A ˙ = S