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 𝐵 ∧ 𝑆 ∈ 𝐴 ) → ∃ 𝑥 ( 𝑥 ⊆ 𝐵 ∧ 𝑆 = ∪ 𝑥 ) ) |
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 𝐵 ∧ 𝑆 ∈ 𝐴 ) → ∃ 𝑥 ( 𝑥 ⊆ 𝐵 ∧ 𝑆 = ∪ 𝑥 ) ) |