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 ⊢∼˙=xy|∃u∈Ax∈u∧y∈u
Assertion prter1 ⊢PrtA→∼˙Er⋃A

Proof

Step Hyp Ref Expression
1 prtlem18.1 ⊢∼˙=xy|∃u∈Ax∈u∧y∈u
2 1 relopabiv ⊢Rel⁡∼˙
3 2 a1i ⊢PrtA→Rel⁡∼˙
4 1 prtlem16 ⊢dom⁡∼˙=⋃A
5 4 a1i ⊢PrtA→dom⁡∼˙=⋃A
6 prtlem15 ⊢PrtA→∃v∈A∃q∈Az∈v∧w∈v∧w∈q∧p∈q→∃r∈Az∈r∧p∈r
7 1 prtlem13 ⊢z∼˙w↔∃v∈Az∈v∧w∈v
8 1 prtlem13 ⊢w∼˙p↔∃q∈Aw∈q∧p∈q
9 7 8 anbi12i ⊢z∼˙w∧w∼˙p↔∃v∈Az∈v∧w∈v∧∃q∈Aw∈q∧p∈q
10 reeanv ⊢∃v∈A∃q∈Az∈v∧w∈v∧w∈q∧p∈q↔∃v∈Az∈v∧w∈v∧∃q∈Aw∈q∧p∈q
11 9 10 bitr4i ⊢z∼˙w∧w∼˙p↔∃v∈A∃q∈Az∈v∧w∈v∧w∈q∧p∈q
12 1 prtlem13 ⊢z∼˙p↔∃r∈Az∈r∧p∈r
13 6 11 12 3imtr4g ⊢PrtA→z∼˙w∧w∼˙p→z∼˙p
14 pm3.22 ⊢z∈v∧w∈v→w∈v∧z∈v
15 14 reximi ⊢∃v∈Az∈v∧w∈v→∃v∈Aw∈v∧z∈v
16 1 prtlem13 ⊢w∼˙z↔∃v∈Aw∈v∧z∈v
17 15 7 16 3imtr4i ⊢z∼˙w→w∼˙z
18 13 17 jctil ⊢PrtA→z∼˙w→w∼˙z∧z∼˙w∧w∼˙p→z∼˙p
19 18 alrimivv ⊢PrtA→∀w∀pz∼˙w→w∼˙z∧z∼˙w∧w∼˙p→z∼˙p
20 19 alrimiv ⊢PrtA→∀z∀w∀pz∼˙w→w∼˙z∧z∼˙w∧w∼˙p→z∼˙p
21 dfer2 ⊢∼˙Er⋃A↔Rel⁡∼˙∧dom⁡∼˙=⋃A∧∀z∀w∀pz∼˙w→w∼˙z∧z∼˙w∧w∼˙p→z∼˙p
22 3 5 20 21 syl3anbrc ⊢PrtA→∼˙Er⋃A