Theorem istopg 19171

Description: Express the predicate " J is a topology." Note: In the literature, a topology is often represented by a script letter T, which resembles the letter J. This confusion may have led to J being used by some authors - e.g. K. D. Joshi, Introduction to General Topology (1983), p. 114 - and it is convenient for us since we later use T to represent linear transformations (operators). (Contributed by Stefan Allan, 3-Mar-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)

Assertion

Ref	Expression
istopg	|- ( J e. A -> ( J e. Top <-> ( A. x ( x C_ J -> U. x e. J ) /\ A. x e. J A. y e. J ( x i^i y ) e. J ) ) )

Distinct variable groups:   x, y, J   x, A

Allowed substitution hint:   A( y)

Proof of Theorem istopg

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		pweq 4013	. . . . 5 |- ( z = J -> ~P z = ~P J )
2		eleq2 2540	. . . . 5 |- ( z = J -> ( U. x e. z <-> U. x e. J ) )
3	1, 2	raleqbidv 3072	. . . 4 |- ( z = J -> ( A. x e. ~P z U. x e. z <-> A. x e. ~P J U. x e. J ) )
4		eleq2 2540	. . . . . 6 |- ( z = J -> ( ( x i^i y ) e. z <-> ( x i^i y ) e. J ) )
5	4	raleqbi1dv 3066	. . . . 5 |- ( z = J -> ( A. y e. z ( x i^i y ) e. z <-> A. y e. J ( x i^i y ) e. J ) )
6	5	raleqbi1dv 3066	. . . 4 |- ( z = J -> ( A. x e. z A. y e. z ( x i^i y ) e. z <-> A. x e. J A. y e. J ( x i^i y ) e. J ) )
7	3, 6	anbi12d 710	. . 3 |- ( z = J -> ( ( A. x e. ~P z U. x e. z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) <-> ( A. x e. ~P J U. x e. J /\ A. x e. J A. y e. J ( x i^i y ) e. J ) ) )
8		df-top 19166	. . 3 |- Top = { z | ( A. x e. ~P z U. x e. z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) }
9	7, 8	elab2g 3252	. 2 |- ( J e. A -> ( J e. Top <-> ( A. x e. ~P J U. x e. J /\ A. x e. J A. y e. J ( x i^i y ) e. J ) ) )
10		df-ral 2819	. . . 4 |- ( A. x e. ~P J U. x e. J <-> A. x ( x e. ~P J -> U. x e. J ) )
11		elpw2g 4610	. . . . . 6 |- ( J e. A -> ( x e. ~P J <-> x C_ J ) )
12	11	imbi1d 317	. . . . 5 |- ( J e. A -> ( ( x e. ~P J -> U. x e. J ) <-> ( x C_ J -> U. x e. J ) ) )
13	12	albidv 1689	. . . 4 |- ( J e. A -> ( A. x ( x e. ~P J -> U. x e. J ) <-> A. x ( x C_ J -> U. x e. J ) ) )
14	10, 13	syl5bb 257	. . 3 |- ( J e. A -> ( A. x e. ~P J U. x e. J <-> A. x ( x C_ J -> U. x e. J ) ) )
15	14	anbi1d 704	. 2 |- ( J e. A -> ( ( A. x e. ~P J U. x e. J /\ A. x e. J A. y e. J ( x i^i y ) e. J ) <-> ( A. x ( x C_ J -> U. x e. J ) /\ A. x e. J A. y e. J ( x i^i y ) e. J ) ) )
16	9, 15	bitrd 253	1 |- ( J e. A -> ( J e. Top <-> ( A. x ( x C_ J -> U. x e. J ) /\ A. x e. J A. y e. J ( x i^i y ) e. J ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   A.wal 1377   = wceq 1379   e. wcel 1767   A.wral 2814   i^i cin 3475   C_ wss 3476   ~Pcpw 4010   U.cuni 4245   Topctop 19161

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-v 3115  df-in 3483  df-ss 3490  df-pw 4012  df-top 19166

This theorem is referenced by:  istop2g  19172  uniopn  19173  inopn  19175  istps3OLD  19190  tgcl  19237  distop  19263  indistopon  19268  fctop  19271  cctop  19273  ppttop  19274  epttop  19276  mretopd  19359  toponmre  19360  neiptoptop  19398  kgentopon  19774  qtoptop2  19935  filcon  20119  utoptop  20472  neibastop1  29780