Theorem eqvrelqseqdisj3

Description: Implication of eqvreldisj3 , lemma for the Member Partition Equivalence Theorem mpet3 . (Contributed by Peter Mazsa, 27-Oct-2020) (Revised by Peter Mazsa, 24-Sep-2021)

	Ref	Expression
Assertion	eqvrelqseqdisj3	$$⊢\left(EqvRelR\wedge B/R=A\right)\to Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqvreldisj3	$$⊢EqvRelR\to Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_{\left(B/R\right)}\right)$$
2	1	adantr	$$⊢\left(EqvRelR\wedge B/R=A\right)\to Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_{\left(B/R\right)}\right)$$
3		reseq2	$$⊢B/R=A\to {{\mathrm{E}}^{-1}\upharpoonright }_{\left(B/R\right)}={{\mathrm{E}}^{-1}\upharpoonright }_A$$
4	3	disjeqd	$$⊢B/R=A\to \left(Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_{\left(B/R\right)}\right)\leftrightarrow Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\right)$$
5	4	adantl	$$⊢\left(EqvRelR\wedge B/R=A\right)\to \left(Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_{\left(B/R\right)}\right)\leftrightarrow Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\right)$$
6	2 5	mpbid	$$⊢\left(EqvRelR\wedge B/R=A\right)\to Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$