Theorem dtt2 10498

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 1473	. . 3 |- U.P~A = U.P~A
2	1	ishaus 7733	. 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 7599	. 2 |- P~A e. Top
5		visset 1809	. . . . . . . 8 |- x e. V
6	5	snid 2431	. . . . . . 7 |- x e. {x}
7	6	a1i 8	. . . . . 6 |- (x =/= y -> x e. {x})
8		visset 1809	. . . . . . . 8 |- y e. V
9	8	snid 2431	. . . . . . 7 |- y e. {y}
10	9	a1i 8	. . . . . 6 |- (x =/= y -> y e. {y})
11		disjsn2 2438	. . . . . 6 |- (x =/= y -> ({x} i^i {y}) = (/))
12	7, 10, 11	3jca 818	. . . . 5 |- (x =/= y -> (x e. {x} /\ y e. {y} /\ ({x} i^i {y}) = (/)))
13		eleq2 1532	. . . . . . . . . 10 |- (u = {x} -> (x e. u <-> x e. {x}))
14		ineq1 2206	. . . . . . . . . . 11 |- (u = {x} -> (u i^i v) = ({x} i^i v))
15	14	eqeq1d 1480	. . . . . . . . . 10 |- (u = {x} -> ((u i^i v) = (/) <-> ({x} i^i v) = (/)))
16	13, 15	3anbi13d 893	. . . . . . . . 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 611	. . . . . . . 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 1532	. . . . . . . . . 10 |- (v = {y} -> (y e. v <-> y e. {y}))
19		ineq2 2207	. . . . . . . . . . 11 |- (v = {y} -> ({x} i^i v) = ({x} i^i {y}))
20	19	eqeq1d 1480	. . . . . . . . . 10 |- (v = {y} -> (({x} i^i v) = (/) <-> ({x} i^i {y}) = (/)))
21	18, 20	3anbi23d 894	. . . . . . . . 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 611	. . . . . . . 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 1877	. . . . . . 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 834	. . . . . 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 2751	. . . . . . . . 9 |- U.P~A = A
26	25	eleq2i 1535	. . . . . . . 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 2747	. . . . . . 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 1535	. . . . . . . 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 2747	. . . . . . 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 454	. . . . 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 1758	. . . . 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 1731	. . . 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 1758	. . . 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 1696	. 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 729	1 |- P~A e. Haus

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 774   = wceq 954   e. wcel 956   =/= wne 1582  A.wral 1642  E.wrex 1643  Vcvv 1807   i^i cin 2042  (/)c0 2276  P~cpw 2397  {csn 2405  U.cuni 2498  Topctop 7538  Hauscha 7731

This theorem is referenced by:  dtt1 10499

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-pow 2737  ax-un 2861

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 776  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-ral 1646  df-rex 1647  df-rab 1649  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-uni 2499  df-top 7542  df-haus 7732

Copyright terms: Public domain