Theorem partim

Description: Partition implies equivalence relation by the cosets of the relation on its natural domain, cf. partim2 . (Contributed by Peter Mazsa, 17-Sep-2021)

	Ref	Expression
Assertion	partim	⊢ ( 𝑅 Part 𝐴 → ≀ 𝑅 ErALTV 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		partim2	⊢ ( ( Disj 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) → ( EqvRel ≀ 𝑅 ∧ ( dom ≀ 𝑅 / ≀ 𝑅 ) = 𝐴 ) )
2		dfpart2	⊢ ( 𝑅 Part 𝐴 ↔ ( Disj 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) )
3		dferALTV2	⊢ ( ≀ 𝑅 ErALTV 𝐴 ↔ ( EqvRel ≀ 𝑅 ∧ ( dom ≀ 𝑅 / ≀ 𝑅 ) = 𝐴 ) )
4	1 2 3	3imtr4i	⊢ ( 𝑅 Part 𝐴 → ≀ 𝑅 ErALTV 𝐴 )