Theorem fnerel

Description: Fineness is a relation. (Contributed by Jeff Hankins, 28-Sep-2009)

	Ref	Expression
Assertion	fnerel	$$⊢\mathrm{Rel}\mathrm{Fne}$$

Proof

Step	Hyp	Ref	Expression
1		df-fne	$$⊢\mathrm{Fne}=\left\{⟨x,y⟩|\left(\bigcup x=\bigcup y\wedge \forall z\in xz\subseteq \bigcup \left(y\cap 𝒫z\right)\right)\right\}$$
2	1	relopabiv	$$⊢\mathrm{Rel}\mathrm{Fne}$$