Theorem is1stc3 15469

Description: An equivalent way of saying "is a first-countable topology."

Hypothesis

Ref	Expression
is1stc3.1	|- X = U.J

Assertion

Ref	Expression
is1stc3	|- (J e. Top -> (J e. 1stc <-> A.x e. X E.y e. ~P J(y ~<_ om /\ A.z e. J (x e. z -> E.w e. y (x e. w /\ w C_ z)))))

Distinct variable groups:   x,y,z,J   x,X   x,w,y,z

Proof of Theorem is1stc3

Step	Hyp	Ref	Expression
1		is1stc3.1	. . 3 |- X = U.J
2	1	is1stc2 15468	. 2 |- (J e. Top -> (J e. 1stc <-> A.x e. X E.y e. ~P J(y ~<_ om /\ A.z e. J (x e. z -> x e. U.(y i^i ~Pz)))))
3		elin 2786	. . . . . . . . . . 11 |- (w e. (y i^i ~Pz) <-> (w e. y /\ w e. ~Pz))
4	3	anbi2i 538	. . . . . . . . . 10 |- ((x e. w /\ w e. (y i^i ~Pz)) <-> (x e. w /\ (w e. y /\ w e. ~Pz)))
5		anass 487	. . . . . . . . . 10 |- (((x e. w /\ w e. y) /\ w e. ~Pz) <-> (x e. w /\ (w e. y /\ w e. ~Pz)))
6		ancom 482	. . . . . . . . . . . 12 |- ((x e. w /\ w e. y) <-> (w e. y /\ x e. w))
7		visset 2295	. . . . . . . . . . . . 13 |- w e. _V
8	7	elpw 3037	. . . . . . . . . . . 12 |- (w e. ~Pz <-> w C_ z)
9	6, 8	anbi12i 540	. . . . . . . . . . 11 |- (((x e. w /\ w e. y) /\ w e. ~Pz) <-> ((w e. y /\ x e. w) /\ w C_ z))
10		anass 487	. . . . . . . . . . 11 |- (((w e. y /\ x e. w) /\ w C_ z) <-> (w e. y /\ (x e. w /\ w C_ z)))
11	9, 10	bitri 190	. . . . . . . . . 10 |- (((x e. w /\ w e. y) /\ w e. ~Pz) <-> (w e. y /\ (x e. w /\ w C_ z)))
12	4, 5, 11	3bitr2i 196	. . . . . . . . 9 |- ((x e. w /\ w e. (y i^i ~Pz)) <-> (w e. y /\ (x e. w /\ w C_ z)))
13	12	exbii 1398	. . . . . . . 8 |- (E.w(x e. w /\ w e. (y i^i ~Pz)) <-> E.w(w e. y /\ (x e. w /\ w C_ z)))
14		eluni 3180	. . . . . . . 8 |- (x e. U.(y i^i ~Pz) <-> E.w(x e. w /\ w e. (y i^i ~Pz)))
15		df-rex 2110	. . . . . . . 8 |- (E.w e. y (x e. w /\ w C_ z) <-> E.w(w e. y /\ (x e. w /\ w C_ z)))
16	13, 14, 15	3bitr4i 200	. . . . . . 7 |- (x e. U.(y i^i ~Pz) <-> E.w e. y (x e. w /\ w C_ z))
17	16	imbi2i 202	. . . . . 6 |- ((x e. z -> x e. U.(y i^i ~Pz)) <-> (x e. z -> E.w e. y (x e. w /\ w C_ z)))
18	17	ralbii 2127	. . . . 5 |- (A.z e. J (x e. z -> x e. U.(y i^i ~Pz)) <-> A.z e. J (x e. z -> E.w e. y (x e. w /\ w C_ z)))
19	18	anbi2i 538	. . . 4 |- ((y ~<_ om /\ A.z e. J (x e. z -> x e. U.(y i^i ~Pz))) <-> (y ~<_ om /\ A.z e. J (x e. z -> E.w e. y (x e. w /\ w C_ z))))
20	19	rexbii 2128	. . 3 |- (E.y e. ~P J(y ~<_ om /\ A.z e. J (x e. z -> x e. U.(y i^i ~Pz))) <-> E.y e. ~P J(y ~<_ om /\ A.z e. J (x e. z -> E.w e. y (x e. w /\ w C_ z))))
21	20	ralbii 2127	. 2 |- (A.x e. X E.y e. ~P J(y ~<_ om /\ A.z e. J (x e. z -> x e. U.(y i^i ~Pz))) <-> A.x e. X E.y e. ~P J(y ~<_ om /\ A.z e. J (x e. z -> E.w e. y (x e. w /\ w C_ z))))
22	2, 21	syl6bb 595	1 |- (J e. Top -> (J e. 1stc <-> A.x e. X E.y e. ~P J(y ~<_ om /\ A.z e. J (x e. z -> E.w e. y (x e. w /\ w C_ z)))))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  E.wex 1326  A.wral 2105  E.wrex 2106   i^i cin 2592   C_ wss 2593  ~Pcpw 3032  U.cuni 3177   class class class wbr 3338  omcom 3949   ~<_ cdom 5424  Topctop 8857  1stcc1stc 15455

This theorem is referenced by:  1stcclb 15471  2ndc1stc 15477

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-in 2603  df-ss 2605  df-pw 3035  df-uni 3178  df-1stc 15461

Copyright terms: Public domain