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 ( 𝑅 ErALTV 𝐴 → CoMembEr 𝐴 )

Proof

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