Metamath Proof Explorer


Theorem dfdisjALTV

Description: Alternate definition of the disjoint relation predicate. A disjoint relation is a converse function of the relation, see the comment of df-disjs why we need disjoint relations instead of converse functions anyway. (Contributed by Peter Mazsa, 27-Jul-2021)

Ref Expression
Assertion dfdisjALTV ( Disj 𝑅 ↔ ( FunALTV 𝑅 ∧ Rel 𝑅 ) )

Proof

Step Hyp Ref Expression
1 df-disjALTV ( Disj 𝑅 ↔ ( CnvRefRel ≀ 𝑅 ∧ Rel 𝑅 ) )
2 relcnv Rel 𝑅
3 df-funALTV ( FunALTV 𝑅 ↔ ( CnvRefRel ≀ 𝑅 ∧ Rel 𝑅 ) )
4 2 3 mpbiran2 ( FunALTV 𝑅 ↔ CnvRefRel ≀ 𝑅 )
5 4 anbi1i ( ( FunALTV 𝑅 ∧ Rel 𝑅 ) ↔ ( CnvRefRel ≀ 𝑅 ∧ Rel 𝑅 ) )
6 1 5 bitr4i ( Disj 𝑅 ↔ ( FunALTV 𝑅 ∧ Rel 𝑅 ) )