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 ( ( 𝐴 Fne 𝐵𝑆𝐴 ) → ∃ 𝑥 ( 𝑥𝐵𝑆 = 𝑥 ) )

Proof

Step Hyp Ref Expression
1 fnetg ( 𝐴 Fne 𝐵𝐴 ⊆ ( topGen ‘ 𝐵 ) )
2 1 sselda ( ( 𝐴 Fne 𝐵𝑆𝐴 ) → 𝑆 ∈ ( topGen ‘ 𝐵 ) )
3 elfvdm ( 𝑆 ∈ ( topGen ‘ 𝐵 ) → 𝐵 ∈ dom topGen )
4 eltg3 ( 𝐵 ∈ dom topGen → ( 𝑆 ∈ ( topGen ‘ 𝐵 ) ↔ ∃ 𝑥 ( 𝑥𝐵𝑆 = 𝑥 ) ) )
5 3 4 syl ( 𝑆 ∈ ( topGen ‘ 𝐵 ) → ( 𝑆 ∈ ( topGen ‘ 𝐵 ) ↔ ∃ 𝑥 ( 𝑥𝐵𝑆 = 𝑥 ) ) )
6 5 ibi ( 𝑆 ∈ ( topGen ‘ 𝐵 ) → ∃ 𝑥 ( 𝑥𝐵𝑆 = 𝑥 ) )
7 2 6 syl ( ( 𝐴 Fne 𝐵𝑆𝐴 ) → ∃ 𝑥 ( 𝑥𝐵𝑆 = 𝑥 ) )