Theorem petlem

Description: If you can prove that the equivalence of cosets on their natural domain implies disjointness (e.g. eqvrelqseqdisj5 ), or converse function (cf. dfdisjALTV ), then disjointness, and equivalence of cosets, both on their natural domain, are equivalent. Lemma for the Partition Equivalence Theorem pet2 . (Contributed by Peter Mazsa, 18-Sep-2021)

	Ref	Expression
Hypothesis	petlem.1	|- ( ( EqvRel ,~ R /\ ( dom ,~ R /. ,~ R ) = A ) -> Disj R )
Assertion	petlem	|- ( ( Disj R /\ ( dom R /. R ) = A ) <-> ( EqvRel ,~ R /\ ( dom ,~ R /. ,~ R ) = A ) )

Proof

Step	Hyp	Ref	Expression
1		petlem.1	|- ( ( EqvRel ,~ R /\ ( dom ,~ R /. ,~ R ) = A ) -> Disj R )
2		partim2	|- ( ( Disj R /\ ( dom R /. R ) = A ) -> ( EqvRel ,~ R /\ ( dom ,~ R /. ,~ R ) = A ) )
3		simpr	|- ( ( EqvRel ,~ R /\ ( dom ,~ R /. ,~ R ) = A ) -> ( dom ,~ R /. ,~ R ) = A )
4		disjdmqseq	|- ( Disj R -> ( ( dom R /. R ) = A <-> ( dom ,~ R /. ,~ R ) = A ) )
5	4	pm5.32i	|- ( ( Disj R /\ ( dom R /. R ) = A ) <-> ( Disj R /\ ( dom ,~ R /. ,~ R ) = A ) )
6	1 3 5	sylanbrc	|- ( ( EqvRel ,~ R /\ ( dom ,~ R /. ,~ R ) = A ) -> ( Disj R /\ ( dom R /. R ) = A ) )
7	2 6	impbii	|- ( ( Disj R /\ ( dom R /. R ) = A ) <-> ( EqvRel ,~ R /\ ( dom ,~ R /. ,~ R ) = A ) )