Theorem istopg 7596

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 2083	. . . . 5 |- (z = J -> (x (_ z <-> x (_ J))
2		eleq2 1535	. . . . 5 |- (z = J -> (U.x e. z <-> U.x e. J))
3	1, 2	imbi12d 626	. . . 4 |- (z = J -> ((x (_ z -> U.x e. z) <-> (x (_ J -> U.x e. J)))
4	3	albidv 1278	. . 3 |- (z = J -> (A.x(x (_ z -> U.x e. z) <-> A.x(x (_ J -> U.x e. J)))
5		eleq2 1535	. . . . 5 |- (z = J -> ((x i^i y) e. z <-> (x i^i y) e. J))
6	5	raleqd 1791	. . . 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 1791	. . 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 628	. 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 7592	. 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 1900	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 954   = wceq 956   e. wcel 958  A.wral 1645   i^i cin 2046   (_ wss 2047  U.cuni 2503  Topctop 7588

This theorem is referenced by:  istop2gOLD 7597  uniopnt 7598  inopnt 7600  istps3 7608  tgclt 7624  subtop 7646  sn0top 7647  indistop 7648  distop 7649  fctopOLD 7650  cctop 7652  opntop 7870  qusp 10555

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-ral 1649  df-v 1812  df-in 2051  df-ss 2053  df-top 7592

Copyright terms: Public domain