![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > tg2 | Structured version Visualization version GIF version |
Description: Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.) |
Ref | Expression |
---|---|
tg2 | ⊢ ((𝐴 ∈ (topGen‘𝐵) ∧ 𝐶 ∈ 𝐴) → ∃𝑥 ∈ 𝐵 (𝐶 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfvdm 6442 | . . 3 ⊢ (𝐴 ∈ (topGen‘𝐵) → 𝐵 ∈ dom topGen) | |
2 | eltg2b 21089 | . . . 4 ⊢ (𝐵 ∈ dom topGen → (𝐴 ∈ (topGen‘𝐵) ↔ ∀𝑦 ∈ 𝐴 ∃𝑥 ∈ 𝐵 (𝑦 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴))) | |
3 | eleq1 2865 | . . . . . . 7 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝑥 ↔ 𝐶 ∈ 𝑥)) | |
4 | 3 | anbi1d 624 | . . . . . 6 ⊢ (𝑦 = 𝐶 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴) ↔ (𝐶 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴))) |
5 | 4 | rexbidv 3232 | . . . . 5 ⊢ (𝑦 = 𝐶 → (∃𝑥 ∈ 𝐵 (𝑦 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴) ↔ ∃𝑥 ∈ 𝐵 (𝐶 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴))) |
6 | 5 | rspccv 3493 | . . . 4 ⊢ (∀𝑦 ∈ 𝐴 ∃𝑥 ∈ 𝐵 (𝑦 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴) → (𝐶 ∈ 𝐴 → ∃𝑥 ∈ 𝐵 (𝐶 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴))) |
7 | 2, 6 | syl6bi 245 | . . 3 ⊢ (𝐵 ∈ dom topGen → (𝐴 ∈ (topGen‘𝐵) → (𝐶 ∈ 𝐴 → ∃𝑥 ∈ 𝐵 (𝐶 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴)))) |
8 | 1, 7 | mpcom 38 | . 2 ⊢ (𝐴 ∈ (topGen‘𝐵) → (𝐶 ∈ 𝐴 → ∃𝑥 ∈ 𝐵 (𝐶 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴))) |
9 | 8 | imp 396 | 1 ⊢ ((𝐴 ∈ (topGen‘𝐵) ∧ 𝐶 ∈ 𝐴) → ∃𝑥 ∈ 𝐵 (𝐶 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 = wceq 1653 ∈ wcel 2157 ∀wral 3088 ∃wrex 3089 ⊆ wss 3768 dom cdm 5311 ‘cfv 6100 topGenctg 16410 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2776 ax-sep 4974 ax-nul 4982 ax-pow 5034 ax-pr 5096 ax-un 7182 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2785 df-cleq 2791 df-clel 2794 df-nfc 2929 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3386 df-sbc 3633 df-dif 3771 df-un 3773 df-in 3775 df-ss 3782 df-nul 4115 df-if 4277 df-pw 4350 df-sn 4368 df-pr 4370 df-op 4374 df-uni 4628 df-br 4843 df-opab 4905 df-mpt 4922 df-id 5219 df-xp 5317 df-rel 5318 df-cnv 5319 df-co 5320 df-dm 5321 df-iota 6063 df-fun 6102 df-fv 6108 df-topgen 16416 |
This theorem is referenced by: tgclb 21100 elcls3 21213 pnfnei 21350 mnfnei 21351 tgcnp 21383 tgcmp 21530 2ndcctbss 21584 2ndcdisj 21585 2ndcomap 21587 dis2ndc 21589 ptpjopn 21741 txlm 21777 flftg 22125 alexsublem 22173 alexsubALT 22180 tmdgsum2 22225 xrge0tsms 22962 xrge0tsmsd 30294 iccllysconn 31742 rellysconn 31743 fnessex 32846 ptrecube 33891 islptre 40584 |
Copyright terms: Public domain | W3C validator |