Theorem fences3

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

	Ref	Expression
Assertion	fences3	⊢ ( ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) → ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		eqvrelqseqdisj2	⊢ ( ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) → ElDisj 𝐴 )
2		n0eldmqseq	⊢ ( ( dom 𝑅 / 𝑅 ) = 𝐴 → ¬ ∅ ∈ 𝐴 )
3	2	adantl	⊢ ( ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) → ¬ ∅ ∈ 𝐴 )
4	1 3	jca	⊢ ( ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) → ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) )