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 >. | E. u e. A ( x e. u /\ y e. u ) }
Assertion prter3 
|- ( ( S Er U. A /\ ( U. A /. S ) = ( A \ { (/) } ) ) -> .~ = S )

Proof

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