Metamath Proof Explorer

Theorem dfdisjs5

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

Ref Expression
Assertion dfdisjs5 ⊢ Disjs = r ∈ Rels | ∀ u ∈ dom ⁡ r ∀ v ∈ dom ⁡ r u = v ∨ u r ∩ v r = ∅

Proof

Step Hyp Ref Expression
1 dfdisjs2 ⊢ Disjs = r ∈ Rels | ≀ r -1 ⊆ I
2 cosscnvssid5 ⊢ ≀ r -1 ⊆ I ∧ Rel ⁡ r ↔ ∀ u ∈ dom ⁡ r ∀ v ∈ dom ⁡ r u = v ∨ u r ∩ v r = ∅ ∧ Rel ⁡ r
3 elrelsrelim ⊢ r ∈ Rels → Rel ⁡ r
4 3 biantrud ⊢ r ∈ Rels → ≀ r -1 ⊆ I ↔ ≀ r -1 ⊆ I ∧ Rel ⁡ r
5 3 biantrud ⊢ r ∈ Rels → ∀ u ∈ dom ⁡ r ∀ v ∈ dom ⁡ r u = v ∨ u r ∩ v r = ∅ ↔ ∀ u ∈ dom ⁡ r ∀ v ∈ dom ⁡ r u = v ∨ u r ∩ v r = ∅ ∧ Rel ⁡ r
6 4 5 bibi12d ⊢ r ∈ Rels → ≀ r -1 ⊆ I ↔ ∀ u ∈ dom ⁡ r ∀ v ∈ dom ⁡ r u = v ∨ u r ∩ v r = ∅ ↔ ≀ r -1 ⊆ I ∧ Rel ⁡ r ↔ ∀ u ∈ dom ⁡ r ∀ v ∈ dom ⁡ r u = v ∨ u r ∩ v r = ∅ ∧ Rel ⁡ r
7 2 6 mpbiri ⊢ r ∈ Rels → ≀ r -1 ⊆ I ↔ ∀ u ∈ dom ⁡ r ∀ v ∈ dom ⁡ r u = v ∨ u r ∩ v r = ∅
8 1 7 rabimbieq ⊢ Disjs = r ∈ Rels | ∀ u ∈ dom ⁡ r ∀ v ∈ dom ⁡ r u = v ∨ u r ∩ v r = ∅