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