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 ) = (/) ) }