This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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