This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑅 ∈ 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 )