Theorem eltop2 22362

Description: Membership in a topology. (Contributed by NM, 19-Jul-2006.)

Assertion

Ref	Expression
eltop2	⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴)))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐽,𝑦

Proof of Theorem eltop2

Step	Hyp	Ref	Expression
1		tgtop 22360	. . 3 ⊢ (𝐽 ∈ Top → (topGen‘𝐽) = 𝐽)
2	1	eleq2d 2818	. 2 ⊢ (𝐽 ∈ Top → (𝐴 ∈ (topGen‘𝐽) ↔ 𝐴 ∈ 𝐽))
3		eltg2b 22346	. 2 ⊢ (𝐽 ∈ Top → (𝐴 ∈ (topGen‘𝐽) ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴)))
4	2, 3	bitr3d 280	1 ⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∈ wcel 2106  ∀wral 3060  ∃wrex 3069   ⊆ wss 3913  ‘cfv 6501  topGenctg 17333  Topctop 22279

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6453  df-fun 6503  df-fv 6509  df-topgen 17339  df-top 22280

This theorem is referenced by:  isclo  22475  cncnp  22668  ist1-2  22735  hauscmp  22795  llycmpkgen2  22938  ptpjopn  23000  txkgen  23040  xkococn  23048  xkoinjcn  23075  fclscf  23413  subgntr  23495  opnsubg  23496  qustgpopn  23508  prdsxmslem2  23922  zdis  24216  efopn  26050  cvmopnlem  33959  neibastop3  34910  ioorrnopn  44666  ioorrnopnxr  44668