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

Metamath Proof Explorer

Theorem mainer

Description: The Main Theorem of Equivalences: every equivalence relation implies equivalent comembers. (Contributed by Peter Mazsa, 26-Sep-2021)

Ref Expression
Assertion mainer ⊢ R ErALTV A → CoMembEr A

Proof

Step Hyp Ref Expression
1 eqvrelqseqdisj2 ⊢ EqvRel R ∧ dom ⁡ R / R = A → ElDisj A
2 eldisjim ⊢ ElDisj A → CoElEqvRel A
3 1 2 syl ⊢ EqvRel R ∧ dom ⁡ R / R = A → CoElEqvRel A
4 n0eldmqseq ⊢ dom ⁡ R / R = A → ¬ ∅ ∈ A
5 4 adantl ⊢ EqvRel R ∧ dom ⁡ R / R = A → ¬ ∅ ∈ A
6 eldisjn0el ⊢ ElDisj A → ¬ ∅ ∈ A ↔ ⋃ A / ∼ A = A
7 1 6 syl ⊢ EqvRel R ∧ dom ⁡ R / R = A → ¬ ∅ ∈ A ↔ ⋃ A / ∼ A = A
8 5 7 mpbid ⊢ EqvRel R ∧ dom ⁡ R / R = A → ⋃ A / ∼ A = A
9 3 8 jca ⊢ EqvRel R ∧ dom ⁡ R / R = A → CoElEqvRel A ∧ ⋃ A / ∼ A = A
10 dferALTV2 ⊢ R ErALTV A ↔ EqvRel R ∧ dom ⁡ R / R = A
11 dfcomember3 ⊢ CoMembEr A ↔ CoElEqvRel A ∧ ⋃ A / ∼ A = A
12 9 10 11 3imtr4i ⊢ R ErALTV A → CoMembEr A