Theorem istopg 7598

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 has 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.)

Assertion

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

Distinct variable group:   x,y,J

Proof of Theorem istopg

Step	Hyp	Ref	Expression
1		sseq2 2086	. . . . 5 |- (z = J -> (x (_ z <-> x (_ J))
2		eleq2 1538	. . . . 5 |- (z = J -> (U.x e. z <-> U.x e. J))
3	1, 2	imbi12d 628	. . . 4 |- (z = J -> ((x (_ z -> U.x e. z) <-> (x (_ J -> U.x e. J)))
4	3	albidv 1280	. . 3 |- (z = J -> (A.x(x (_ z -> U.x e. z) <-> A.x(x (_ J -> U.x e. J)))
5		eleq2 1538	. . . . 5 |- (z = J -> ((x i^i y) e. z <-> (x i^i y) e. J))
6	5	raleqd 1794	. . . 4 |- (z = J -> (A.y e. z (x i^i y) e. z <-> A.y e. J (x i^i y) e. J))
7	6	raleqd 1794	. . 3 |- (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))
8	4, 7	anbi12d 630	. 2 |- (z = J -> ((A.x(x (_ z -> U.x e. z) /\ A.x e. z A.y e. z (x i^i y) e. z) <-> (A.x(x (_ J -> U.x e. J) /\ A.x e. J A.y e. J (x i^i y) e. J)))
9		df-top 7594	. 2 |- Top = {z | (A.x(x (_ z -> U.x e. z) /\ A.x e. z A.y e. z (x i^i y) e. z)}
10	8, 9	elab2g 1903	1 |- (J e. A -> (J e. Top <-> (A.x(x (_ J -> U.x e. J) /\ A.x e. J A.y e. J (x i^i y) e. J)))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223  A.wal 956   = wceq 958   e. wcel 960  A.wral 1648   i^i cin 2049   (_ wss 2050  U.cuni 2507  Topctop 7590

This theorem is referenced by:  uniopnt 7599  inopnt 7601  istps3 7609  tgclt 7623  subtop 7643  sn0top 7644  indistop 7645  distop 7646  fctopOLD 7647  cctop 7649  opntop 7867  qusp 10541

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-ral 1652  df-v 1815  df-in 2054  df-ss 2056  df-top 7594

Copyright terms: Public domain