Metamath Proof Explorer

Theorem eldisjsdisj

Description: The element of the class of disjoint relations and the disjoint relation predicate are the same, that is ( R e. Disjs <-> Disj R ) when R is a set. (Contributed by Peter Mazsa, 25-Jul-2021)

Ref Expression
Assertion eldisjsdisj ⊢ R ∈ V → R ∈ Disjs ↔ Disj R

Proof

Step Hyp Ref Expression
1 cosscnvex ⊢ R ∈ V → ≀ R -1 ∈ V
2 elcnvrefrelsrel ⊢ ≀ R -1 ∈ V → ≀ R -1 ∈ CnvRefRels ↔ CnvRefRel ≀ R -1
3 1 2 syl ⊢ R ∈ V → ≀ R -1 ∈ CnvRefRels ↔ CnvRefRel ≀ R -1
4 elrelsrel ⊢ R ∈ V → R ∈ Rels ↔ Rel ⁡ R
5 3 4 anbi12d ⊢ R ∈ V → ≀ R -1 ∈ CnvRefRels ∧ R ∈ Rels ↔ CnvRefRel ≀ R -1 ∧ Rel ⁡ R
6 eldisjs ⊢ R ∈ Disjs ↔ ≀ R -1 ∈ CnvRefRels ∧ R ∈ Rels
7 df-disjALTV ⊢ Disj R ↔ CnvRefRel ≀ R -1 ∧ Rel ⁡ R
8 5 6 7 3bitr4g ⊢ R ∈ V → R ∈ Disjs ↔ Disj R