Metamath Proof Explorer


Theorem prter2

Description: The quotient set of the equivalence relation generated by a partition equals the partition itself. (Contributed by Rodolfo Medina, 17-Oct-2010)

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

Proof

Step Hyp Ref Expression
1 prtlem18.1
 |-  .~ = { <. x , y >. | E. u e. A ( x e. u /\ y e. u ) }
2 rexcom4
 |-  ( E. v e. A E. z ( z e. v /\ p = [ z ] .~ ) <-> E. z E. v e. A ( z e. v /\ p = [ z ] .~ ) )
3 r19.41v
 |-  ( E. v e. A ( z e. v /\ p = [ z ] .~ ) <-> ( E. v e. A z e. v /\ p = [ z ] .~ ) )
4 3 exbii
 |-  ( E. z E. v e. A ( z e. v /\ p = [ z ] .~ ) <-> E. z ( E. v e. A z e. v /\ p = [ z ] .~ ) )
5 2 4 bitri
 |-  ( E. v e. A E. z ( z e. v /\ p = [ z ] .~ ) <-> E. z ( E. v e. A z e. v /\ p = [ z ] .~ ) )
6 df-rex
 |-  ( E. z e. v p = [ z ] .~ <-> E. z ( z e. v /\ p = [ z ] .~ ) )
7 6 rexbii
 |-  ( E. v e. A E. z e. v p = [ z ] .~ <-> E. v e. A E. z ( z e. v /\ p = [ z ] .~ ) )
8 vex
 |-  p e. _V
9 8 elqs
 |-  ( p e. ( U. A /. .~ ) <-> E. z e. U. A p = [ z ] .~ )
10 df-rex
 |-  ( E. z e. U. A p = [ z ] .~ <-> E. z ( z e. U. A /\ p = [ z ] .~ ) )
11 eluni2
 |-  ( z e. U. A <-> E. v e. A z e. v )
12 11 anbi1i
 |-  ( ( z e. U. A /\ p = [ z ] .~ ) <-> ( E. v e. A z e. v /\ p = [ z ] .~ ) )
13 12 exbii
 |-  ( E. z ( z e. U. A /\ p = [ z ] .~ ) <-> E. z ( E. v e. A z e. v /\ p = [ z ] .~ ) )
14 10 13 bitri
 |-  ( E. z e. U. A p = [ z ] .~ <-> E. z ( E. v e. A z e. v /\ p = [ z ] .~ ) )
15 9 14 bitri
 |-  ( p e. ( U. A /. .~ ) <-> E. z ( E. v e. A z e. v /\ p = [ z ] .~ ) )
16 5 7 15 3bitr4ri
 |-  ( p e. ( U. A /. .~ ) <-> E. v e. A E. z e. v p = [ z ] .~ )
17 1 prtlem19
 |-  ( Prt A -> ( ( v e. A /\ z e. v ) -> v = [ z ] .~ ) )
18 17 ralrimivv
 |-  ( Prt A -> A. v e. A A. z e. v v = [ z ] .~ )
19 2r19.29
 |-  ( ( A. v e. A A. z e. v v = [ z ] .~ /\ E. v e. A E. z e. v p = [ z ] .~ ) -> E. v e. A E. z e. v ( v = [ z ] .~ /\ p = [ z ] .~ ) )
20 19 ex
 |-  ( A. v e. A A. z e. v v = [ z ] .~ -> ( E. v e. A E. z e. v p = [ z ] .~ -> E. v e. A E. z e. v ( v = [ z ] .~ /\ p = [ z ] .~ ) ) )
21 18 20 syl
 |-  ( Prt A -> ( E. v e. A E. z e. v p = [ z ] .~ -> E. v e. A E. z e. v ( v = [ z ] .~ /\ p = [ z ] .~ ) ) )
22 16 21 syl5bi
 |-  ( Prt A -> ( p e. ( U. A /. .~ ) -> E. v e. A E. z e. v ( v = [ z ] .~ /\ p = [ z ] .~ ) ) )
23 eqtr3
 |-  ( ( v = [ z ] .~ /\ p = [ z ] .~ ) -> v = p )
24 23 reximi
 |-  ( E. z e. v ( v = [ z ] .~ /\ p = [ z ] .~ ) -> E. z e. v v = p )
25 24 reximi
 |-  ( E. v e. A E. z e. v ( v = [ z ] .~ /\ p = [ z ] .~ ) -> E. v e. A E. z e. v v = p )
26 22 25 syl6
 |-  ( Prt A -> ( p e. ( U. A /. .~ ) -> E. v e. A E. z e. v v = p ) )
