Theorem cptclsscpt 11489

Description: A closed subset of a compact space is compact.

Assertion

Ref	Expression
cptclsscpt	|- ((J e. Comp /\ S e. (Clsd` J)) -> (subSp` <.S, J>.) e. Comp)

Proof of Theorem cptclsscpt

Step	Hyp	Ref	Expression
1		eqid 1518	. . . . . . . 8 |- U.J = U.J
2	1	compcov 11486	. . . . . . 7 |- ((J e. Comp /\ (s u. {(U.J \ S)}) (_ J /\ U.J = U.(s u. {(U.J \ S)})) -> E.u e. (P~(s u. {(U.J \ S)}) i^i Fin)U.J = U.u)
3		simpll 412	. . . . . . . 8 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J) -> J e. Comp)
4	3	3adant3 805	. . . . . . 7 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) -> J e. Comp)
5		3simp2 795	. . . . . . . . 9 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) -> s (_ J)
6	1	cldopn 7882	. . . . . . . . . . . 12 |- ((J e. Top /\ S e. (Clsd` J)) -> (U.J \ S) e. J)
7		comptop 11485	. . . . . . . . . . . 12 |- (J e. Comp -> J e. Top)
8	6, 7	sylan 450	. . . . . . . . . . 11 |- ((J e. Comp /\ S e. (Clsd` J)) -> (U.J \ S) e. J)
9	8	3ad2ant1 806	. . . . . . . . . 10 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) -> (U.J \ S) e. J)
10		snssi 2530	. . . . . . . . . 10 |- ((U.J \ S) e. J -> {(U.J \ S)} (_ J)
11	9, 10	syl 10	. . . . . . . . 9 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) -> {(U.J \ S)} (_ J)
12	5, 11	jca 286	. . . . . . . 8 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) -> (s (_ J /\ {(U.J \ S)} (_ J))
13		unss 2256	. . . . . . . 8 |- ((s (_ J /\ {(U.J \ S)} (_ J) <-> (s u. {(U.J \ S)}) (_ J)
14	12, 13	sylib 196	. . . . . . 7 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) -> (s u. {(U.J \ S)}) (_ J)
15		3simp3 796	. . . . . . . . . . . . 13 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) -> S (_ U.s)
16		uniss 2588	. . . . . . . . . . . . . 14 |- (s (_ J -> U.s (_ U.J)
17	16	3ad2ant2 807	. . . . . . . . . . . . 13 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) -> U.s (_ U.J)
18	15, 17	sstrd 2126	. . . . . . . . . . . 12 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) -> S (_ U.J)
19		undif 2397	. . . . . . . . . . . 12 |- (S (_ U.J <-> (S u. (U.J \ S)) = U.J)
20	18, 19	sylib 196	. . . . . . . . . . 11 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) -> (S u. (U.J \ S)) = U.J)
21		unss1 2251	. . . . . . . . . . . 12 |- (S (_ U.s -> (S u. (U.J \ S)) (_ (U.s u. (U.J \ S)))
22	21	3ad2ant3 808	. . . . . . . . . . 11 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) -> (S u. (U.J \ S)) (_ (U.s u. (U.J \ S)))
23	20, 22	eqsstr3d 2148	. . . . . . . . . 10 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) -> U.J (_ (U.s u. (U.J \ S)))
24		difss 2219	. . . . . . . . . . . 12 |- (U.J \ S) (_ U.J
25	17, 24	jctir 291	. . . . . . . . . . 11 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) -> (U.s (_ U.J /\ (U.J \ S) (_ U.J))
26		unss 2256	. . . . . . . . . . 11 |- ((U.s (_ U.J /\ (U.J \ S) (_ U.J) <-> (U.s u. (U.J \ S)) (_ U.J)
27	25, 26	sylib 196	. . . . . . . . . 10 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) -> (U.s u. (U.J \ S)) (_ U.J)
28	23, 27	eqssd 2131	. . . . . . . . 9 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) -> U.J = (U.s u. (U.J \ S)))
29		uniexg 3094	. . . . . . . . . . . . 13 |- (J e. Comp -> U.J e. V)
30	29	ad2antrr 404	. . . . . . . . . . . 12 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J) -> U.J e. V)
31	30	3adant3 805	. . . . . . . . . . 11 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) -> U.J e. V)
32		difexg 2796	. . . . . . . . . . 11 |- (U.J e. V -> (U.J \ S) e. V)
33		unisng 2585	. . . . . . . . . . 11 |- ((U.J \ S) e. V -> U.{(U.J \ S)} = (U.J \ S))
34	31, 32, 33	3syl 20	. . . . . . . . . 10 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) -> U.{(U.J \ S)} = (U.J \ S))
35	34	uneq2d 2236	. . . . . . . . 9 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) -> (U.s u. U.{(U.J \ S)}) = (U.s u. (U.J \ S)))
36	28, 35	eqtr4d 1553	. . . . . . . 8 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) -> U.J = (U.s u. U.{(U.J \ S)}))
37		uniun 2586	. . . . . . . 8 |- U.(s u. {(U.J \ S)}) = (U.s u. U.{(U.J \ S)})
38	36, 37	syl6eqr 1568	. . . . . . 7 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) -> U.J = U.(s u. {(U.J \ S)}))
39	2, 4, 14, 38	syl3anc 864	. . . . . 6 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) -> E.u e. (P~(s u. {(U.J \ S)}) i^i Fin)U.J = U.u)
40		unieq 2576	. . . . . . . . . . . 12 |- (t = (u \ {(U.J \ S)}) -> U.t = U.(u \ {(U.J \ S)}))
41	40	sseq2d 2141	. . . . . . . . . . 11 |- (t = (u \ {(U.J \ S)}) -> (S (_ U.t <-> S (_ U.(u \ {(U.J \ S)})))
42	41	rcla4ev 1923	. . . . . . . . . 10 |- (((u \ {(U.J \ S)}) e. (P~s i^i Fin) /\ S (_ U.(u \ {(U.J \ S)})) -> E.t e. (P~s i^i Fin)S (_ U.t)
43		simprl 414	. . . . . . . . . . . . . . 15 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin)) -> u (_ (s u. {(U.J \ S)}))
44	43	3adant3 805	. . . . . . . . . . . . . 14 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> u (_ (s u. {(U.J \ S)}))
45		uncom 2228	. . . . . . . . . . . . . 14 |- (s u. {(U.J \ S)}) = ({(U.J \ S)} u. s)
46	44, 45	syl6ss 2159	. . . . . . . . . . . . 13 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> u (_ ({(U.J \ S)} u. s))
47		ssundif 2398	. . . . . . . . . . . . 13 |- (u (_ ({(U.J \ S)} u. s) <-> (u \ {(U.J \ S)}) (_ s)
48	46, 47	sylib 196	. . . . . . . . . . . 12 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> (u \ {(U.J \ S)}) (_ s)
49		difss 2219	. . . . . . . . . . . . . . 15 |- (u \ {(U.J \ S)}) (_ u
50		ssfi 4683	. . . . . . . . . . . . . . 15 |- ((u e. Fin /\ (u \ {(U.J \ S)}) (_ u) -> (u \ {(U.J \ S)}) e. Fin)
51	49, 50	mpan2 700	. . . . . . . . . . . . . 14 |- (u e. Fin -> (u \ {(U.J \ S)}) e. Fin)
52	51	ad2antll 407	. . . . . . . . . . . . 13 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin)) -> (u \ {(U.J \ S)}) e. Fin)
53	52	3adant3 805	. . . . . . . . . . . 12 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> (u \ {(U.J \ S)}) e. Fin)
54	48, 53	jca 286	. . . . . . . . . . 11 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> ((u \ {(U.J \ S)}) (_ s /\ (u \ {(U.J \ S)}) e. Fin))
55		elin 2259	. . . . . . . . . . . 12 |- ((u \ {(U.J \ S)}) e. (P~s i^i Fin) <-> ((u \ {(U.J \ S)}) e. P~s /\ (u \ {(U.J \ S)}) e. Fin))
56		visset 1859	. . . . . . . . . . . . . . 15 |- u e. V
57	56, 49	ssexi 2794	. . . . . . . . . . . . . 14 |- (u \ {(U.J \ S)}) e. V
58	57	elpw 2461	. . . . . . . . . . . . 13 |- ((u \ {(U.J \ S)}) e. P~s <-> (u \ {(U.J \ S)}) (_ s)
59	58	anbi1i 484	. . . . . . . . . . . 12 |- (((u \ {(U.J \ S)}) e. P~s /\ (u \ {(U.J \ S)}) e. Fin) <-> ((u \ {(U.J \ S)}) (_ s /\ (u \ {(U.J \ S)}) e. Fin))
60	55, 59	bitri 171	. . . . . . . . . . 11 |- ((u \ {(U.J \ S)}) e. (P~s i^i Fin) <-> ((u \ {(U.J \ S)}) (_ s /\ (u \ {(U.J \ S)}) e. Fin))
61	54, 60	sylibr 198	. . . . . . . . . 10 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> (u \ {(U.J \ S)}) e. (P~s i^i Fin))
62	15	3ad2ant1 806	. . . . . . . . . . . . . . . . . 18 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> S (_ U.s)
63	17	3ad2ant1 806	. . . . . . . . . . . . . . . . . . 19 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> U.s (_ U.J)
64		3simp3 796	. . . . . . . . . . . . . . . . . . 19 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> U.J = U.u)
65	63, 64	sseqtrd 2149	. . . . . . . . . . . . . . . . . 18 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> U.s (_ U.u)
66	62, 65	sstrd 2126	. . . . . . . . . . . . . . . . 17 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> S (_ U.u)
67	66	sseld 2119	. . . . . . . . . . . . . . . 16 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> (v e. S -> v e. U.u))
68	67	imp 348	. . . . . . . . . . . . . . 15 |- (((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) /\ v e. S) -> v e. U.u)
69		eluni 2572	. . . . . . . . . . . . . . 15 |- (v e. U.u <-> E.w(v e. w /\ w e. u))
70	68, 69	sylib 196	. . . . . . . . . . . . . 14 |- (((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) /\ v e. S) -> E.w(v e. w /\ w e. u))
71		pm3.26 317	. . . . . . . . . . . . . . . . 17 |- ((v e. w /\ w e. u) -> v e. w)
72	71	a1i 8	. . . . . . . . . . . . . . . 16 |- (((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) /\ v e. S) -> ((v e. w /\ w e. u) -> v e. w))
73		pm3.27 321	. . . . . . . . . . . . . . . . . . 19 |- ((v e. w /\ w e. u) -> w e. u)
74	73	a1i 8	. . . . . . . . . . . . . . . . . 18 |- (((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) /\ v e. S) -> ((v e. w /\ w e. u) -> w e. u))
75		elndif 2216	. . . . . . . . . . . . . . . . . . . . . . 23 |- (v e. S -> -. v e. (U.J \ S))
76	75	ad2antlr 405	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) /\ v e. S) /\ v e. w) -> -. v e. (U.J \ S))
77		eleq2 1578	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (w = (U.J \ S) -> (v e. w <-> v e. (U.J \ S)))
78	77	biimpd 151	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (w = (U.J \ S) -> (v e. w -> v e. (U.J \ S)))
79	78	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) /\ v e. S) -> (w = (U.J \ S) -> (v e. w -> v e. (U.J \ S))))
80	79	com23 32	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) /\ v e. S) -> (v e. w -> (w = (U.J \ S) -> v e. (U.J \ S))))
81	80	imp 348	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) /\ v e. S) /\ v e. w) -> (w = (U.J \ S) -> v e. (U.J \ S)))
82	76, 81	mtod 107	. . . . . . . . . . . . . . . . . . . . 21 |- ((((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) /\ v e. S) /\ v e. w) -> -. w = (U.J \ S))
83	82	ex 371	. . . . . . . . . . . . . . . . . . . 20 |- (((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) /\ v e. S) -> (v e. w -> -. w = (U.J \ S)))
84	83	adantrd 391	. . . . . . . . . . . . . . . . . . 19 |- (((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) /\ v e. S) -> ((v e. w /\ w e. u) -> -. w = (U.J \ S)))
85		elsn 2479	. . . . . . . . . . . . . . . . . . . 20 |- (w e. {(U.J \ S)} <-> w = (U.J \ S))
86	85	notbii 185	. . . . . . . . . . . . . . . . . . 19 |- (-. w e. {(U.J \ S)} <-> -. w = (U.J \ S))
87	84, 86	syl6ibr 211	. . . . . . . . . . . . . . . . . 18 |- (((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) /\ v e. S) -> ((v e. w /\ w e. u) -> -. w e. {(U.J \ S)}))
88	74, 87	jcad 603	. . . . . . . . . . . . . . . . 17 |- (((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) /\ v e. S) -> ((v e. w /\ w e. u) -> (w e. u /\ -. w e. {(U.J \ S)})))
89		eldif 2109	. . . . . . . . . . . . . . . . 17 |- (w e. (u \ {(U.J \ S)}) <-> (w e. u /\ -. w e. {(U.J \ S)}))
90	88, 89	syl6ibr 211	. . . . . . . . . . . . . . . 16 |- (((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) /\ v e. S) -> ((v e. w /\ w e. u) -> w e. (u \ {(U.J \ S)})))
91	72, 90	jcad 603	. . . . . . . . . . . . . . 15 |- (((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) /\ v e. S) -> ((v e. w /\ w e. u) -> (v e. w /\ w e. (u \ {(U.J \ S)}))))
92	91	19.22dv 1328	. . . . . . . . . . . . . 14 |- (((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) /\ v e. S) -> (E.w(v e. w /\ w e. u) -> E.w(v e. w /\ w e. (u \ {(U.J \ S)}))))
93	70, 92	mpd 26	. . . . . . . . . . . . 13 |- (((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) /\ v e. S) -> E.w(v e. w /\ w e. (u \ {(U.J \ S)})))
94	93	ex 371	. . . . . . . . . . . 12 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> (v e. S -> E.w(v e. w /\ w e. (u \ {(U.J \ S)}))))
95		eluni 2572	. . . . . . . . . . . 12 |- (v e. U.(u \ {(U.J \ S)}) <-> E.w(v e. w /\ w e. (u \ {(U.J \ S)})))
96	94, 95	syl6ibr 211	. . . . . . . . . . 11 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> (v e. S -> v e. U.(u \ {(U.J \ S)})))
97	96	ssrdv 2122	. . . . . . . . . 10 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> S (_ U.(u \ {(U.J \ S)}))
98	42, 61, 97	sylanc 473	. . . . . . . . 9 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ (u (_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> E.t e. (P~s i^i Fin)S (_ U.t)
99		elin 2259	. . . . . . . . . 10 |- (u e. (P~(s u. {(U.J \ S)}) i^i Fin) <-> (u e. P~(s u. {(U.J \ S)}) /\ u e. Fin))
100	56	elpw 2461	. . . . . . . . . . 11 |- (u e. P~(s u. {(U.J \ S)}) <-> u (_ (s u. {(U.J \ S)}))
101	100	anbi1i 484	. . . . . . . . . 10 |- ((u e. P~(s u. {(U.J \ S)}) /\ u e. Fin) <-> (u (_ (s u. {(U.J \ S)}) /\ u e. Fin))
102	99, 101	bitri 171	. . . . . . . . 9 |- (u e. (P~(s u. {(U.J \ S)}) i^i Fin) <-> (u (_ (s u. {(U.J \ S)}) /\ u e. Fin))
103	98, 102	syl3an2b 869	. . . . . . . 8 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) /\ u e. (P~(s u. {(U.J \ S)}) i^i Fin) /\ U.J = U.u) -> E.t e. (P~s i^i Fin)S (_ U.t)
104	103	3exp 838	. . . . . . 7 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) -> (u e. (P~(s u. {(U.J \ S)}) i^i Fin) -> (U.J = U.u -> E.t e. (P~s i^i Fin)S (_ U.t)))
105	104	r19.23adv 1792	. . . . . 6 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) -> (E.u e. (P~(s u. {(U.J \ S)}) i^i Fin)U.J = U.u -> E.t e. (P~s i^i Fin)S (_ U.t))
106	39, 105	mpd 26	. . . . 5 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s (_ J /\ S (_ U.s) -> E.t e. (P~s i^i Fin)S (_ U.t)
107	106	3exp 838	. . . 4 |- ((J e. Comp /\ S e. (Clsd` J)) -> (s (_ J -> (S (_ U.s -> E.t e. (P~s i^i Fin)S (_ U.t)))
108		visset 1859	. . . . 5 |- s e. V
109	108	elpw 2461	. . . 4 |- (s e. P~J <-> s (_ J)
110	107, 109	syl5ib 204	. . 3 |- ((J e. Comp /\ S e. (Clsd` J)) -> (s e. P~J -> (S (_ U.s -> E.t e. (P~s i^i Fin)S (_ U.t)))
111	110	r19.21aiv 1759	. 2 |- ((J e. Comp /\ S e. (Clsd` J)) -> A.s e. P~ J(S (_ U.s -> E.t e. (P~s i^i Fin)S (_ U.t))
112	1	cldss 7881	. . . 4 |- ((J e. Top /\ S e. (Clsd` J)) -> S (_ U.J)
113	1	compsub 11488	. . . 4 |- ((J e. Top /\ S (_ U.J) -> ((subSp` <.S, J>.) e. Comp <-> A.s e. P~ J(S (_ U.s -> E.t e. (P~s i^i Fin)S (_ U.t)))
114	112, 113	syldan 469	. . 3 |- ((J e. Top /\ S e. (Clsd` J)) -> ((subSp` <.S, J>.) e. Comp <-> A.s e. P~ J(S (_ U.s -> E.t e. (P~s i^i Fin)S (_ U.t)))
115	114, 7	sylan 450	. 2 |- ((J e. Comp /\ S e. (Clsd` J)) -> ((subSp` <.S, J>.) e. Comp <-> A.s e. P~ J(S (_ U.s -> E.t e. (P~s i^i Fin)S (_ U.t)))
116	111, 115	mpbird 194	1 |- ((J e. Comp /\ S e. (Clsd` J)) -> (subSp` <.S, J>.) e. Comp)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 144   /\ wa 221   /\ w3a 781   = wceq 992   e. wcel 994  E.wex 1016  A.wral 1691  E.wrex 1692  Vcvv 1857   \ cdif 2096   u. cun 2097   i^i cin 2098   (_ wss 2099  P~cpw 2458  {csn 2467  <.cop 2469  U.cuni 2569  ` cfv 3263  Fincfn 4508  Topctop 7800  Clsdccld 7870  subSpcsubsp 11054  Compccomp 11112

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-9 1001  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-rep 2767  ax-sep 2777  ax-nul 2784  ax-pow 2818  ax-pr 2855  ax-un 3089  ax-reg 4736

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3or 782  df-3an 783  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-ral 1695  df-rex 1696  df-rab 1698  df-v 1858  df-sbc 1987  df-csb 2052  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-pss 2107  df-nul 2333  df-if 2416  df-pw 2459  df-sn 2470  df-pr 2471  df-tp 2473  df-op 2474  df-uni 2570  df-iun 2635  df-br 2693  df-opab 2741  df-tr 2755  df-eprel 2910  df-id 2913  df-po 2918  df-so 2929  df-fr 2947  df-we 2962  df-ord 2978  df-on 2979  df-lim 2980  df-suc 2981  df-om 3219  df-xp 3265  df-rel 3266  df-cnv 3267  df-co 3268  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fun 3273  df-fn 3274  df-f 3275  df-f1 3276  df-fo 3277  df-f1o 3278  df-fv 3279  df-opr 4023  df-oprab 4024  df-1o 4269  df-er 4401  df-en 4509  df-dom 4510  df-fin 4512  df-top 7804  df-topsp 7805  df-cld 7873  df-subsp 11055  df-comp 11113

Copyright terms: Public domain