Theorem dfdisjs2

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

	Ref	Expression
Assertion	dfdisjs2	⊢ Disjs = { 𝑟 ∈ Rels ∣ ≀ ◡ 𝑟 ⊆ I }

Proof

Step	Hyp	Ref	Expression
1		dfdisjs	⊢ Disjs = { 𝑟 ∈ Rels ∣ ≀ ◡ 𝑟 ∈ CnvRefRels }
2		cosselcnvrefrels2	⊢ ( ≀ ◡ 𝑟 ∈ CnvRefRels ↔ ( ≀ ◡ 𝑟 ⊆ I ∧ ≀ ◡ 𝑟 ∈ Rels ) )
3		cosscnvelrels	⊢ ( 𝑟 ∈ Rels → ≀ ◡ 𝑟 ∈ Rels )
4	3	biantrud	⊢ ( 𝑟 ∈ Rels → ( ≀ ◡ 𝑟 ⊆ I ↔ ( ≀ ◡ 𝑟 ⊆ I ∧ ≀ ◡ 𝑟 ∈ Rels ) ) )
5	2 4	bitr4id	⊢ ( 𝑟 ∈ Rels → ( ≀ ◡ 𝑟 ∈ CnvRefRels ↔ ≀ ◡ 𝑟 ⊆ I ) )
6	1 5	rabimbieq	⊢ Disjs = { 𝑟 ∈ Rels ∣ ≀ ◡ 𝑟 ⊆ I }