27 df-rex
 |-  ( E. z e. v v = p <-> E. z ( z e. v /\ v = p ) )
28 19.41v
 |-  ( E. z ( z e. v /\ v = p ) <-> ( E. z z e. v /\ v = p ) )
29 27 28 bitri
 |-  ( E. z e. v v = p <-> ( E. z z e. v /\ v = p ) )
30 29 simprbi
 |-  ( E. z e. v v = p -> v = p )
31 30 reximi
 |-  ( E. v e. A E. z e. v v = p -> E. v e. A v = p )
32 26 31 syl6
 |-  ( Prt A -> ( p e. ( U. A /. .~ ) -> E. v e. A v = p ) )
33 risset
 |-  ( p e. A <-> E. v e. A v = p )
34 32 33 syl6ibr
 |-  ( Prt A -> ( p e. ( U. A /. .~ ) -> p e. A ) )
35 1 prtlem400
 |-  -. (/) e. ( U. A /. .~ )
36 nelelne
 |-  ( -. (/) e. ( U. A /. .~ ) -> ( p e. ( U. A /. .~ ) -> p =/= (/) ) )
37 35 36 mp1i
 |-  ( Prt A -> ( p e. ( U. A /. .~ ) -> p =/= (/) ) )
38 34 37 jcad
 |-  ( Prt A -> ( p e. ( U. A /. .~ ) -> ( p e. A /\ p =/= (/) ) ) )
39 eldifsn
 |-  ( p e. ( A \ { (/) } ) <-> ( p e. A /\ p =/= (/) ) )
40 38 39 syl6ibr
 |-  ( Prt A -> ( p e. ( U. A /. .~ ) -> p e. ( A \ { (/) } ) ) )
41 neldifsn
 |-  -. (/) e. ( A \ { (/) } )
42 n0el
 |-  ( -. (/) e. ( A \ { (/) } ) <-> A. p e. ( A \ { (/) } ) E. z z e. p )
43 41 42 mpbi
 |-  A. p e. ( A \ { (/) } ) E. z z e. p
44 43 rspec
 |-  ( p e. ( A \ { (/) } ) -> E. z z e. p )
45 eldifi
 |-  ( p e. ( A \ { (/) } ) -> p e. A )
46 44 45 jca
 |-  ( p e. ( A \ { (/) } ) -> ( E. z z e. p /\ p e. A ) )
47 1 prtlem19
 |-  ( Prt A -> ( ( p e. A /\ z e. p ) -> p = [ z ] .~ ) )
48 47 ancomsd
 |-  ( Prt A -> ( ( z e. p /\ p e. A ) -> p = [ z ] .~ ) )
49 elunii
 |-  ( ( z e. p /\ p e. A ) -> z e. U. A )
50 48 49 jca2r
 |-  ( Prt A -> ( ( z e. p /\ p e. A ) -> ( z e. U. A /\ p = [ z ] .~ ) ) )
51 prtlem11
 |-  ( p e. _V -> ( z e. U. A -> ( p = [ z ] .~ -> p e. ( U. A /. .~ ) ) ) )
52 51 elv
 |-  ( z e. U. A -> ( p = [ z ] .~ -> p e. ( U. A /. .~ ) ) )
53 52 imp
 |-  ( ( z e. U. A /\ p = [ z ] .~ ) -> p e. ( U. A /. .~ ) )
54 50 53 syl6
 |-  ( Prt A -> ( ( z e. p /\ p e. A ) -> p e. ( U. A /. .~ ) ) )
55 54 eximdv
 |-  ( Prt A -> ( E. z ( z e. p /\ p e. A ) -> E. z p e. ( U. A /. .~ ) ) )
56 19.41v
 |-  ( E. z ( z e. p /\ p e. A ) <-> ( E. z z e. p /\ p e. A ) )
57 19.9v
 |-  ( E. z p e. ( U. A /. .~ ) <-> p e. ( U. A /. .~ ) )
58 55 56 57 3imtr3g
 |-  ( Prt A -> ( ( E. z z e. p /\ p e. A ) -> p e. ( U. A /. .~ ) ) )
59 46 58 syl5
 |-  ( Prt A -> ( p e. ( A \ { (/) } ) -> p e. ( U. A /. .~ ) ) )
60 40 59 impbid
 |-  ( Prt A -> ( p e. ( U. A /. .~ ) <-> p e. ( A \ { (/) } ) ) )
61 60 eqrdv
 |-  ( Prt A -> ( U. A /. .~ ) = ( A \ { (/) } ) )