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

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 biimtrid 
 |-  ( 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 imbitrrdi 
 |-  ( 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 imbitrrdi 
 |-  ( 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 \ { (/) } ) )