Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eltopss | Structured version Visualization version GIF version |
Description: A member of a topology is a subset of its underlying set. (Contributed by NM, 12-Sep-2006.) |
Ref | Expression |
---|---|
1open.1 | ⊢ 𝑋 = ∪ 𝐽 |
Ref | Expression |
---|---|
eltopss | ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elssuni 4825 | . . 3 ⊢ (𝐴 ∈ 𝐽 → 𝐴 ⊆ ∪ 𝐽) | |
2 | 1open.1 | . . 3 ⊢ 𝑋 = ∪ 𝐽 | |
3 | 1, 2 | sseqtrrdi 3926 | . 2 ⊢ (𝐴 ∈ 𝐽 → 𝐴 ⊆ 𝑋) |
4 | 3 | adantl 485 | 1 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1542 ∈ wcel 2113 ⊆ wss 3841 ∪ cuni 4793 Topctop 21637 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1545 df-ex 1787 df-sb 2074 df-clab 2717 df-cleq 2730 df-clel 2811 df-v 3399 df-in 3848 df-ss 3858 df-uni 4794 |
This theorem is referenced by: riinopn 21652 opncld 21777 ntrval2 21795 ntrss3 21804 cmclsopn 21806 opncldf1 21828 opnneissb 21858 opnssneib 21859 opnneiss 21862 neitr 21924 restntr 21926 cnpnei 22008 imasnopn 22434 cnextcn 22811 utopreg 22997 ist0cld 31347 opnregcld 34149 ptrecube 35389 poimirlem29 35418 poimir 35422 seposep 45725 iscnrm3rlem7 45746 |
Copyright terms: Public domain | W3C validator |