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 | ∃ u ∈ A x ∈ u ∧ y ∈ u
Assertion prter1 ⊢ Prt A → ∼ ˙ Er ⋃ A

Proof

Step Hyp Ref Expression
1 prtlem18.1 ⊢ ∼ ˙ = x y | ∃ u ∈ A x ∈ u ∧ y ∈ u
2 1 relopabiv ⊢ Rel ⁡ ∼ ˙
3 2 a1i ⊢ Prt A → Rel ⁡ ∼ ˙
4 1 prtlem16 ⊢ dom ⁡ ∼ ˙ = ⋃ A
5 4 a1i ⊢ Prt A → dom ⁡ ∼ ˙ = ⋃ A
6 prtlem15 ⊢ Prt A → ∃ v ∈ A ∃ q ∈ A z ∈ v ∧ w ∈ v ∧ w ∈ q ∧ p ∈ q → ∃ r ∈ A z ∈ r ∧ p ∈ r
7 1 prtlem13 ⊢ z ∼ ˙ w ↔ ∃ v ∈ A z ∈ v ∧ w ∈ v
8 1 prtlem13 ⊢ w ∼ ˙ p ↔ ∃ q ∈ A w ∈ q ∧ p ∈ q
9 7 8 anbi12i ⊢ z ∼ ˙ w ∧ w ∼ ˙ p ↔ ∃ v ∈ A z ∈ v ∧ w ∈ v ∧ ∃ q ∈ A w ∈ q ∧ p ∈ q
10 reeanv ⊢ ∃ v ∈ A ∃ q ∈ A z ∈ v ∧ w ∈ v ∧ w ∈ q ∧ p ∈ q ↔ ∃ v ∈ A z ∈ v ∧ w ∈ v ∧ ∃ q ∈ A w ∈ q ∧ p ∈ q
11 9 10 bitr4i ⊢ z ∼ ˙ w ∧ w ∼ ˙ p ↔ ∃ v ∈ A ∃ q ∈ A z ∈ v ∧ w ∈ v ∧ w ∈ q ∧ p ∈ q
12 1 prtlem13 ⊢ z ∼ ˙ p ↔ ∃ r ∈ A z ∈ r ∧ p ∈ r
13 6 11 12 3imtr4g ⊢ Prt A → z ∼ ˙ w ∧ w ∼ ˙ p → z ∼ ˙ p
14 pm3.22 ⊢ z ∈ v ∧ w ∈ v → w ∈ v ∧ z ∈ v
15 14 reximi ⊢ ∃ v ∈ A z ∈ v ∧ w ∈ v → ∃ v ∈ A w ∈ v ∧ z ∈ v
16 1 prtlem13 ⊢ w ∼ ˙ z ↔ ∃ v ∈ A w ∈ v ∧ z ∈ 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 → ∀ w ∀ p z ∼ ˙ w → w ∼ ˙ z ∧ z ∼ ˙ w ∧ w ∼ ˙ p → z ∼ ˙ p
20 19 alrimiv ⊢ Prt A → ∀ z ∀ w ∀ p z ∼ ˙ w → w ∼ ˙ z ∧ z ∼ ˙ w ∧ w ∼ ˙ p → z ∼ ˙ p
21 dfer2 ⊢ ∼ ˙ Er ⋃ A ↔ Rel ⁡ ∼ ˙ ∧ dom ⁡ ∼ ˙ = ⋃ A ∧ ∀ z ∀ w ∀ p z ∼ ˙ w → w ∼ ˙ z ∧ z ∼ ˙ w ∧ w ∼ ˙ p → z ∼ ˙ p
22 3 5 20 21 syl3anbrc ⊢ Prt A → ∼ ˙ Er ⋃ A