Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Disjoints vs. converse functions
eldisjs
Next ⟩
eldisjs2
Metamath Proof Explorer
Ascii
Unicode
Theorem
eldisjs
Description:
Elementhood in the class of disjoints.
(Contributed by
Peter Mazsa
, 24-Jul-2021)
Ref
Expression
Assertion
eldisjs
⊢
R
∈
Disjs
↔
≀
R
-1
∈
CnvRefRels
∧
R
∈
Rels
Proof
Step
Hyp
Ref
Expression
1
dfdisjs
⊢
Disjs
=
r
∈
Rels
|
≀
r
-1
∈
CnvRefRels
2
cnveq
⊢
r
=
R
→
r
-1
=
R
-1
3
2
cosseqd
⊢
r
=
R
→
≀
r
-1
=
≀
R
-1
4
3
eleq1d
⊢
r
=
R
→
≀
r
-1
∈
CnvRefRels
↔
≀
R
-1
∈
CnvRefRels
5
1
4
rabeqel
⊢
R
∈
Disjs
↔
≀
R
-1
∈
CnvRefRels
∧
R
∈
Rels