Metamath Proof Explorer

Theorem fneuni

Description: If B is finer than A , every element of A is a union of elements of B . (Contributed by Jeff Hankins, 11-Oct-2009)

Ref Expression
Assertion fneuni ⊢ A Fne B ∧ S ∈ A → ∃ x x ⊆ B ∧ S = ⋃ x

Proof

Step Hyp Ref Expression
1 fnetg ⊢ A Fne B → A ⊆ topGen ⁡ B
2 1 sselda ⊢ A Fne B ∧ S ∈ A → S ∈ topGen ⁡ B
3 elfvdm ⊢ S ∈ topGen ⁡ B → B ∈ dom ⁡ topGen
4 eltg3 ⊢ B ∈ dom ⁡ topGen → S ∈ topGen ⁡ B ↔ ∃ x x ⊆ B ∧ S = ⋃ x
5 3 4 syl ⊢ S ∈ topGen ⁡ B → S ∈ topGen ⁡ B ↔ ∃ x x ⊆ B ∧ S = ⋃ x
6 5 ibi ⊢ S ∈ topGen ⁡ B → ∃ x x ⊆ B ∧ S = ⋃ x
7 2 6 syl ⊢ A Fne B ∧ S ∈ A → ∃ x x ⊆ B ∧ S = ⋃ x