Theorem dtt2 10589

Description: A discrete topology is Hausdorff. Morris. Topology without tears. p.72. ex. 13.

Hypothesis

Ref	Expression
dtt2.1	|- A e. V

Assertion

Ref	Expression
dtt2	|- P~A e. Haus

Proof of Theorem dtt2

Step	Hyp	Ref	Expression
1		eqid 1478	. . 3 |- U.P~A = U.P~A
2	1	ishaus 7780	. 2 |- (P~A e. Haus <-> (P~A e. Top /\ A.x e. U.P~AA.y e. U.P~A(x =/= y -> E.u e. P~ AE.v e. P~ A(x e. u /\ y e. v /\ (u i^i v) = (/)))))
3		dtt2.1	. . 3 |- A e. V
4	3	distop 7646	. 2 |- P~A e. Top
5		visset 1816	. . . . . . . 8 |- x e. V
6	5	snid 2439	. . . . . . 7 |- x e. {x}
7	6	a1i 8	. . . . . 6 |- (x =/= y -> x e. {x})
8		visset 1816	. . . . . . . 8 |- y e. V
9	8	snid 2439	. . . . . . 7 |- y e. {y}
10	9	a1i 8	. . . . . 6 |- (x =/= y -> y e. {y})
11		disjsn2 2446	. . . . . 6 |- (x =/= y -> ({x} i^i {y}) = (/))
12	7, 10, 11	3jca 821	. . . . 5 |- (x =/= y -> (x e. {x} /\ y e. {y} /\ ({x} i^i {y}) = (/)))
13		eleq2 1538	. . . . . . . . . 10 |- (u = {x} -> (x e. u <-> x e. {x}))
14		ineq1 2213	. . . . . . . . . . 11 |- (u = {x} -> (u i^i v) = ({x} i^i v))
15	14	eqeq1d 1486	. . . . . . . . . 10 |- (u = {x} -> ((u i^i v) = (/) <-> ({x} i^i v) = (/)))
16	13, 15	3anbi13d 897	. . . . . . . . 9 |- (u = {x} -> ((x e. u /\ y e. v /\ (u i^i v) = (/)) <-> (x e. {x} /\ y e. v /\ ({x} i^i v) = (/))))
17	16	imbi2d 614	. . . . . . . 8 |- (u = {x} -> ((x =/= y -> (x e. u /\ y e. v /\ (u i^i v) = (/))) <-> (x =/= y -> (x e. {x} /\ y e. v /\ ({x} i^i v) = (/)))))
18		eleq2 1538	. . . . . . . . . 10 |- (v = {y} -> (y e. v <-> y e. {y}))
19		ineq2 2214	. . . . . . . . . . 11 |- (v = {y} -> ({x} i^i v) = ({x} i^i {y}))
20	19	eqeq1d 1486	. . . . . . . . . 10 |- (v = {y} -> (({x} i^i v) = (/) <-> ({x} i^i {y}) = (/)))
21	18, 20	3anbi23d 898	. . . . . . . . 9 |- (v = {y} -> ((x e. {x} /\ y e. v /\ ({x} i^i v) = (/)) <-> (x e. {x} /\ y e. {y} /\ ({x} i^i {y}) = (/))))
22	21	imbi2d 614	. . . . . . . 8 |- (v = {y} -> ((x =/= y -> (x e. {x} /\ y e. v /\ ({x} i^i v) = (/))) <-> (x =/= y -> (x e. {x} /\ y e. {y} /\ ({x} i^i {y}) = (/)))))
23	17, 22	rcla42ev 1884	. . . . . . 7 |- (({x} e. P~A /\ {y} e. P~A /\ (x =/= y -> (x e. {x} /\ y e. {y} /\ ({x} i^i {y}) = (/)))) -> E.u e. P~ AE.v e. P~ A(x =/= y -> (x e. u /\ y e. v /\ (u i^i v) = (/))))
24	23	3expia 837	. . . . . 6 |- (({x} e. P~A /\ {y} e. P~A) -> ((x =/= y -> (x e. {x} /\ y e. {y} /\ ({x} i^i {y}) = (/))) -> E.u e. P~ AE.v e. P~ A(x =/= y -> (x e. u /\ y e. v /\ (u i^i v) = (/)))))
25		unipw 2762	. . . . . . . . 9 |- U.P~A = A
26	25	eleq2i 1541	. . . . . . . 8 |- (x e. U.P~A <-> x e. A)
27	26	biimp 151	. . . . . . 7 |- (x e. U.P~A -> x e. A)
28	5	snelpw 2758	. . . . . . 7 |- (x e. A <-> {x} e. P~A)
29	27, 28	sylib 198	. . . . . 6 |- (x e. U.P~A -> {x} e. P~A)
30	25	eleq2i 1541	. . . . . . . 8 |- (y e. U.P~A <-> y e. A)
31	30	biimp 151	. . . . . . 7 |- (y e. U.P~A -> y e. A)
32	8	snelpw 2758	. . . . . . 7 |- (y e. A <-> {y} e. P~A)
33	31, 32	sylib 198	. . . . . 6 |- (y e. U.P~A -> {y} e. P~A)
34	24, 29, 33	syl2an 456	. . . . 5 |- ((x e. U.P~A /\ y e. U.P~A) -> ((x =/= y -> (x e. {x} /\ y e. {y} /\ ({x} i^i {y}) = (/))) -> E.u e. P~ AE.v e. P~ A(x =/= y -> (x e. u /\ y e. v /\ (u i^i v) = (/)))))
35	12, 34	mpi 44	. . . 4 |- ((x e. U.P~A /\ y e. U.P~A) -> E.u e. P~ AE.v e. P~ A(x =/= y -> (x e. u /\ y e. v /\ (u i^i v) = (/))))
36		r19.37av 1764	. . . . 5 |- (E.v e. P~ A(x =/= y -> (x e. u /\ y e. v /\ (u i^i v) = (/))) -> (x =/= y -> E.v e. P~ A(x e. u /\ y e. v /\ (u i^i v) = (/))))
37	36	r19.22si 1737	. . . 4 |- (E.u e. P~ AE.v e. P~ A(x =/= y -> (x e. u /\ y e. v /\ (u i^i v) = (/))) -> E.u e. P~ A(x =/= y -> E.v e. P~ A(x e. u /\ y e. v /\ (u i^i v) = (/))))
38		r19.37av 1764	. . . 4 |- (E.u e. P~ A(x =/= y -> E.v e. P~ A(x e. u /\ y e. v /\ (u i^i v) = (/))) -> (x =/= y -> E.u e. P~ AE.v e. P~ A(x e. u /\ y e. v /\ (u i^i v) = (/))))
39	35, 37, 38	3syl 20	. . 3 |- ((x e. U.P~A /\ y e. U.P~A) -> (x =/= y -> E.u e. P~ AE.v e. P~ A(x e. u /\ y e. v /\ (u i^i v) = (/))))
40	39	rgen2a 1702	. 2 |- A.x e. U.P~AA.y e. U.P~A(x =/= y -> E.u e. P~ AE.v e. P~ A(x e. u /\ y e. v /\ (u i^i v) = (/)))
41	2, 4, 40	mpbir2an 732	1 |- P~A e. Haus

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 777   = wceq 958   e. wcel 960   =/= wne 1588  A.wral 1648  E.wrex 1649  Vcvv 1814   i^i cin 2049  (/)c0 2283  P~cpw 2405  {csn 2413  U.cuni 2507  Topctop 7590  Hauscha 7778

This theorem is referenced by:  dtt1 10590

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-11 969  ax-12 970  ax-13 971  ax-14 972  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  ax-sep 2708  ax-pow 2748  ax-un 2872

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 779  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-ral 1652  df-rex 1653  df-rab 1655  df-v 1815  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-nul 2284  df-pw 2406  df-sn 2416  df-pr 2417  df-uni 2508  df-top 7594  df-haus 7779

Copyright terms: Public domain