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

Metamath Proof Explorer

Theorem prter1

Description: Every partition generates an equivalence relation. (Contributed by Rodolfo Medina, 13-Oct-2010) (Revised by Mario Carneiro, 12-Aug-2015)

Ref Expression
Hypothesis prtlem18.1 
|- .~ = { <. x , y >. | E. u e. A ( x e. u /\ y e. u ) }
Assertion prter1 
|- ( Prt A -> .~ Er U. A )

Proof

Step Hyp Ref Expression
1 prtlem18.1 
 |-  .~ = { <. x , y >. | E. u e. A ( x e. u /\ y e. u ) }
2 1 relopabiv 
 |-  Rel .~
3 2 a1i 
 |-  ( Prt A -> Rel .~ )
4 1 prtlem16 
 |-  dom .~ = U. A
5 4 a1i 
 |-  ( Prt A -> dom .~ = U. A )
6 prtlem15 
 |-  ( Prt A -> ( E. v e. A E. q e. A ( ( z e. v /\ w e. v ) /\ ( w e. q /\ p e. q ) ) -> E. r e. A ( z e. r /\ p e. r ) ) )
7 1 prtlem13 
 |-  ( z .~ w <-> E. v e. A ( z e. v /\ w e. v ) )
8 1 prtlem13 
 |-  ( w .~ p <-> E. q e. A ( w e. q /\ p e. q ) )
9 7 8 anbi12i 
 |-  ( ( z .~ w /\ w .~ p ) <-> ( E. v e. A ( z e. v /\ w e. v ) /\ E. q e. A ( w e. q /\ p e. q ) ) )
10 reeanv 
 |-  ( E. v e. A E. q e. A ( ( z e. v /\ w e. v ) /\ ( w e. q /\ p e. q ) ) <-> ( E. v e. A ( z e. v /\ w e. v ) /\ E. q e. A ( w e. q /\ p e. q ) ) )
11 9 10 bitr4i 
 |-  ( ( z .~ w /\ w .~ p ) <-> E. v e. A E. q e. A ( ( z e. v /\ w e. v ) /\ ( w e. q /\ p e. q ) ) )
12 1 prtlem13 
 |-  ( z .~ p <-> E. r e. A ( z e. r /\ p e. r ) )
13 6 11 12 3imtr4g 
 |-  ( Prt A -> ( ( z .~ w /\ w .~ p ) -> z .~ p ) )
14 pm3.22 
 |-  ( ( z e. v /\ w e. v ) -> ( w e. v /\ z e. v ) )
15 14 reximi 
 |-  ( E. v e. A ( z e. v /\ w e. v ) -> E. v e. A ( w e. v /\ z e. v ) )
16 1 prtlem13 
 |-  ( w .~ z <-> E. v e. A ( w e. v /\ z e. v ) )
17 15 7 16 3imtr4i 
 |-  ( z .~ w -> w .~ z )
18 13 17 jctil 
 |-  ( Prt A -> ( ( z .~ w -> w .~ z ) /\ ( ( z .~ w /\ w .~ p ) -> z .~ p ) ) )
19 18 alrimivv 
 |-  ( Prt A -> A. w A. p ( ( z .~ w -> w .~ z ) /\ ( ( z .~ w /\ w .~ p ) -> z .~ p ) ) )
20 19 alrimiv 
 |-  ( Prt A -> A. z A. w A. p ( ( z .~ w -> w .~ z ) /\ ( ( z .~ w /\ w .~ p ) -> z .~ p ) ) )
21 dfer2 
 |-  ( .~ Er U. A <-> ( Rel .~ /\ dom .~ = U. A /\ A. z A. w A. p ( ( z .~ w -> w .~ z ) /\ ( ( z .~ w /\ w .~ p ) -> z .~ p ) ) ) )
22 3 5 20 21 syl3anbrc 
 |-  ( Prt A -> .~ Er U. A )