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 ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) }
Assertion prter1 ( Prt 𝐴 → ∼ Er ∪ 𝐴 )

Proof

Step Hyp Ref Expression
1 prtlem18.1 ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) }
2 1 relopabiv ⊢ Rel ∼
3 2 a1i ⊢ ( Prt 𝐴 → Rel ∼ )
4 1 prtlem16 ⊢ dom ∼ = ∪ 𝐴
5 4 a1i ⊢ ( Prt 𝐴 → dom ∼ = ∪ 𝐴 )
6 prtlem15 ⊢ ( Prt 𝐴 → ( ∃ 𝑣 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑤 ∈ 𝑞 ∧ 𝑝 ∈ 𝑞 ) ) → ∃ 𝑟 ∈ 𝐴 ( 𝑧 ∈ 𝑟 ∧ 𝑝 ∈ 𝑟 ) ) )
7 1 prtlem13 ⊢ ( 𝑧 ∼ 𝑤 ↔ ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) )
8 1 prtlem13 ⊢ ( 𝑤 ∼ 𝑝 ↔ ∃ 𝑞 ∈ 𝐴 ( 𝑤 ∈ 𝑞 ∧ 𝑝 ∈ 𝑞 ) )
9 7 8 anbi12i ⊢ ( ( 𝑧 ∼ 𝑤 ∧ 𝑤 ∼ 𝑝 ) ↔ ( ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ∧ ∃ 𝑞 ∈ 𝐴 ( 𝑤 ∈ 𝑞 ∧ 𝑝 ∈ 𝑞 ) ) )
10 reeanv ⊢ ( ∃ 𝑣 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑤 ∈ 𝑞 ∧ 𝑝 ∈ 𝑞 ) ) ↔ ( ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ∧ ∃ 𝑞 ∈ 𝐴 ( 𝑤 ∈ 𝑞 ∧ 𝑝 ∈ 𝑞 ) ) )
11 9 10 bitr4i ⊢ ( ( 𝑧 ∼ 𝑤 ∧ 𝑤 ∼ 𝑝 ) ↔ ∃ 𝑣 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑤 ∈ 𝑞 ∧ 𝑝 ∈ 𝑞 ) ) )
12 1 prtlem13 ⊢ ( 𝑧 ∼ 𝑝 ↔ ∃ 𝑟 ∈ 𝐴 ( 𝑧 ∈ 𝑟 ∧ 𝑝 ∈ 𝑟 ) )
13 6 11 12 3imtr4g ⊢ ( Prt 𝐴 → ( ( 𝑧 ∼ 𝑤 ∧ 𝑤 ∼ 𝑝 ) → 𝑧 ∼ 𝑝 ) )
14 pm3.22 ⊢ ( ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) → ( 𝑤 ∈ 𝑣 ∧ 𝑧 ∈ 𝑣 ) )
15 14 reximi ⊢ ( ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) → ∃ 𝑣 ∈ 𝐴 ( 𝑤 ∈ 𝑣 ∧ 𝑧 ∈ 𝑣 ) )
16 1 prtlem13 ⊢ ( 𝑤 ∼ 𝑧 ↔ ∃ 𝑣 ∈ 𝐴 ( 𝑤 ∈ 𝑣 ∧ 𝑧 ∈ 𝑣 ) )
17 15 7 16 3imtr4i ⊢ ( 𝑧 ∼ 𝑤 → 𝑤 ∼ 𝑧 )
18 13 17 jctil ⊢ ( Prt 𝐴 → ( ( 𝑧 ∼ 𝑤 → 𝑤 ∼ 𝑧 ) ∧ ( ( 𝑧 ∼ 𝑤 ∧ 𝑤 ∼ 𝑝 ) → 𝑧 ∼ 𝑝 ) ) )
19 18 alrimivv ⊢ ( Prt 𝐴 → ∀ 𝑤 ∀ 𝑝 ( ( 𝑧 ∼ 𝑤 → 𝑤 ∼ 𝑧 ) ∧ ( ( 𝑧 ∼ 𝑤 ∧ 𝑤 ∼ 𝑝 ) → 𝑧 ∼ 𝑝 ) ) )
20 19 alrimiv ⊢ ( Prt 𝐴 → ∀ 𝑧 ∀ 𝑤 ∀ 𝑝 ( ( 𝑧 ∼ 𝑤 → 𝑤 ∼ 𝑧 ) ∧ ( ( 𝑧 ∼ 𝑤 ∧ 𝑤 ∼ 𝑝 ) → 𝑧 ∼ 𝑝 ) ) )
21 dfer2 ⊢ ( ∼ Er ∪ 𝐴 ↔ ( Rel ∼ ∧ dom ∼ = ∪ 𝐴 ∧ ∀ 𝑧 ∀ 𝑤 ∀ 𝑝 ( ( 𝑧 ∼ 𝑤 → 𝑤 ∼ 𝑧 ) ∧ ( ( 𝑧 ∼ 𝑤 ∧ 𝑤 ∼ 𝑝 ) → 𝑧 ∼ 𝑝 ) ) ) )
22 3 5 20 21 syl3anbrc ⊢ ( Prt 𝐴 → ∼ Er ∪ 𝐴 )