This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ R Part A → ≀ R ErALTV A

Proof

Step Hyp Ref Expression
1 partim2 ⊢ Disj R ∧ dom ⁡ R / R = A → EqvRel ≀ R ∧ dom ⁡ ≀ R / ≀ R = A
2 dfpart2 ⊢ R Part A ↔ Disj R ∧ dom ⁡ R / R = A
3 dferALTV2 ⊢ ≀ R ErALTV A ↔ EqvRel ≀ R ∧ dom ⁡ ≀ R / ≀ R = A
4 1 2 3 3imtr4i ⊢ R Part A → ≀ R ErALTV A