Theorem connsub 15443

Description: Two equivalent ways of saying that a subspace topology is connected.

Hypothesis

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

Assertion

Ref	Expression
connsub	|- ((J e. Top /\ S C_ X) -> ((subSp` <.S, J>.) e. Con <-> A.x e. J A.y e. J (((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S)) -> -. S C_ (x u. y))))

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

Proof of Theorem connsub

Step	Hyp	Ref	Expression
1		stoig3 10253	. . . 4 |- ((J e. Top /\ S C_ U.J) -> (subSp` <.S, J>.) e. Top)
2		connsub.1	. . . . 5 |- X = U.J
3	2	sseq2i 2642	. . . 4 |- (S C_ X <-> S C_ U.J)
4	1, 3	sylan2b 501	. . 3 |- ((J e. Top /\ S C_ X) -> (subSp` <.S, J>.) e. Top)
5		eqid 1884	. . . 4 |- U.(subSp` <.S, J>.) = U.(subSp` <.S, J>.)
6	5	dfcon2 15442	. . 3 |- ((subSp` <.S, J>.) e. Top -> ((subSp` <.S, J>.) e. Con <-> A.u e. (subSp` <.S, J>.)A.v e. (subSp` <.S, J>.)((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> U.(subSp` <.S, J>.) =/= (u u. v))))
7	4, 6	syl 12	. 2 |- ((J e. Top /\ S C_ X) -> ((subSp` <.S, J>.) e. Con <-> A.u e. (subSp` <.S, J>.)A.v e. (subSp` <.S, J>.)((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> U.(subSp` <.S, J>.) =/= (u u. v))))
8		stoig2 10252	. . . 4 |- ((J e. Top /\ S C_ U.J) -> U.(subSp` <.S, J>.) = S)
9	8, 3	sylan2b 501	. . 3 |- ((J e. Top /\ S C_ X) -> U.(subSp` <.S, J>.) = S)
10		neeq1 2024	. . . . 5 |- (U.(subSp` <.S, J>.) = S -> (U.(subSp` <.S, J>.) =/= (u u. v) <-> S =/= (u u. v)))
11	10	imbi2d 674	. . . 4 |- (U.(subSp` <.S, J>.) = S -> (((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> U.(subSp` <.S, J>.) =/= (u u. v)) <-> ((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> S =/= (u u. v))))
12	11	2ralbidv 2140	. . 3 |- (U.(subSp` <.S, J>.) = S -> (A.u e. (subSp` <.S, J>.)A.v e. (subSp` <.S, J>.)((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> U.(subSp` <.S, J>.) =/= (u u. v)) <-> A.u e. (subSp` <.S, J>.)A.v e. (subSp` <.S, J>.)((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> S =/= (u u. v))))
13	9, 12	syl 12	. 2 |- ((J e. Top /\ S C_ X) -> (A.u e. (subSp` <.S, J>.)A.v e. (subSp` <.S, J>.)((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> U.(subSp` <.S, J>.) =/= (u u. v)) <-> A.u e. (subSp` <.S, J>.)A.v e. (subSp` <.S, J>.)((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> S =/= (u u. v))))
14		simp1l 900	. . . . . . . . . 10 |- (((J e. Top /\ S C_ X) /\ (x e. J /\ y e. J) /\ ((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S))) -> J e. Top)
15		simp1r 901	. . . . . . . . . 10 |- (((J e. Top /\ S C_ X) /\ (x e. J /\ y e. J) /\ ((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S))) -> S C_ X)
16		simp2l 902	. . . . . . . . . 10 |- (((J e. Top /\ S C_ X) /\ (x e. J /\ y e. J) /\ ((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S))) -> x e. J)
17		eqidd 1885	. . . . . . . . . 10 |- (((J e. Top /\ S C_ X) /\ (x e. J /\ y e. J) /\ ((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S))) -> (x i^i S) = (x i^i S))
18	2	elsubsp 10248	. . . . . . . . . 10 |- (((J e. Top /\ S C_ X) /\ (x e. J /\ (x i^i S) = (x i^i S))) -> (x i^i S) e. (subSp` <.S, J>.))
19	14, 15, 16, 17, 18	syl22anc 1101	. . . . . . . . 9 |- (((J e. Top /\ S C_ X) /\ (x e. J /\ y e. J) /\ ((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S))) -> (x i^i S) e. (subSp` <.S, J>.))
20		simp2r 903	. . . . . . . . . 10 |- (((J e. Top /\ S C_ X) /\ (x e. J /\ y e. J) /\ ((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S))) -> y e. J)
21		eqidd 1885	. . . . . . . . . 10 |- (((J e. Top /\ S C_ X) /\ (x e. J /\ y e. J) /\ ((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S))) -> (y i^i S) = (y i^i S))
22	2	elsubsp 10248	. . . . . . . . . 10 |- (((J e. Top /\ S C_ X) /\ (y e. J /\ (y i^i S) = (y i^i S))) -> (y i^i S) e. (subSp` <.S, J>.))
23	14, 15, 20, 21, 22	syl22anc 1101	. . . . . . . . 9 |- (((J e. Top /\ S C_ X) /\ (x e. J /\ y e. J) /\ ((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S))) -> (y i^i S) e. (subSp` <.S, J>.))
24		neeq1 2024	. . . . . . . . . . . 12 |- (u = (x i^i S) -> (u =/= (/) <-> (x i^i S) =/= (/)))
25		ineq1 2789	. . . . . . . . . . . . 13 |- (u = (x i^i S) -> (u i^i v) = ((x i^i S) i^i v))
26	25	eqeq1d 1892	. . . . . . . . . . . 12 |- (u = (x i^i S) -> ((u i^i v) = (/) <-> ((x i^i S) i^i v) = (/)))
27	24, 26	3anbi13d 1170	. . . . . . . . . . 11 |- (u = (x i^i S) -> ((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) <-> ((x i^i S) =/= (/) /\ v =/= (/) /\ ((x i^i S) i^i v) = (/))))
28		uneq1 2748	. . . . . . . . . . . 12 |- (u = (x i^i S) -> (u u. v) = ((x i^i S) u. v))
29	28	neeq2d 2029	. . . . . . . . . . 11 |- (u = (x i^i S) -> (S =/= (u u. v) <-> S =/= ((x i^i S) u. v)))
30	27, 29	imbi12d 688	. . . . . . . . . 10 |- (u = (x i^i S) -> (((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> S =/= (u u. v)) <-> (((x i^i S) =/= (/) /\ v =/= (/) /\ ((x i^i S) i^i v) = (/)) -> S =/= ((x i^i S) u. v))))
31		neeq1 2024	. . . . . . . . . . . 12 |- (v = (y i^i S) -> (v =/= (/) <-> (y i^i S) =/= (/)))
32		ineq2 2790	. . . . . . . . . . . . 13 |- (v = (y i^i S) -> ((x i^i S) i^i v) = ((x i^i S) i^i (y i^i S)))
33	32	eqeq1d 1892	. . . . . . . . . . . 12 |- (v = (y i^i S) -> (((x i^i S) i^i v) = (/) <-> ((x i^i S) i^i (y i^i S)) = (/)))
34	31, 33	3anbi23d 1171	. . . . . . . . . . 11 |- (v = (y i^i S) -> (((x i^i S) =/= (/) /\ v =/= (/) /\ ((x i^i S) i^i v) = (/)) <-> ((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ ((x i^i S) i^i (y i^i S)) = (/))))
35		uneq2 2749	. . . . . . . . . . . 12 |- (v = (y i^i S) -> ((x i^i S) u. v) = ((x i^i S) u. (y i^i S)))
36	35	neeq2d 2029	. . . . . . . . . . 11 |- (v = (y i^i S) -> (S =/= ((x i^i S) u. v) <-> S =/= ((x i^i S) u. (y i^i S))))
37	34, 36	imbi12d 688	. . . . . . . . . 10 |- (v = (y i^i S) -> ((((x i^i S) =/= (/) /\ v =/= (/) /\ ((x i^i S) i^i v) = (/)) -> S =/= ((x i^i S) u. v)) <-> (((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ ((x i^i S) i^i (y i^i S)) = (/)) -> S =/= ((x i^i S) u. (y i^i S)))))
38	30, 37	rcla42v 2384	. . . . . . . . 9 |- (((x i^i S) e. (subSp` <.S, J>.) /\ (y i^i S) e. (subSp` <.S, J>.)) -> (A.u e. (subSp` <.S, J>.)A.v e. (subSp` <.S, J>.)((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> S =/= (u u. v)) -> (((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ ((x i^i S) i^i (y i^i S)) = (/)) -> S =/= ((x i^i S) u. (y i^i S)))))
39	19, 23, 38	syl11anc 524	. . . . . . . 8 |- (((J e. Top /\ S C_ X) /\ (x e. J /\ y e. J) /\ ((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S))) -> (A.u e. (subSp` <.S, J>.)A.v e. (subSp` <.S, J>.)((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> S =/= (u u. v)) -> (((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ ((x i^i S) i^i (y i^i S)) = (/)) -> S =/= ((x i^i S) u. (y i^i S)))))
40		difss 2735	. . . . . . . . . . . . . . 15 |- (X \ S) C_ X
41		sstr 2625	. . . . . . . . . . . . . . 15 |- (((x i^i y) C_ (X \ S) /\ (X \ S) C_ X) -> (x i^i y) C_ X)
42	40, 41	mpan2 760	. . . . . . . . . . . . . 14 |- ((x i^i y) C_ (X \ S) -> (x i^i y) C_ X)
43		reldisj 2916	. . . . . . . . . . . . . 14 |- ((x i^i y) C_ X -> (((x i^i y) i^i S) = (/) <-> (x i^i y) C_ (X \ S)))
44	42, 43	syl 12	. . . . . . . . . . . . 13 |- ((x i^i y) C_ (X \ S) -> (((x i^i y) i^i S) = (/) <-> (x i^i y) C_ (X \ S)))
45	44	ibir 653	. . . . . . . . . . . 12 |- ((x i^i y) C_ (X \ S) -> ((x i^i y) i^i S) = (/))
46		inindir 2810	. . . . . . . . . . . 12 |- ((x i^i y) i^i S) = ((x i^i S) i^i (y i^i S))
47	45, 46	syl5eqr 1942	. . . . . . . . . . 11 |- ((x i^i y) C_ (X \ S) -> ((x i^i S) i^i (y i^i S)) = (/))
48	47	3anim3i 1055	. . . . . . . . . 10 |- (((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S)) -> ((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ ((x i^i S) i^i (y i^i S)) = (/)))
49	48	3ad2ant3 899	. . . . . . . . 9 |- (((J e. Top /\ S C_ X) /\ (x e. J /\ y e. J) /\ ((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S))) -> ((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ ((x i^i S) i^i (y i^i S)) = (/)))
50		pm2.27 76	. . . . . . . . . 10 |- (((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ ((x i^i S) i^i (y i^i S)) = (/)) -> ((((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ ((x i^i S) i^i (y i^i S)) = (/)) -> S =/= ((x i^i S) u. (y i^i S))) -> S =/= ((x i^i S) u. (y i^i S))))
51		df-ss 2605	. . . . . . . . . . . . . . 15 |- (S C_ (x u. y) <-> (S i^i (x u. y)) = S)
52	51	biimpi 168	. . . . . . . . . . . . . 14 |- (S C_ (x u. y) -> (S i^i (x u. y)) = S)
53		incom 2787	. . . . . . . . . . . . . 14 |- (S i^i (x u. y)) = ((x u. y) i^i S)
54	52, 53	syl5reqr 1943	. . . . . . . . . . . . 13 |- (S C_ (x u. y) -> S = ((x u. y) i^i S))
55		indir 2842	. . . . . . . . . . . . 13 |- ((x u. y) i^i S) = ((x i^i S) u. (y i^i S))
56	54, 55	syl6eq 1944	. . . . . . . . . . . 12 |- (S C_ (x u. y) -> S = ((x i^i S) u. (y i^i S)))
57	56	necon3ai 2043	. . . . . . . . . . 11 |- (S =/= ((x i^i S) u. (y i^i S)) -> -. S C_ (x u. y))
58	57	a1i 8	. . . . . . . . . 10 |- (((J e. Top /\ S C_ X) /\ (x e. J /\ y e. J) /\ ((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S))) -> (S =/= ((x i^i S) u. (y i^i S)) -> -. S C_ (x u. y)))
59	50, 58	syl9r 72	. . . . . . . . 9 |- (((J e. Top /\ S C_ X) /\ (x e. J /\ y e. J) /\ ((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S))) -> (((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ ((x i^i S) i^i (y i^i S)) = (/)) -> ((((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ ((x i^i S) i^i (y i^i S)) = (/)) -> S =/= ((x i^i S) u. (y i^i S))) -> -. S C_ (x u. y))))
60	49, 59	mpd 29	. . . . . . . 8 |- (((J e. Top /\ S C_ X) /\ (x e. J /\ y e. J) /\ ((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S))) -> ((((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ ((x i^i S) i^i (y i^i S)) = (/)) -> S =/= ((x i^i S) u. (y i^i S))) -> -. S C_ (x u. y)))
61	39, 60	syld 30	. . . . . . 7 |- (((J e. Top /\ S C_ X) /\ (x e. J /\ y e. J) /\ ((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S))) -> (A.u e. (subSp` <.S, J>.)A.v e. (subSp` <.S, J>.)((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> S =/= (u u. v)) -> -. S C_ (x u. y)))
62	61	3exp 1066	. . . . . 6 |- ((J e. Top /\ S C_ X) -> ((x e. J /\ y e. J) -> (((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S)) -> (A.u e. (subSp` <.S, J>.)A.v e. (subSp` <.S, J>.)((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> S =/= (u u. v)) -> -. S C_ (x u. y)))))
63	62	com34 40	. . . . 5 |- ((J e. Top /\ S C_ X) -> ((x e. J /\ y e. J) -> (A.u e. (subSp` <.S, J>.)A.v e. (subSp` <.S, J>.)((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> S =/= (u u. v)) -> (((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S)) -> -. S C_ (x u. y)))))
64	63	com23 36	. . . 4 |- ((J e. Top /\ S C_ X) -> (A.u e. (subSp` <.S, J>.)A.v e. (subSp` <.S, J>.)((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> S =/= (u u. v)) -> ((x e. J /\ y e. J) -> (((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S)) -> -. S C_ (x u. y)))))
65	64	r19.21advv 2184	. . 3 |- ((J e. Top /\ S C_ X) -> (A.u e. (subSp` <.S, J>.)A.v e. (subSp` <.S, J>.)((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> S =/= (u u. v)) -> A.x e. J A.y e. J (((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S)) -> -. S C_ (x u. y))))
66		ssexg 3457	. . . . . . . . 9 |- ((S C_ U.J /\ U.J e. _V) -> S e. _V)
67	66	ancoms 484	. . . . . . . 8 |- ((U.J e. _V /\ S C_ U.J) -> S e. _V)
68		uniexg 3795	. . . . . . . 8 |- (J e. Top -> U.J e. _V)
69	3	biimpi 168	. . . . . . . 8 |- (S C_ X -> S C_ U.J)
70	67, 68, 69	syl2an 503	. . . . . . 7 |- ((J e. Top /\ S C_ X) -> S e. _V)
71		visset 2295	. . . . . . . . 9 |- u e. _V
72		issubspt 10247	. . . . . . . . 9 |- ((J e. Top /\ u e. _V /\ S e. _V) -> (u e. (subSp` <.S, J>.) <-> E.r e. J u = (r i^i S)))
73	71, 72	mp3an2 1179	. . . . . . . 8 |- ((J e. Top /\ S e. _V) -> (u e. (subSp` <.S, J>.) <-> E.r e. J u = (r i^i S)))
74		visset 2295	. . . . . . . . 9 |- v e. _V
75		issubspt 10247	. . . . . . . . 9 |- ((J e. Top /\ v e. _V /\ S e. _V) -> (v e. (subSp` <.S, J>.) <-> E.s e. J v = (s i^i S)))
76	74, 75	mp3an2 1179	. . . . . . . 8 |- ((J e. Top /\ S e. _V) -> (v e. (subSp` <.S, J>.) <-> E.s e. J v = (s i^i S)))
77	73, 76	anbi12d 690	. . . . . . 7 |- ((J e. Top /\ S e. _V) -> ((u e. (subSp` <.S, J>.) /\ v e. (subSp` <.S, J>.)) <-> (E.r e. J u = (r i^i S) /\ E.s e. J v = (s i^i S))))
78	70, 77	syldan 516	. . . . . 6 |- ((J e. Top /\ S C_ X) -> ((u e. (subSp` <.S, J>.) /\ v e. (subSp` <.S, J>.)) <-> (E.r e. J u = (r i^i S) /\ E.s e. J v = (s i^i S))))
79		ineq1 2789	. . . . . . . . . . . . . . 15 |- (x = r -> (x i^i S) = (r i^i S))
80	79	neeq1d 2028	. . . . . . . . . . . . . 14 |- (x = r -> ((x i^i S) =/= (/) <-> (r i^i S) =/= (/)))
81		ineq1 2789	. . . . . . . . . . . . . . 15 |- (x = r -> (x i^i y) = (r i^i y))
82	81	sseq1d 2644	. . . . . . . . . . . . . 14 |- (x = r -> ((x i^i y) C_ (X \ S) <-> (r i^i y) C_ (X \ S)))
83	80, 82	3anbi13d 1170	. . . . . . . . . . . . 13 |- (x = r -> (((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S)) <-> ((r i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (r i^i y) C_ (X \ S))))
84		uneq1 2748	. . . . . . . . . . . . . . 15 |- (x = r -> (x u. y) = (r u. y))
85	84	sseq2d 2645	. . . . . . . . . . . . . 14 |- (x = r -> (S C_ (x u. y) <-> S C_ (r u. y)))
86	85	notbid 673	. . . . . . . . . . . . 13 |- (x = r -> (-. S C_ (x u. y) <-> -. S C_ (r u. y)))
87	83, 86	imbi12d 688	. . . . . . . . . . . 12 |- (x = r -> ((((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S)) -> -. S C_ (x u. y)) <-> (((r i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (r i^i y) C_ (X \ S)) -> -. S C_ (r u. y))))
88		ineq1 2789	. . . . . . . . . . . . . . 15 |- (y = s -> (y i^i S) = (s i^i S))
89	88	neeq1d 2028	. . . . . . . . . . . . . 14 |- (y = s -> ((y i^i S) =/= (/) <-> (s i^i S) =/= (/)))
90		ineq2 2790	. . . . . . . . . . . . . . 15 |- (y = s -> (r i^i y) = (r i^i s))
91	90	sseq1d 2644	. . . . . . . . . . . . . 14 |- (y = s -> ((r i^i y) C_ (X \ S) <-> (r i^i s) C_ (X \ S)))
92	89, 91	3anbi23d 1171	. . . . . . . . . . . . 13 |- (y = s -> (((r i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (r i^i y) C_ (X \ S)) <-> ((r i^i S) =/= (/) /\ (s i^i S) =/= (/) /\ (r i^i s) C_ (X \ S))))
93		uneq2 2749	. . . . . . . . . . . . . . 15 |- (y = s -> (r u. y) = (r u. s))
94	93	sseq2d 2645	. . . . . . . . . . . . . 14 |- (y = s -> (S C_ (r u. y) <-> S C_ (r u. s)))
95	94	notbid 673	. . . . . . . . . . . . 13 |- (y = s -> (-. S C_ (r u. y) <-> -. S C_ (r u. s)))
96	92, 95	imbi12d 688	. . . . . . . . . . . 12 |- (y = s -> ((((r i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (r i^i y) C_ (X \ S)) -> -. S C_ (r u. y)) <-> (((r i^i S) =/= (/) /\ (s i^i S) =/= (/) /\ (r i^i s) C_ (X \ S)) -> -. S C_ (r u. s))))
97	87, 96	rcla42v 2384	. . . . . . . . . . 11 |- ((r e. J /\ s e. J) -> (A.x e. J A.y e. J (((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S)) -> -. S C_ (x u. y)) -> (((r i^i S) =/= (/) /\ (s i^i S) =/= (/) /\ (r i^i s) C_ (X \ S)) -> -. S C_ (r u. s))))
98	97	3ad2ant2 898	. . . . . . . . . 10 |- (((J e. Top /\ S C_ X) /\ (r e. J /\ s e. J) /\ (u = (r i^i S) /\ v = (s i^i S))) -> (A.x e. J A.y e. J (((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S)) -> -. S C_ (x u. y)) -> (((r i^i S) =/= (/) /\ (s i^i S) =/= (/) /\ (r i^i s) C_ (X \ S)) -> -. S C_ (r u. s))))
99		neeq1 2024	. . . . . . . . . . . . . . . . . 18 |- (u = (r i^i S) -> (u =/= (/) <-> (r i^i S) =/= (/)))
100	99	biimpa 460	. . . . . . . . . . . . . . . . 17 |- ((u = (r i^i S) /\ u =/= (/)) -> (r i^i S) =/= (/))
101	100	3ad2antr1 1041	. . . . . . . . . . . . . . . 16 |- ((u = (r i^i S) /\ (u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/))) -> (r i^i S) =/= (/))
102	101	adantlr 429	. . . . . . . . . . . . . . 15 |- (((u = (r i^i S) /\ v = (s i^i S)) /\ (u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/))) -> (r i^i S) =/= (/))
103	102	3ad2antl3 1040	. . . . . . . . . . . . . 14 |- ((((J e. Top /\ S C_ X) /\ (r e. J /\ s e. J) /\ (u = (r i^i S) /\ v = (s i^i S))) /\ (u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/))) -> (r i^i S) =/= (/))
104		neeq1 2024	. . . . . . . . . . . . . . . . . 18 |- (v = (s i^i S) -> (v =/= (/) <-> (s i^i S) =/= (/)))
105	104	biimpa 460	. . . . . . . . . . . . . . . . 17 |- ((v = (s i^i S) /\ v =/= (/)) -> (s i^i S) =/= (/))
106	105	3ad2antr2 1042	. . . . . . . . . . . . . . . 16 |- ((v = (s i^i S) /\ (u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/))) -> (s i^i S) =/= (/))
107	106	adantll 428	. . . . . . . . . . . . . . 15 |- (((u = (r i^i S) /\ v = (s i^i S)) /\ (u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/))) -> (s i^i S) =/= (/))
108	107	3ad2antl3 1040	. . . . . . . . . . . . . 14 |- ((((J e. Top /\ S C_ X) /\ (r e. J /\ s e. J) /\ (u = (r i^i S) /\ v = (s i^i S))) /\ (u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/))) -> (s i^i S) =/= (/))
109		ineq12 2791	. . . . . . . . . . . . . . . . . . . 20 |- ((u = (r i^i S) /\ v = (s i^i S)) -> (u i^i v) = ((r i^i S) i^i (s i^i S)))
110	109	eqeq1d 1892	. . . . . . . . . . . . . . . . . . 19 |- ((u = (r i^i S) /\ v = (s i^i S)) -> ((u i^i v) = (/) <-> ((r i^i S) i^i (s i^i S)) = (/)))
111	110	biimpa 460	. . . . . . . . . . . . . . . . . 18 |- (((u = (r i^i S) /\ v = (s i^i S)) /\ (u i^i v) = (/)) -> ((r i^i S) i^i (s i^i S)) = (/))
112	111	3ad2antl3 1040	. . . . . . . . . . . . . . . . 17 |- ((((J e. Top /\ S C_ X) /\ (r e. J /\ s e. J) /\ (u = (r i^i S) /\ v = (s i^i S))) /\ (u i^i v) = (/)) -> ((r i^i S) i^i (s i^i S)) = (/))
113	112	3ad2antr3 1043	. . . . . . . . . . . . . . . 16 |- ((((J e. Top /\ S C_ X) /\ (r e. J /\ s e. J) /\ (u = (r i^i S) /\ v = (s i^i S))) /\ (u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/))) -> ((r i^i S) i^i (s i^i S)) = (/))
114		inindir 2810	. . . . . . . . . . . . . . . 16 |- ((r i^i s) i^i S) = ((r i^i S) i^i (s i^i S))
115	113, 114	syl5eq 1940	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ S C_ X) /\ (r e. J /\ s e. J) /\ (u = (r i^i S) /\ v = (s i^i S))) /\ (u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/))) -> ((r i^i s) i^i S) = (/))
116	2	eltopss 8872	. . . . . . . . . . . . . . . . . . . 20 |- ((J e. Top /\ r e. J) -> r C_ X)
117		ssinss1 2821	. . . . . . . . . . . . . . . . . . . 20 |- (r C_ X -> (r i^i s) C_ X)
118	116, 117	syl 12	. . . . . . . . . . . . . . . . . . 19 |- ((J e. Top /\ r e. J) -> (r i^i s) C_ X)
119	118	ad2ant2r 445	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ S C_ X) /\ (r e. J /\ s e. J)) -> (r i^i s) C_ X)
120	119	3adant3 896	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ S C_ X) /\ (r e. J /\ s e. J) /\ (u = (r i^i S) /\ v = (s i^i S))) -> (r i^i s) C_ X)
121	120	adantr 425	. . . . . . . . . . . . . . . 16 |- ((((J e. Top /\ S C_ X) /\ (r e. J /\ s e. J) /\ (u = (r i^i S) /\ v = (s i^i S))) /\ (u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/))) -> (r i^i s) C_ X)
122		reldisj 2916	. . . . . . . . . . . . . . . 16 |- ((r i^i s) C_ X -> (((r i^i s) i^i S) = (/) <-> (r i^i s) C_ (X \ S)))
123	121, 122	syl 12	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ S C_ X) /\ (r e. J /\ s e. J) /\ (u = (r i^i S) /\ v = (s i^i S))) /\ (u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/))) -> (((r i^i s) i^i S) = (/) <-> (r i^i s) C_ (X \ S)))
124	115, 123	mpbid 212	. . . . . . . . . . . . . 14 |- ((((J e. Top /\ S C_ X) /\ (r e. J /\ s e. J) /\ (u = (r i^i S) /\ v = (s i^i S))) /\ (u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/))) -> (r i^i s) C_ (X \ S))
125	103, 108, 124	3jca 1050	. . . . . . . . . . . . 13 |- ((((J e. Top /\ S C_ X) /\ (r e. J /\ s e. J) /\ (u = (r i^i S) /\ v = (s i^i S))) /\ (u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/))) -> ((r i^i S) =/= (/) /\ (s i^i S) =/= (/) /\ (r i^i s) C_ (X \ S)))
126		pm2.27 76	. . . . . . . . . . . . . 14 |- (((r i^i S) =/= (/) /\ (s i^i S) =/= (/) /\ (r i^i s) C_ (X \ S)) -> ((((r i^i S) =/= (/) /\ (s i^i S) =/= (/) /\ (r i^i s) C_ (X \ S)) -> -. S C_ (r u. s)) -> -. S C_ (r u. s)))
127		sseq1 2637	. . . . . . . . . . . . . . . . . . . 20 |- (S = (u u. v) -> (S C_ (r u. s) <-> (u u. v) C_ (r u. s)))
128		unss12 2778	. . . . . . . . . . . . . . . . . . . 20 |- ((u C_ r /\ v C_ s) -> (u u. v) C_ (r u. s))
129	127, 128	syl5cbir 228	. . . . . . . . . . . . . . . . . . 19 |- ((u C_ r /\ v C_ s) -> (S = (u u. v) -> S C_ (r u. s)))
130	129	a1d 15	. . . . . . . . . . . . . . . . . 18 |- ((u C_ r /\ v C_ s) -> ((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> (S = (u u. v) -> S C_ (r u. s))))
131	130	3ad2ant3 899	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ S C_ X) /\ (r e. J /\ s e. J) /\ (u C_ r /\ v C_ s)) -> ((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> (S = (u u. v) -> S C_ (r u. s))))
132		inss1 2812	. . . . . . . . . . . . . . . . . . 19 |- (r i^i S) C_ r
133		sseq1 2637	. . . . . . . . . . . . . . . . . . 19 |- (u = (r i^i S) -> (u C_ r <-> (r i^i S) C_ r))
134	132, 133	mpbiri 211	. . . . . . . . . . . . . . . . . 18 |- (u = (r i^i S) -> u C_ r)
135		inss1 2812	. . . . . . . . . . . . . . . . . . 19 |- (s i^i S) C_ s
136		sseq1 2637	. . . . . . . . . . . . . . . . . . 19 |- (v = (s i^i S) -> (v C_ s <-> (s i^i S) C_ s))
137	135, 136	mpbiri 211	. . . . . . . . . . . . . . . . . 18 |- (v = (s i^i S) -> v C_ s)
138	134, 137	anim12i 360	. . . . . . . . . . . . . . . . 17 |- ((u = (r i^i S) /\ v = (s i^i S)) -> (u C_ r /\ v C_ s))
139	131, 138	syl3an3 1132	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ S C_ X) /\ (r e. J /\ s e. J) /\ (u = (r i^i S) /\ v = (s i^i S))) -> ((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> (S = (u u. v) -> S C_ (r u. s))))
140	139	imp 377	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ S C_ X) /\ (r e. J /\ s e. J) /\ (u = (r i^i S) /\ v = (s i^i S))) /\ (u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/))) -> (S = (u u. v) -> S C_ (r u. s)))
141	140	necon3bd 2039	. . . . . . . . . . . . . 14 |- ((((J e. Top /\ S C_ X) /\ (r e. J /\ s e. J) /\ (u = (r i^i S) /\ v = (s i^i S))) /\ (u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/))) -> (-. S C_ (r u. s) -> S =/= (u u. v)))
142	126, 141	syl9r 72	. . . . . . . . . . . . 13 |- ((((J e. Top /\ S C_ X) /\ (r e. J /\ s e. J) /\ (u = (r i^i S) /\ v = (s i^i S))) /\ (u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/))) -> (((r i^i S) =/= (/) /\ (s i^i S) =/= (/) /\ (r i^i s) C_ (X \ S)) -> ((((r i^i S) =/= (/) /\ (s i^i S) =/= (/) /\ (r i^i s) C_ (X \ S)) -> -. S C_ (r u. s)) -> S =/= (u u. v))))
143	125, 142	mpd 29	. . . . . . . . . . . 12 |- ((((J e. Top /\ S C_ X) /\ (r e. J /\ s e. J) /\ (u = (r i^i S) /\ v = (s i^i S))) /\ (u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/))) -> ((((r i^i S) =/= (/) /\ (s i^i S) =/= (/) /\ (r i^i s) C_ (X \ S)) -> -. S C_ (r u. s)) -> S =/= (u u. v)))
144	143	ex 402	. . . . . . . . . . 11 |- (((J e. Top /\ S C_ X) /\ (r e. J /\ s e. J) /\ (u = (r i^i S) /\ v = (s i^i S))) -> ((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> ((((r i^i S) =/= (/) /\ (s i^i S) =/= (/) /\ (r i^i s) C_ (X \ S)) -> -. S C_ (r u. s)) -> S =/= (u u. v))))
145	144	com23 36	. . . . . . . . . 10 |- (((J e. Top /\ S C_ X) /\ (r e. J /\ s e. J) /\ (u = (r i^i S) /\ v = (s i^i S))) -> ((((r i^i S) =/= (/) /\ (s i^i S) =/= (/) /\ (r i^i s) C_ (X \ S)) -> -. S C_ (r u. s)) -> ((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> S =/= (u u. v))))
146	98, 145	syld 30	. . . . . . . . 9 |- (((J e. Top /\ S C_ X) /\ (r e. J /\ s e. J) /\ (u = (r i^i S) /\ v = (s i^i S))) -> (A.x e. J A.y e. J (((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S)) -> -. S C_ (x u. y)) -> ((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> S =/= (u u. v))))
147	146	3exp 1066	. . . . . . . 8 |- ((J e. Top /\ S C_ X) -> ((r e. J /\ s e. J) -> ((u = (r i^i S) /\ v = (s i^i S)) -> (A.x e. J A.y e. J (((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S)) -> -. S C_ (x u. y)) -> ((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> S =/= (u u. v))))))
148	147	r19.23advv 2218	. . . . . . 7 |- ((J e. Top /\ S C_ X) -> (E.r e. J E.s e. J (u = (r i^i S) /\ v = (s i^i S)) -> (A.x e. J A.y e. J (((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S)) -> -. S C_ (x u. y)) -> ((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> S =/= (u u. v)))))
149		reeanv 2249	. . . . . . 7 |- (E.r e. J E.s e. J (u = (r i^i S) /\ v = (s i^i S)) <-> (E.r e. J u = (r i^i S) /\ E.s e. J v = (s i^i S)))
150	148, 149	syl5ibr 224	. . . . . 6 |- ((J e. Top /\ S C_ X) -> ((E.r e. J u = (r i^i S) /\ E.s e. J v = (s i^i S)) -> (A.x e. J A.y e. J (((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S)) -> -. S C_ (x u. y)) -> ((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> S =/= (u u. v)))))
151	78, 150	sylbid 220	. . . . 5 |- ((J e. Top /\ S C_ X) -> ((u e. (subSp` <.S, J>.) /\ v e. (subSp` <.S, J>.)) -> (A.x e. J A.y e. J (((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S)) -> -. S C_ (x u. y)) -> ((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> S =/= (u u. v)))))
152	151	com23 36	. . . 4 |- ((J e. Top /\ S C_ X) -> (A.x e. J A.y e. J (((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S)) -> -. S C_ (x u. y)) -> ((u e. (subSp` <.S, J>.) /\ v e. (subSp` <.S, J>.)) -> ((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> S =/= (u u. v)))))
153	152	r19.21advv 2184	. . 3 |- ((J e. Top /\ S C_ X) -> (A.x e. J A.y e. J (((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S)) -> -. S C_ (x u. y)) -> A.u e. (subSp` <.S, J>.)A.v e. (subSp` <.S, J>.)((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> S =/= (u u. v))))
154	65, 153	impbid 574	. 2 |- ((J e. Top /\ S C_ X) -> (A.u e. (subSp` <.S, J>.)A.v e. (subSp` <.S, J>.)((u =/= (/) /\ v =/= (/) /\ (u i^i v) = (/)) -> S =/= (u u. v)) <-> A.x e. J A.y e. J (((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S)) -> -. S C_ (x u. y))))
155	7, 13, 154	3bitrd 603	1 |- ((J e. Top /\ S C_ X) -> ((subSp` <.S, J>.) e. Con <-> A.x e. J A.y e. J (((x i^i S) =/= (/) /\ (y i^i S) =/= (/) /\ (x i^i y) C_ (X \ S)) -> -. S C_ (x u. y))))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300   =/= wne 2017  A.wral 2105  E.wrex 2106  _Vcvv 2292   \ cdif 2590   u. cun 2591   i^i cin 2592   C_ wss 2593  (/)c0 2875  <.cop 3046  U.cuni 3177  ` cfv 3998  Topctop 8857  subSpcsubsp 10242  Conccon 10337

This theorem is referenced by:  reconnlem1 15446  reconn 15451

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-cld 8939  df-subsp 10243  df-con 10338

Copyright terms: Public domain