Metamath Proof Explorer


Theorem dfdisjs5

Description: Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021)

Ref Expression
Assertion dfdisjs5
|- Disjs = { r e. Rels | A. u e. dom r A. v e. dom r ( u = v \/ ( [ u ] r i^i [ v ] r ) = (/) ) }

Proof

Step Hyp Ref Expression
1 dfdisjs2
 |-  Disjs = { r e. Rels | ,~ `' r C_ _I }
2 cosscnvssid5
 |-  ( ( ,~ `' r C_ _I /\ Rel r ) <-> ( A. u e. dom r A. v e. dom r ( u = v \/ ( [ u ] r i^i [ v ] r ) = (/) ) /\ Rel r ) )
3 elrelsrelim
 |-  ( r e. Rels -> Rel r )
4 3 biantrud
 |-  ( r e. Rels -> ( ,~ `' r C_ _I <-> ( ,~ `' r C_ _I /\ Rel r ) ) )
5 3 biantrud
 |-  ( r e. Rels -> ( A. u e. dom r A. v e. dom r ( u = v \/ ( [ u ] r i^i [ v ] r ) = (/) ) <-> ( A. u e. dom r A. v e. dom r ( u = v \/ ( [ u ] r i^i [ v ] r ) = (/) ) /\ Rel r ) ) )
6 4 5 bibi12d
 |-  ( r e. Rels -> ( ( ,~ `' r C_ _I <-> A. u e. dom r A. v e. dom r ( u = v \/ ( [ u ] r i^i [ v ] r ) = (/) ) ) <-> ( ( ,~ `' r C_ _I /\ Rel r ) <-> ( A. u e. dom r A. v e. dom r ( u = v \/ ( [ u ] r i^i [ v ] r ) = (/) ) /\ Rel r ) ) ) )
7 2 6 mpbiri
 |-  ( r e. Rels -> ( ,~ `' r C_ _I <-> A. u e. dom r A. v e. dom r ( u = v \/ ( [ u ] r i^i [ v ] r ) = (/) ) ) )
8 1 7 rabimbieq
 |-  Disjs = { r e. Rels | A. u e. dom r A. v e. dom r ( u = v \/ ( [ u ] r i^i [ v ] r ) = (/) ) }