Theorem fences3

Description: Implication of eqvrelqseqdisj2 and n0eldmqseq , see comment of fences . (Contributed by Peter Mazsa, 30-Dec-2024)

	Ref	Expression
Assertion	fences3	$$⊢\left(EqvRelR\wedge \mathrm{dom}R/R=A\right)\to \left(ElDisjA\wedge \neg \varnothing \in A\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqvrelqseqdisj2	$$⊢\left(EqvRelR\wedge \mathrm{dom}R/R=A\right)\to ElDisjA$$
2		n0eldmqseq	$$⊢\mathrm{dom}R/R=A\to \neg \varnothing \in A$$
3	2	adantl	$$⊢\left(EqvRelR\wedge \mathrm{dom}R/R=A\right)\to \neg \varnothing \in A$$
4	1 3	jca	$$⊢\left(EqvRelR\wedge \mathrm{dom}R/R=A\right)\to \left(ElDisjA\wedge \neg \varnothing \in A\right)$$