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 ∪ 𝐴 )