Metamath Proof Explorer

Theorem eldisjs2

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

Ref Expression
Assertion eldisjs2 ⊢ R ∈ Disjs ↔ ≀ R -1 ⊆ I ∧ R ∈ Rels

Proof

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