This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑅 ∈ 𝑉 → ( 𝑅 ∈ Disjs ↔ Disj 𝑅 ) )

Proof

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