Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Jeff Hankins
Refinements
fnerel
Next ⟩
isfne
Metamath Proof Explorer
Ascii
Unicode
Theorem
fnerel
Description:
Fineness is a relation.
(Contributed by
Jeff Hankins
, 28-Sep-2009)
Ref
Expression
Assertion
fnerel
⊢
Rel
⁡
Fne
Proof
Step
Hyp
Ref
Expression
1
df-fne
⊢
Fne
=
x
y
|
⋃
x
=
⋃
y
∧
∀
z
∈
x
z
⊆
⋃
y
∩
𝒫
z
2
1
relopabi
⊢
Rel
⁡
Fne