MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tg2 Unicode version

Theorem tg2 16954
Description: Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.)
Assertion
Ref Expression
tg2  |-  ( ( A  e.  ( topGen `  B )  /\  C  e.  A )  ->  E. x  e.  B  ( C  e.  x  /\  x  C_  A ) )
Distinct variable groups:    x, A    x, B    x, C

Proof of Theorem tg2
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 elfvdm 5698 . . 3  |-  ( A  e.  ( topGen `  B
)  ->  B  e.  dom  topGen )
2 eltg2b 16948 . . . 4  |-  ( B  e.  dom  topGen  ->  ( A  e.  ( topGen `  B )  <->  A. y  e.  A  E. x  e.  B  ( y  e.  x  /\  x  C_  A ) ) )
3 eleq1 2448 . . . . . . 7  |-  ( y  =  C  ->  (
y  e.  x  <->  C  e.  x ) )
43anbi1d 686 . . . . . 6  |-  ( y  =  C  ->  (
( y  e.  x  /\  x  C_  A )  <-> 
( C  e.  x  /\  x  C_  A ) ) )
54rexbidv 2671 . . . . 5  |-  ( y  =  C  ->  ( E. x  e.  B  ( y  e.  x  /\  x  C_  A )  <->  E. x  e.  B  ( C  e.  x  /\  x  C_  A ) ) )
65rspccv 2993 . . . 4  |-  ( A. y  e.  A  E. x  e.  B  (
y  e.  x  /\  x  C_  A )  -> 
( C  e.  A  ->  E. x  e.  B  ( C  e.  x  /\  x  C_  A ) ) )
72, 6syl6bi 220 . . 3  |-  ( B  e.  dom  topGen  ->  ( A  e.  ( topGen `  B )  ->  ( C  e.  A  ->  E. x  e.  B  ( C  e.  x  /\  x  C_  A ) ) ) )
81, 7mpcom 34 . 2  |-  ( A  e.  ( topGen `  B
)  ->  ( C  e.  A  ->  E. x  e.  B  ( C  e.  x  /\  x  C_  A ) ) )
98imp 419 1  |-  ( ( A  e.  ( topGen `  B )  /\  C  e.  A )  ->  E. x  e.  B  ( C  e.  x  /\  x  C_  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1717   A.wral 2650   E.wrex 2651    C_ wss 3264   dom cdm 4819   ` cfv 5395   topGenctg 13593
This theorem is referenced by:  tgclb  16959  elcls3  17071  pnfnei  17207  mnfnei  17208  tgcnp  17240  tgcmp  17387  2ndcctbss  17440  2ndcdisj  17441  2ndcomap  17443  dis2ndc  17445  ptpjopn  17566  txlm  17602  flftg  17950  alexsublem  17997  alexsubALT  18004  tmdgsum2  18048  xrge0tsms  18737  xrge0tsmsd  24053  iccllyscon  24717  rellyscon  24718  fnessex  26047
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-sep 4272  ax-nul 4280  ax-pow 4319  ax-pr 4345  ax-un 4642
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2243  df-mo 2244  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ne 2553  df-ral 2655  df-rex 2656  df-rab 2659  df-v 2902  df-sbc 3106  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-nul 3573  df-if 3684  df-pw 3745  df-sn 3764  df-pr 3765  df-op 3767  df-uni 3959  df-br 4155  df-opab 4209  df-mpt 4210  df-id 4440  df-xp 4825  df-rel 4826  df-cnv 4827  df-co 4828  df-dm 4829  df-iota 5359  df-fun 5397  df-fv 5403  df-topgen 13595
  Copyright terms: Public domain W3C validator