Metamath Proof Explorer


Theorem eldisjs2

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

Ref Expression
Assertion eldisjs2 ( 𝑅 ∈ Disjs ↔ ( ≀ 𝑅 ⊆ I ∧ 𝑅 ∈ Rels ) )

Proof

Step Hyp Ref Expression
1 eldisjs ( 𝑅 ∈ Disjs ↔ ( ≀ 𝑅 ∈ CnvRefRels ∧ 𝑅 ∈ Rels ) )
2 cosselcnvrefrels2 ( ≀ 𝑅 ∈ CnvRefRels ↔ ( ≀ 𝑅 ⊆ I ∧ ≀ 𝑅 ∈ Rels ) )
3 cosscnvelrels ( 𝑅 ∈ Rels → ≀ 𝑅 ∈ Rels )
4 3 biantrud ( 𝑅 ∈ Rels → ( ≀ 𝑅 ⊆ I ↔ ( ≀ 𝑅 ⊆ I ∧ ≀ 𝑅 ∈ Rels ) ) )
5 2 4 bitr4id ( 𝑅 ∈ Rels → ( ≀ 𝑅 ∈ CnvRefRels ↔ ≀ 𝑅 ⊆ I ) )
6 5 pm5.32ri ( ( ≀ 𝑅 ∈ CnvRefRels ∧ 𝑅 ∈ Rels ) ↔ ( ≀ 𝑅 ⊆ I ∧ 𝑅 ∈ Rels ) )
7 1 6 bitri ( 𝑅 ∈ Disjs ↔ ( ≀ 𝑅 ⊆ I ∧ 𝑅 ∈ Rels ) )