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 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∪ 𝑥 = ∪ 𝑦 ∧ ∀ 𝑧 ∈ 𝑥 𝑧 ⊆ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) }
2	1	relopabiv	⊢ Rel Fne