Theorem usinuniop 10341

Description: If a topology is connected, its underlying set can't be partitioned into two non empty non-overlapping open sets. (Contributed by FL, 17-Nov-2008.)

Hypothesis

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

Assertion

Ref	Expression
usinuniop	|- (J e. Con -> A.x e. J A.y e. J ((x =/= (/) /\ y =/= (/) /\ (x i^i y) = (/)) -> X =/= (x u. y)))

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

Proof of Theorem usinuniop

Step	Hyp	Ref	Expression
1		usinuniop.1	. . . . . . . . . . . . . . . . . . 19 |- X = U.J
2	1	opncld 8950	. . . . . . . . . . . . . . . . . 18 |- ((J e. Top /\ x e. J) -> (X \ x) e. (Clsd` J))
3		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((X \ x) = y -> ((X \ x) e. (Clsd` J) <-> y e. (Clsd` J)))
4		elin 2786	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y e. (J i^i (Clsd` J)) <-> (y e. J /\ y e. (Clsd` J)))
5		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((J i^i (Clsd` J)) = {(/), U.J} -> (y e. (J i^i (Clsd` J)) <-> y e. {(/), U.J}))
6	5	biimpd 170	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((J i^i (Clsd` J)) = {(/), U.J} -> (y e. (J i^i (Clsd` J)) -> y e. {(/), U.J}))
7		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- y e. _V
8	7	elpr 3061	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (y e. {(/), U.J} <-> (y = (/) \/ y = U.J))
9		olc 290	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (y = (/) -> (x = (/) \/ y = (/)))
10	9	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((X \ x) = y -> (y = (/) -> (x = (/) \/ y = (/))))
11	10	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((J e. Top /\ x e. J) -> ((X \ x) = y -> (y = (/) -> (x = (/) \/ y = (/)))))
12	11	com13 37	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (y = (/) -> ((X \ x) = y -> ((J e. Top /\ x e. J) -> (x = (/) \/ y = (/)))))
13	1	eqcomi 1888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- U.J = X
14	13	eqeq2i 1894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (y = U.J <-> y = X)
15		eqeq2 1893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (y = X -> ((X \ x) = y <-> (X \ x) = X))
16	1	eltopss 8872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((J e. Top /\ x e. J) -> x C_ X)
17		dfss2 2610	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (x C_ X <-> A.y(y e. x -> y e. X))
18		df-dif 2597	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (X \ x) = {y | (y e. X /\ -. y e. x)}
19		eqtr 1904	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ((X = (X \ x) /\ (X \ x) = {y | (y e. X /\ -. y e. x)}) -> X = {y | (y e. X /\ -. y e. x)})
20		abeq2 1999	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (X = {y | (y e. X /\ -. y e. x)} <-> A.y(y e. X <-> (y e. X /\ -. y e. x)))
21		pm4.71 697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((y e. X -> -. y e. x) <-> (y e. X <-> (y e. X /\ -. y e. x)))
22	21	albii 1346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (A.y(y e. X -> -. y e. x) <-> A.y(y e. X <-> (y e. X /\ -. y e. x)))
23		19.26 1416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- (A.y((y e. X -> -. y e. x) /\ (y e. x -> y e. X)) <-> (A.y(y e. X -> -. y e. x) /\ A.y(y e. x -> y e. X)))
24		imim1 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ((y e. x -> y e. X) -> ((y e. X -> -. y e. x) -> (y e. x -> -. y e. x)))
25		pm2.01 104	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ((y e. x -> -. y e. x) -> -. y e. x)
26	24, 25	syl6 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ((y e. x -> y e. X) -> ((y e. X -> -. y e. x) -> -. y e. x))
27	26	impcom 378	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- (((y e. X -> -. y e. x) /\ (y e. x -> y e. X)) -> -. y e. x)
28	27	alimi 1338	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- (A.y((y e. X -> -. y e. x) /\ (y e. x -> y e. X)) -> A.y -. y e. x)
29		eq0 2889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- (x = (/) <-> A.y -. y e. x)
30	28, 29	sylibr 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- (A.y((y e. X -> -. y e. x) /\ (y e. x -> y e. X)) -> x = (/))
31	23, 30	sylbir 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((A.y(y e. X -> -. y e. x) /\ A.y(y e. x -> y e. X)) -> x = (/))
32	31	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (A.y(y e. X -> -. y e. x) -> (A.y(y e. x -> y e. X) -> x = (/)))
33	22, 32	sylbir 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (A.y(y e. X <-> (y e. X /\ -. y e. x)) -> (A.y(y e. x -> y e. X) -> x = (/)))
34	20, 33	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (X = {y | (y e. X /\ -. y e. x)} -> (A.y(y e. x -> y e. X) -> x = (/)))
35	19, 34	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((X = (X \ x) /\ (X \ x) = {y | (y e. X /\ -. y e. x)}) -> (A.y(y e. x -> y e. X) -> x = (/)))
36	35	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (X = (X \ x) -> ((X \ x) = {y | (y e. X /\ -. y e. x)} -> (A.y(y e. x -> y e. X) -> x = (/))))
37	36	eqcoms 1887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((X \ x) = X -> ((X \ x) = {y | (y e. X /\ -. y e. x)} -> (A.y(y e. x -> y e. X) -> x = (/))))
38	18, 37	mpi 55	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((X \ x) = X -> (A.y(y e. x -> y e. X) -> x = (/)))
39	38	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (A.y(y e. x -> y e. X) -> ((X \ x) = X -> x = (/)))
40	17, 39	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (x C_ X -> ((X \ x) = X -> x = (/)))
41	40	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((x C_ X /\ (X \ x) = X) -> x = (/))
42	41	orcd 294	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((x C_ X /\ (X \ x) = X) -> (x = (/) \/ y = (/)))
43	42	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (x C_ X -> ((X \ x) = X -> (x = (/) \/ y = (/))))
44	16, 43	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((J e. Top /\ x e. J) -> ((X \ x) = X -> (x = (/) \/ y = (/))))
45	44	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((X \ x) = X -> ((J e. Top /\ x e. J) -> (x = (/) \/ y = (/))))
46	15, 45	syl6bi 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (y = X -> ((X \ x) = y -> ((J e. Top /\ x e. J) -> (x = (/) \/ y = (/)))))
47	14, 46	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (y = U.J -> ((X \ x) = y -> ((J e. Top /\ x e. J) -> (x = (/) \/ y = (/)))))
48	12, 47	jaoi 368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((y = (/) \/ y = U.J) -> ((X \ x) = y -> ((J e. Top /\ x e. J) -> (x = (/) \/ y = (/)))))
49	8, 48	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (y e. {(/), U.J} -> ((X \ x) = y -> ((J e. Top /\ x e. J) -> (x = (/) \/ y = (/)))))
50	6, 49	syl6com 64	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (y e. (J i^i (Clsd` J)) -> ((J i^i (Clsd` J)) = {(/), U.J} -> ((X \ x) = y -> ((J e. Top /\ x e. J) -> (x = (/) \/ y = (/))))))
51	50	com24 41	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y e. (J i^i (Clsd` J)) -> ((J e. Top /\ x e. J) -> ((X \ x) = y -> ((J i^i (Clsd` J)) = {(/), U.J} -> (x = (/) \/ y = (/))))))
52	4, 51	sylbir 218	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((y e. J /\ y e. (Clsd` J)) -> ((J e. Top /\ x e. J) -> ((X \ x) = y -> ((J i^i (Clsd` J)) = {(/), U.J} -> (x = (/) \/ y = (/))))))
53	52	expcom 403	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y e. (Clsd` J) -> (y e. J -> ((J e. Top /\ x e. J) -> ((X \ x) = y -> ((J i^i (Clsd` J)) = {(/), U.J} -> (x = (/) \/ y = (/)))))))
54	53	com24 41	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y e. (Clsd` J) -> ((X \ x) = y -> ((J e. Top /\ x e. J) -> (y e. J -> ((J i^i (Clsd` J)) = {(/), U.J} -> (x = (/) \/ y = (/)))))))
55	3, 54	syl6bi 231	. . . . . . . . . . . . . . . . . . . . . 22 |- ((X \ x) = y -> ((X \ x) e. (Clsd` J) -> ((X \ x) = y -> ((J e. Top /\ x e. J) -> (y e. J -> ((J i^i (Clsd` J)) = {(/), U.J} -> (x = (/) \/ y = (/))))))))
56	55	pm2.43a 80	. . . . . . . . . . . . . . . . . . . . 21 |- ((X \ x) = y -> ((X \ x) e. (Clsd` J) -> ((J e. Top /\ x e. J) -> (y e. J -> ((J i^i (Clsd` J)) = {(/), U.J} -> (x = (/) \/ y = (/)))))))
57	56	com3l 38	. . . . . . . . . . . . . . . . . . . 20 |- ((X \ x) e. (Clsd` J) -> ((J e. Top /\ x e. J) -> ((X \ x) = y -> (y e. J -> ((J i^i (Clsd` J)) = {(/), U.J} -> (x = (/) \/ y = (/)))))))
58	57	imp 377	. . . . . . . . . . . . . . . . . . 19 |- (((X \ x) e. (Clsd` J) /\ (J e. Top /\ x e. J)) -> ((X \ x) = y -> (y e. J -> ((J i^i (Clsd` J)) = {(/), U.J} -> (x = (/) \/ y = (/))))))
59	58	com24 41	. . . . . . . . . . . . . . . . . 18 |- (((X \ x) e. (Clsd` J) /\ (J e. Top /\ x e. J)) -> ((J i^i (Clsd` J)) = {(/), U.J} -> (y e. J -> ((X \ x) = y -> (x = (/) \/ y = (/))))))
60	2, 59	mpancom 769	. . . . . . . . . . . . . . . . 17 |- ((J e. Top /\ x e. J) -> ((J i^i (Clsd` J)) = {(/), U.J} -> (y e. J -> ((X \ x) = y -> (x = (/) \/ y = (/))))))
61	60	ex 402	. . . . . . . . . . . . . . . 16 |- (J e. Top -> (x e. J -> ((J i^i (Clsd` J)) = {(/), U.J} -> (y e. J -> ((X \ x) = y -> (x = (/) \/ y = (/)))))))
62	61	com14 42	. . . . . . . . . . . . . . 15 |- (y e. J -> (x e. J -> ((J i^i (Clsd` J)) = {(/), U.J} -> (J e. Top -> ((X \ x) = y -> (x = (/) \/ y = (/)))))))
63	62	impcom 378	. . . . . . . . . . . . . 14 |- ((x e. J /\ y e. J) -> ((J i^i (Clsd` J)) = {(/), U.J} -> (J e. Top -> ((X \ x) = y -> (x = (/) \/ y = (/))))))
64	63	com13 37	. . . . . . . . . . . . 13 |- (J e. Top -> ((J i^i (Clsd` J)) = {(/), U.J} -> ((x e. J /\ y e. J) -> ((X \ x) = y -> (x = (/) \/ y = (/))))))
65	64	imp41 395	. . . . . . . . . . . 12 |- ((((J e. Top /\ (J i^i (Clsd` J)) = {(/), U.J}) /\ (x e. J /\ y e. J)) /\ (X \ x) = y) -> (x = (/) \/ y = (/)))
66		nne 2021	. . . . . . . . . . . . 13 |- (-. x =/= (/) <-> x = (/))
67		nne 2021	. . . . . . . . . . . . 13 |- (-. y =/= (/) <-> y = (/))
68	66, 67	orbi12i 277	. . . . . . . . . . . 12 |- ((-. x =/= (/) \/ -. y =/= (/)) <-> (x = (/) \/ y = (/)))
69	65, 68	sylibr 217	. . . . . . . . . . 11 |- ((((J e. Top /\ (J i^i (Clsd` J)) = {(/), U.J}) /\ (x e. J /\ y e. J)) /\ (X \ x) = y) -> (-. x =/= (/) \/ -. y =/= (/)))
70		ianor 329	. . . . . . . . . . 11 |- (-. (x =/= (/) /\ y =/= (/)) <-> (-. x =/= (/) \/ -. y =/= (/)))
71	69, 70	sylibr 217	. . . . . . . . . 10 |- ((((J e. Top /\ (J i^i (Clsd` J)) = {(/), U.J}) /\ (x e. J /\ y e. J)) /\ (X \ x) = y) -> -. (x =/= (/) /\ y =/= (/)))
72	71	ex 402	. . . . . . . . 9 |- (((J e. Top /\ (J i^i (Clsd` J)) = {(/), U.J}) /\ (x e. J /\ y e. J)) -> ((X \ x) = y -> -. (x =/= (/) /\ y =/= (/))))
73	72	con2d 107	. . . . . . . 8 |- (((J e. Top /\ (J i^i (Clsd` J)) = {(/), U.J}) /\ (x e. J /\ y e. J)) -> ((x =/= (/) /\ y =/= (/)) -> -. (X \ x) = y))
74		iscon2 10340	. . . . . . . 8 |- (J e. Con <-> (J e. Top /\ (J i^i (Clsd` J)) = {(/), U.J}))
75	73, 74	sylanb 498	. . . . . . 7 |- ((J e. Con /\ (x e. J /\ y e. J)) -> ((x =/= (/) /\ y =/= (/)) -> -. (X \ x) = y))
76	75	com12 14	. . . . . 6 |- ((x =/= (/) /\ y =/= (/)) -> ((J e. Con /\ (x e. J /\ y e. J)) -> -. (X \ x) = y))
77	76	3adant3 896	. . . . 5 |- ((x =/= (/) /\ y =/= (/) /\ (x i^i y) = (/)) -> ((J e. Con /\ (x e. J /\ y e. J)) -> -. (X \ x) = y))
78	77	impcom 378	. . . 4 |- (((J e. Con /\ (x e. J /\ y e. J)) /\ (x =/= (/) /\ y =/= (/) /\ (x i^i y) = (/))) -> -. (X \ x) = y)
79		twpar2 10149	. . . . . . . . . . . 12 |- ((x C_ X /\ (x i^i y) = (/)) -> ((x u. y) = X <-> (X \ x) = y))
80	13	sseq2i 2642	. . . . . . . . . . . 12 |- (x C_ U.J <-> x C_ X)
81	79, 80	sylanb 498	. . . . . . . . . . 11 |- ((x C_ U.J /\ (x i^i y) = (/)) -> ((x u. y) = X <-> (X \ x) = y))
82		eqcom 1886	. . . . . . . . . . 11 |- (X = (x u. y) <-> (x u. y) = X)
83	81, 82	syl5bb 591	. . . . . . . . . 10 |- ((x C_ U.J /\ (x i^i y) = (/)) -> (X = (x u. y) <-> (X \ x) = y))
84	83	expcom 403	. . . . . . . . 9 |- ((x i^i y) = (/) -> (x C_ U.J -> (X = (x u. y) <-> (X \ x) = y)))
85	84	3ad2ant3 899	. . . . . . . 8 |- ((x =/= (/) /\ y =/= (/) /\ (x i^i y) = (/)) -> (x C_ U.J -> (X = (x u. y) <-> (X \ x) = y)))
86		elssuni 3206	. . . . . . . 8 |- (x e. J -> x C_ U.J)
87	85, 86	syl5com 63	. . . . . . 7 |- (x e. J -> ((x =/= (/) /\ y =/= (/) /\ (x i^i y) = (/)) -> (X = (x u. y) <-> (X \ x) = y)))
88	87	ad2antrl 442	. . . . . 6 |- ((J e. Con /\ (x e. J /\ y e. J)) -> ((x =/= (/) /\ y =/= (/) /\ (x i^i y) = (/)) -> (X = (x u. y) <-> (X \ x) = y)))
89	88	imp 377	. . . . 5 |- (((J e. Con /\ (x e. J /\ y e. J)) /\ (x =/= (/) /\ y =/= (/) /\ (x i^i y) = (/))) -> (X = (x u. y) <-> (X \ x) = y))
90	89	necon3abid 2033	. . . 4 |- (((J e. Con /\ (x e. J /\ y e. J)) /\ (x =/= (/) /\ y =/= (/) /\ (x i^i y) = (/))) -> (X =/= (x u. y) <-> -. (X \ x) = y))
91	78, 90	mpbird 213	. . 3 |- (((J e. Con /\ (x e. J /\ y e. J)) /\ (x =/= (/) /\ y =/= (/) /\ (x i^i y) = (/))) -> X =/= (x u. y))
92	91	exp31 407	. 2 |- (J e. Con -> ((x e. J /\ y e. J) -> ((x =/= (/) /\ y =/= (/) /\ (x i^i y) = (/)) -> X =/= (x u. y))))
93	92	r19.21aivv 2183	1 |- (J e. Con -> A.x e. J A.y e. J ((x =/= (/) /\ y =/= (/) /\ (x i^i y) = (/)) -> X =/= (x u. y)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   /\ w3a 858  A.wal 1296   = wceq 1298   e. wcel 1300  {cab 1871   =/= wne 2017  A.wral 2105   \ cdif 2590   u. cun 2591   i^i cin 2592   C_ wss 2593  (/)c0 2875  {cpr 3045  U.cuni 3177  ` cfv 3998  Topctop 8857  Clsdccld 8936  Conccon 10337

This theorem is referenced by:  dfcon2 15442

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-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

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-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  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-fv 4014  df-cld 8939  df-con 10338

Copyright terms: Public domain