Metamath Proof Explorer

Theorem eldisjs5

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

Ref Expression
Assertion eldisjs5 ⊢ R ∈ V → R ∈ Disjs ↔ ∀ u ∈ dom ⁡ R ∀ v ∈ dom ⁡ R u = v ∨ u R ∩ v R = ∅ ∧ R ∈ Rels

Proof

Step Hyp Ref Expression
1 eldisjs2 ⊢ R ∈ Disjs ↔ ≀ R -1 ⊆ I ∧ R ∈ Rels
2 cosscnvssid5 ⊢ ≀ R -1 ⊆ I ∧ Rel ⁡ R ↔ ∀ u ∈ dom ⁡ R ∀ v ∈ dom ⁡ R u = v ∨ u R ∩ v R = ∅ ∧ Rel ⁡ R
3 elrelsrel ⊢ R ∈ V → R ∈ Rels ↔ Rel ⁡ R
4 3 anbi2d ⊢ R ∈ V → ≀ R -1 ⊆ I ∧ R ∈ Rels ↔ ≀ R -1 ⊆ I ∧ Rel ⁡ R
5 3 anbi2d ⊢ R ∈ V → ∀ u ∈ dom ⁡ R ∀ v ∈ dom ⁡ R u = v ∨ u R ∩ v R = ∅ ∧ R ∈ Rels ↔ ∀ u ∈ dom ⁡ R ∀ v ∈ dom ⁡ R u = v ∨ u R ∩ v R = ∅ ∧ Rel ⁡ R
6 4 5 bibi12d ⊢ R ∈ V → ≀ R -1 ⊆ I ∧ R ∈ Rels ↔ ∀ u ∈ dom ⁡ R ∀ v ∈ dom ⁡ R u = v ∨ u R ∩ v R = ∅ ∧ R ∈ Rels ↔ ≀ R -1 ⊆ I ∧ Rel ⁡ R ↔ ∀ u ∈ dom ⁡ R ∀ v ∈ dom ⁡ R u = v ∨ u R ∩ v R = ∅ ∧ Rel ⁡ R
7 2 6 mpbiri ⊢ R ∈ V → ≀ R -1 ⊆ I ∧ R ∈ Rels ↔ ∀ u ∈ dom ⁡ R ∀ v ∈ dom ⁡ R u = v ∨ u R ∩ v R = ∅ ∧ R ∈ Rels
8 1 7 bitrid ⊢ R ∈ V → R ∈ Disjs ↔ ∀ u ∈ dom ⁡ R ∀ v ∈ dom ⁡ R u = v ∨ u R ∩ v R = ∅ ∧ R ∈ Rels