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	|- ( R e. Disjs -> ( dom R /. R ) e. ElDisjs )

Proof

Step	Hyp	Ref	Expression
1		disjimeldisjdmqs	|- ( Disj R -> ElDisj ( dom R /. R ) )
2		eldisjsdisj	|- ( R e. Disjs -> ( R e. Disjs <-> Disj R ) )
3		dmqsex	|- ( R e. Disjs -> ( dom R /. R ) e. _V )
4		eleldisjseldisj	|- ( ( dom R /. R ) e. _V -> ( ( dom R /. R ) e. ElDisjs <-> ElDisj ( dom R /. R ) ) )
5	3 4	syl	|- ( R e. Disjs -> ( ( dom R /. R ) e. ElDisjs <-> ElDisj ( dom R /. R ) ) )
6	2 5	imbi12d	|- ( R e. Disjs -> ( ( R e. Disjs -> ( dom R /. R ) e. ElDisjs ) <-> ( Disj R -> ElDisj ( dom R /. R ) ) ) )
7	1 6	mpbiri	|- ( R e. Disjs -> ( R e. Disjs -> ( dom R /. R ) e. ElDisjs ) )
8	7	pm2.43i	|- ( R e. Disjs -> ( dom R /. R ) e. ElDisjs )