Theorem eldisjsim3

Description: Disjs implies element-disjoint quotient carrier. Exports the carrier-disjointness property in the ElDisjs packaging. (Contributed by Peter Mazsa, 11-Feb-2026)

	Ref	Expression
Assertion	eldisjsim3	⊢ ( 𝑅 ∈ Disjs → ( dom 𝑅 / 𝑅 ) ∈ ElDisjs )

Proof

Step	Hyp	Ref	Expression
1		disjimeldisjdmqs	⊢ ( Disj 𝑅 → ElDisj ( dom 𝑅 / 𝑅 ) )
2		eldisjsdisj	⊢ ( 𝑅 ∈ Disjs → ( 𝑅 ∈ Disjs ↔ Disj 𝑅 ) )
3		dmqsex	⊢ ( 𝑅 ∈ Disjs → ( dom 𝑅 / 𝑅 ) ∈ V )
4		eleldisjseldisj	⊢ ( ( dom 𝑅 / 𝑅 ) ∈ V → ( ( dom 𝑅 / 𝑅 ) ∈ ElDisjs ↔ ElDisj ( dom 𝑅 / 𝑅 ) ) )
5	3 4	syl	⊢ ( 𝑅 ∈ Disjs → ( ( dom 𝑅 / 𝑅 ) ∈ ElDisjs ↔ ElDisj ( dom 𝑅 / 𝑅 ) ) )
6	2 5	imbi12d	⊢ ( 𝑅 ∈ Disjs → ( ( 𝑅 ∈ Disjs → ( dom 𝑅 / 𝑅 ) ∈ ElDisjs ) ↔ ( Disj 𝑅 → ElDisj ( dom 𝑅 / 𝑅 ) ) ) )
7	1 6	mpbiri	⊢ ( 𝑅 ∈ Disjs → ( 𝑅 ∈ Disjs → ( dom 𝑅 / 𝑅 ) ∈ ElDisjs ) )
8	7	pm2.43i	⊢ ( 𝑅 ∈ Disjs → ( dom 𝑅 / 𝑅 ) ∈ ElDisjs )