Theorem subtopsin2 14907

Description: The subspace topology induced by a singleton.

Hypothesis

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

Assertion

Ref	Expression
subtopsin2	|- ((J e. Top /\ A e. X) -> (subSp` <.{A}, J>.) = {(/), {A}})

Proof of Theorem subtopsin2

Step	Hyp	Ref	Expression
1		simpl 346	. . . . 5 |- ((J e. Top /\ A e. X) -> J e. Top)
2		visset 2295	. . . . . 6 |- x e. _V
3	2	a1i 8	. . . . 5 |- ((J e. Top /\ A e. X) -> x e. _V)
4		snex 3492	. . . . . 6 |- {A} e. _V
5	4	a1i 8	. . . . 5 |- ((J e. Top /\ A e. X) -> {A} e. _V)
6		issubspt 10247	. . . . 5 |- ((J e. Top /\ x e. _V /\ {A} e. _V) -> (x e. (subSp` <.{A}, J>.) <-> E.y e. J x = (y i^i {A})))
7	1, 3, 5, 6	syl111anc 1100	. . . 4 |- ((J e. Top /\ A e. X) -> (x e. (subSp` <.{A}, J>.) <-> E.y e. J x = (y i^i {A})))
8		snssi 3129	. . . . . . . 8 |- (A e. y -> {A} C_ y)
9		df-ss 2605	. . . . . . . . 9 |- ({A} C_ y <-> ({A} i^i y) = {A})
10		incom 2787	. . . . . . . . . 10 |- (y i^i {A}) = ({A} i^i y)
11		eqtr 1904	. . . . . . . . . . . . 13 |- ((x = (y i^i {A}) /\ (y i^i {A}) = {A}) -> x = {A})
12		olc 290	. . . . . . . . . . . . . 14 |- (x = {A} -> (x = (/) \/ x = {A}))
13	2	elpr 3061	. . . . . . . . . . . . . 14 |- (x e. {(/), {A}} <-> (x = (/) \/ x = {A}))
14	12, 13	sylibr 217	. . . . . . . . . . . . 13 |- (x = {A} -> x e. {(/), {A}})
15	11, 14	syl 12	. . . . . . . . . . . 12 |- ((x = (y i^i {A}) /\ (y i^i {A}) = {A}) -> x e. {(/), {A}})
16	15	ex 402	. . . . . . . . . . 11 |- (x = (y i^i {A}) -> ((y i^i {A}) = {A} -> x e. {(/), {A}}))
17		eqtr 1904	. . . . . . . . . . 11 |- (((y i^i {A}) = ({A} i^i y) /\ ({A} i^i y) = {A}) -> (y i^i {A}) = {A})
18	16, 17	syl5com 63	. . . . . . . . . 10 |- (((y i^i {A}) = ({A} i^i y) /\ ({A} i^i y) = {A}) -> (x = (y i^i {A}) -> x e. {(/), {A}}))
19	10, 18	mpan 759	. . . . . . . . 9 |- (({A} i^i y) = {A} -> (x = (y i^i {A}) -> x e. {(/), {A}}))
20	9, 19	sylbi 216	. . . . . . . 8 |- ({A} C_ y -> (x = (y i^i {A}) -> x e. {(/), {A}}))
21	8, 20	syl 12	. . . . . . 7 |- (A e. y -> (x = (y i^i {A}) -> x e. {(/), {A}}))
22		disjsn 3089	. . . . . . . 8 |- ((y i^i {A}) = (/) <-> -. A e. y)
23		eqtr 1904	. . . . . . . . . 10 |- ((x = (y i^i {A}) /\ (y i^i {A}) = (/)) -> x = (/))
24		orc 291	. . . . . . . . . . 11 |- (x = (/) -> (x = (/) \/ x = {A}))
25	24, 13	sylibr 217	. . . . . . . . . 10 |- (x = (/) -> x e. {(/), {A}})
26	23, 25	syl 12	. . . . . . . . 9 |- ((x = (y i^i {A}) /\ (y i^i {A}) = (/)) -> x e. {(/), {A}})
27	26	expcom 403	. . . . . . . 8 |- ((y i^i {A}) = (/) -> (x = (y i^i {A}) -> x e. {(/), {A}}))
28	22, 27	sylbir 218	. . . . . . 7 |- (-. A e. y -> (x = (y i^i {A}) -> x e. {(/), {A}}))
29	21, 28	pm2.61i 140	. . . . . 6 |- (x = (y i^i {A}) -> x e. {(/), {A}})
30	29	a1i 8	. . . . 5 |- (y e. J -> (x = (y i^i {A}) -> x e. {(/), {A}}))
31	30	r19.23aiv 2211	. . . 4 |- (E.y e. J x = (y i^i {A}) -> x e. {(/), {A}})
32	7, 31	syl6bi 231	. . 3 |- ((J e. Top /\ A e. X) -> (x e. (subSp` <.{A}, J>.) -> x e. {(/), {A}}))
33		eleq1 1957	. . . . . . 7 |- (x = (/) -> (x e. (subSp` <.{A}, J>.) <-> (/) e. (subSp` <.{A}, J>.)))
34		stoig 10251	. . . . . . . . 9 |- ((J e. Top /\ {A} C_ U.J) -> <.{A}, (subSp` <.{A}, J>.)>. e. TopSp)
35		subtopsin2.1	. . . . . . . . . . 11 |- X = U.J
36	35	eleq2i 1961	. . . . . . . . . 10 |- (A e. X <-> A e. U.J)
37		snssi 3129	. . . . . . . . . 10 |- (A e. U.J -> {A} C_ U.J)
38	36, 37	sylbi 216	. . . . . . . . 9 |- (A e. X -> {A} C_ U.J)
39	34, 38	sylan2 500	. . . . . . . 8 |- ((J e. Top /\ A e. X) -> <.{A}, (subSp` <.{A}, J>.)>. e. TopSp)
40		istps 8875	. . . . . . . . 9 |- (<.{A}, (subSp` <.{A}, J>.)>. e. TopSp <-> ((subSp` <.{A}, J>.) e. Top /\ {A} = U.(subSp` <.{A}, J>.)))
41		0opn 8870	. . . . . . . . . 10 |- ((subSp` <.{A}, J>.) e. Top -> (/) e. (subSp` <.{A}, J>.))
42	41	adantr 425	. . . . . . . . 9 |- (((subSp` <.{A}, J>.) e. Top /\ {A} = U.(subSp` <.{A}, J>.)) -> (/) e. (subSp` <.{A}, J>.))
43	40, 42	sylbi 216	. . . . . . . 8 |- (<.{A}, (subSp` <.{A}, J>.)>. e. TopSp -> (/) e. (subSp` <.{A}, J>.))
44	39, 43	syl 12	. . . . . . 7 |- ((J e. Top /\ A e. X) -> (/) e. (subSp` <.{A}, J>.))
45	33, 44	syl5bir 227	. . . . . 6 |- (x = (/) -> ((J e. Top /\ A e. X) -> x e. (subSp` <.{A}, J>.)))
46		eleq1 1957	. . . . . . 7 |- (x = {A} -> (x e. (subSp` <.{A}, J>.) <-> {A} e. (subSp` <.{A}, J>.)))
47		eqid 1884	. . . . . . . . . . 11 |- U.(subSp` <.{A}, J>.) = U.(subSp` <.{A}, J>.)
48	47	topopn 8871	. . . . . . . . . 10 |- ((subSp` <.{A}, J>.) e. Top -> U.(subSp` <.{A}, J>.) e. (subSp` <.{A}, J>.))
49		eleq1 1957	. . . . . . . . . . . 12 |- (U.(subSp` <.{A}, J>.) = {A} -> (U.(subSp` <.{A}, J>.) e. (subSp` <.{A}, J>.) <-> {A} e. (subSp` <.{A}, J>.)))
50	49	biimpd 170	. . . . . . . . . . 11 |- (U.(subSp` <.{A}, J>.) = {A} -> (U.(subSp` <.{A}, J>.) e. (subSp` <.{A}, J>.) -> {A} e. (subSp` <.{A}, J>.)))
51	50	eqcoms 1887	. . . . . . . . . 10 |- ({A} = U.(subSp` <.{A}, J>.) -> (U.(subSp` <.{A}, J>.) e. (subSp` <.{A}, J>.) -> {A} e. (subSp` <.{A}, J>.)))
52	48, 51	mpan9 521	. . . . . . . . 9 |- (((subSp` <.{A}, J>.) e. Top /\ {A} = U.(subSp` <.{A}, J>.)) -> {A} e. (subSp` <.{A}, J>.))
53	40, 52	sylbi 216	. . . . . . . 8 |- (<.{A}, (subSp` <.{A}, J>.)>. e. TopSp -> {A} e. (subSp` <.{A}, J>.))
54	39, 53	syl 12	. . . . . . 7 |- ((J e. Top /\ A e. X) -> {A} e. (subSp` <.{A}, J>.))
55	46, 54	syl5bir 227	. . . . . 6 |- (x = {A} -> ((J e. Top /\ A e. X) -> x e. (subSp` <.{A}, J>.)))
56	45, 55	jaoi 368	. . . . 5 |- ((x = (/) \/ x = {A}) -> ((J e. Top /\ A e. X) -> x e. (subSp` <.{A}, J>.)))
57	13, 56	sylbi 216	. . . 4 |- (x e. {(/), {A}} -> ((J e. Top /\ A e. X) -> x e. (subSp` <.{A}, J>.)))
58	57	com12 14	. . 3 |- ((J e. Top /\ A e. X) -> (x e. {(/), {A}} -> x e. (subSp` <.{A}, J>.)))
59	32, 58	impbid 574	. 2 |- ((J e. Top /\ A e. X) -> (x e. (subSp` <.{A}, J>.) <-> x e. {(/), {A}}))
60	59	eqrdv 1882	1 |- ((J e. Top /\ A e. X) -> (subSp` <.{A}, J>.) = {(/), {A}})

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   = wceq 1298   e. wcel 1300  E.wrex 2106  _Vcvv 2292   i^i cin 2592   C_ wss 2593  (/)c0 2875  {csn 3044  {cpr 3045  <.cop 3046  U.cuni 3177  ` cfv 3998  Topctop 8857  TopSpctps 8858  subSpcsubsp 10242

This theorem is referenced by:  subsincomp 14956  singcon 14968

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-13 1311  ax-14 1312  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  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-reg 5695

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-iun 3257  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-fv 4014  df-opr 4886  df-oprab 4887  df-top 8861  df-topsp 8862  df-subsp 10243

Copyright terms: Public domain