Metamath Proof Explorer

Theorem topbas

Description: A topology is its own basis. (Contributed by NM, 17-Jul-2006)

Ref Expression
Assertion topbas 
|- ( J e. Top -> J e. TopBases )

Proof

Step Hyp Ref Expression
1 inopn 
 |-  ( ( J e. Top /\ x e. J /\ y e. J ) -> ( x i^i y ) e. J )
2 1 3expb 
 |-  ( ( J e. Top /\ ( x e. J /\ y e. J ) ) -> ( x i^i y ) e. J )
3 simpr 
 |-  ( ( ( J e. Top /\ ( x e. J /\ y e. J ) ) /\ z e. ( x i^i y ) ) -> z e. ( x i^i y ) )
4 ssid 
 |-  ( x i^i y ) C_ ( x i^i y )
5 3 4 jctir 
 |-  ( ( ( J e. Top /\ ( x e. J /\ y e. J ) ) /\ z e. ( x i^i y ) ) -> ( z e. ( x i^i y ) /\ ( x i^i y ) C_ ( x i^i y ) ) )
6 eleq2 
 |-  ( w = ( x i^i y ) -> ( z e. w <-> z e. ( x i^i y ) ) )
7 sseq1 
 |-  ( w = ( x i^i y ) -> ( w C_ ( x i^i y ) <-> ( x i^i y ) C_ ( x i^i y ) ) )
8 6 7 anbi12d 
 |-  ( w = ( x i^i y ) -> ( ( z e. w /\ w C_ ( x i^i y ) ) <-> ( z e. ( x i^i y ) /\ ( x i^i y ) C_ ( x i^i y ) ) ) )
9 8 rspcev 
 |-  ( ( ( x i^i y ) e. J /\ ( z e. ( x i^i y ) /\ ( x i^i y ) C_ ( x i^i y ) ) ) -> E. w e. J ( z e. w /\ w C_ ( x i^i y ) ) )
10 2 5 9 syl2an2r 
 |-  ( ( ( J e. Top /\ ( x e. J /\ y e. J ) ) /\ z e. ( x i^i y ) ) -> E. w e. J ( z e. w /\ w C_ ( x i^i y ) ) )
11 10 exp31 
 |-  ( J e. Top -> ( ( x e. J /\ y e. J ) -> ( z e. ( x i^i y ) -> E. w e. J ( z e. w /\ w C_ ( x i^i y ) ) ) ) )
12 11 ralrimdv 
 |-  ( J e. Top -> ( ( x e. J /\ y e. J ) -> A. z e. ( x i^i y ) E. w e. J ( z e. w /\ w C_ ( x i^i y ) ) ) )
13 12 ralrimivv 
 |-  ( J e. Top -> A. x e. J A. y e. J A. z e. ( x i^i y ) E. w e. J ( z e. w /\ w C_ ( x i^i y ) ) )
14 isbasis2g 
 |-  ( J e. Top -> ( J e. TopBases <-> A. x e. J A. y e. J A. z e. ( x i^i y ) E. w e. J ( z e. w /\ w C_ ( x i^i y ) ) ) )
15 13 14 mpbird 
 |-  ( J e. Top -> J e. TopBases )