Metamath Proof Explorer

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 ∈ Disjs → dom ⁡ R / R ∈ ElDisjs

Proof

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