Metamath Proof Explorer

Theorem eldisjs5

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

Ref Expression
Assertion eldisjs5 
|- ( R e. V -> ( R e. Disjs <-> ( A. u e. dom R A. v e. dom R ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) /\ R e. Rels ) ) )

Proof

Step Hyp Ref Expression
1 eldisjs2 
 |-  ( R e. Disjs <-> ( ,~ `' R C_ _I /\ R e. Rels ) )
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 elrelsrel 
 |-  ( R e. V -> ( R e. Rels <-> Rel R ) )
4 3 anbi2d 
 |-  ( R e. V -> ( ( ,~ `' R C_ _I /\ R e. Rels ) <-> ( ,~ `' R C_ _I /\ Rel R ) ) )
5 3 anbi2d 
 |-  ( R e. V -> ( ( A. u e. dom R A. v e. dom R ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) /\ R e. Rels ) <-> ( 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. V -> ( ( ( ,~ `' R C_ _I /\ R e. Rels ) <-> ( A. u e. dom R A. v e. dom R ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) /\ R e. Rels ) ) <-> ( ( ,~ `' 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. V -> ( ( ,~ `' R C_ _I /\ R e. Rels ) <-> ( A. u e. dom R A. v e. dom R ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) /\ R e. Rels ) ) )
8 1 7 syl5bb 
 |-  ( R e. V -> ( R e. Disjs <-> ( A. u e. dom R A. v e. dom R ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) /\ R e. Rels ) ) )