Description: Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006)
Ref | Expression | ||
---|---|---|---|
Assertion | tg1 | ⊢ ( 𝐴 ∈ ( topGen ‘ 𝐵 ) → 𝐴 ⊆ ∪ 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfvdm | ⊢ ( 𝐴 ∈ ( topGen ‘ 𝐵 ) → 𝐵 ∈ dom topGen ) | |
2 | eltg2 | ⊢ ( 𝐵 ∈ dom topGen → ( 𝐴 ∈ ( topGen ‘ 𝐵 ) ↔ ( 𝐴 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) ) ) ) | |
3 | 2 | simprbda | ⊢ ( ( 𝐵 ∈ dom topGen ∧ 𝐴 ∈ ( topGen ‘ 𝐵 ) ) → 𝐴 ⊆ ∪ 𝐵 ) |
4 | 1 3 | mpancom | ⊢ ( 𝐴 ∈ ( topGen ‘ 𝐵 ) → 𝐴 ⊆ ∪ 𝐵 ) |