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 𝑅 ) )