Table of ContentsTable of Contents Mathbox for Jeff Hankins < Previous   Next >
Related theorems
Unicode version
Theorem cptclsscpt 15432
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
StepHypRef Expression
1 simp1l 900 . . . . . . 7 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) -> J e. Comp)
2 simp2 877 . . . . . . . . 9 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) -> s C_ J)
3 eqid 1884 . . . . . . . . . . . . 13 |- U.J = U.J
43cldopn 8948 . . . . . . . . . . . 12 |- ((J e. Top /\ S e. (Clsd` J)) -> (U.J \ S) e. J)
5 comptop 15428 . . . . . . . . . . . 12 |- (J e. Comp -> J e. Top)
64, 5sylan 497 . . . . . . . . . . 11 |- ((J e. Comp /\ S e. (Clsd` J)) -> (U.J \ S) e. J)
763ad2ant1 897 . . . . . . . . . 10 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) -> (U.J \ S) e. J)
87snssd 3130 . . . . . . . . 9 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) -> {(U.J \ S)} C_ J)
92, 8jca 310 . . . . . . . 8 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) -> (s C_ J /\ {(U.J \ S)} C_ J))
10 unss 2780 . . . . . . . 8 |- ((s C_ J /\ {(U.J \ S)} C_ J) <-> (s u. {(U.J \ S)}) C_ J)
119, 10sylib 215 . . . . . . 7 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) -> (s u. {(U.J \ S)}) C_ J)
12 simp3 878 . . . . . . . . . . . . 13 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) -> S C_ U.s)
13 uniss 3199 . . . . . . . . . . . . . 14 |- (s C_ J -> U.s C_ U.J)
14133ad2ant2 898 . . . . . . . . . . . . 13 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) -> U.s C_ U.J)
1512, 14sstrd 2627 . . . . . . . . . . . 12 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) -> S C_ U.J)
16 undif 2954 . . . . . . . . . . . 12 |- (S C_ U.J <-> (S u. (U.J \ S)) = U.J)
1715, 16sylib 215 . . . . . . . . . . 11 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) -> (S u. (U.J \ S)) = U.J)
18 unss1 2773 . . . . . . . . . . . 12 |- (S C_ U.s -> (S u. (U.J \ S)) C_ (U.s u. (U.J \ S)))
19183ad2ant3 899 . . . . . . . . . . 11 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) -> (S u. (U.J \ S)) C_ (U.s u. (U.J \ S)))
2017, 19eqsstr3d 2652 . . . . . . . . . 10 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) -> U.J C_ (U.s u. (U.J \ S)))
21 difss 2735 . . . . . . . . . . . 12 |- (U.J \ S) C_ U.J
2214, 21jctir 317 . . . . . . . . . . 11 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) -> (U.s C_ U.J /\ (U.J \ S) C_ U.J))
23 unss 2780 . . . . . . . . . . 11 |- ((U.s C_ U.J /\ (U.J \ S) C_ U.J) <-> (U.s u. (U.J \ S)) C_ U.J)
2422, 23sylib 215 . . . . . . . . . 10 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) -> (U.s u. (U.J \ S)) C_ U.J)
2520, 24eqssd 2633 . . . . . . . . 9 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) -> U.J = (U.s u. (U.J \ S)))
26 uniexg 3795 . . . . . . . . . . . . 13 |- (J e. Comp -> U.J e. _V)
2726ad2antrr 440 . . . . . . . . . . . 12 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J) -> U.J e. _V)
28273adant3 896 . . . . . . . . . . 11 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) -> U.J e. _V)
29 difexg 3458 . . . . . . . . . . 11 |- (U.J e. _V -> (U.J \ S) e. _V)
30 unisng 3194 . . . . . . . . . . 11 |- ((U.J \ S) e. _V -> U.{(U.J \ S)} = (U.J \ S))
3128, 29, 303syl 24 . . . . . . . . . 10 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) -> U.{(U.J \ S)} = (U.J \ S))
3231uneq2d 2755 . . . . . . . . 9 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) -> (U.s u. U.{(U.J \ S)}) = (U.s u. (U.J \ S)))
3325, 32eqtr4d 1928 . . . . . . . 8 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) -> U.J = (U.s u. U.{(U.J \ S)}))
34 uniun 3196 . . . . . . . 8 |- U.(s u. {(U.J \ S)}) = (U.s u. U.{(U.J \ S)})
3533, 34syl6eqr 1946 . . . . . . 7 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) -> U.J = U.(s u. {(U.J \ S)}))
363compcov 15429 . . . . . . 7 |- ((J e. Comp /\ (s u. {(U.J \ S)}) C_ 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)
371, 11, 35, 36syl111anc 1100 . . . . . 6 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) -> E.u e. (~P(s u. {(U.J \ S)}) i^i Fin)U.J = U.u)
38 elin 2786 . . . . . . . . . . . 12 |- ((u \ {(U.J \ S)}) e. (~Ps i^i Fin) <-> ((u \ {(U.J \ S)}) e. ~Ps /\ (u \ {(U.J \ S)}) e. Fin))
39 visset 2295 . . . . . . . . . . . . . . 15 |- u e. _V
40 difss 2735 . . . . . . . . . . . . . . 15 |- (u \ {(U.J \ S)}) C_ u
4139, 40ssexi 3456 . . . . . . . . . . . . . 14 |- (u \ {(U.J \ S)}) e. _V
4241elpw 3037 . . . . . . . . . . . . 13 |- ((u \ {(U.J \ S)}) e. ~Ps <-> (u \ {(U.J \ S)}) C_ s)
4342anbi1i 539 . . . . . . . . . . . 12 |- (((u \ {(U.J \ S)}) e. ~Ps /\ (u \ {(U.J \ S)}) e. Fin) <-> ((u \ {(U.J \ S)}) C_ s /\ (u \ {(U.J \ S)}) e. Fin))
4438, 43bitri 190 . . . . . . . . . . 11 |- ((u \ {(U.J \ S)}) e. (~Ps i^i Fin) <-> ((u \ {(U.J \ S)}) C_ s /\ (u \ {(U.J \ S)}) e. Fin))
45 simp2l 902 . . . . . . . . . . . . 13 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> u C_ (s u. {(U.J \ S)}))
46 uncom 2744 . . . . . . . . . . . . 13 |- (s u. {(U.J \ S)}) = ({(U.J \ S)} u. s)
4745, 46syl6ss 2663 . . . . . . . . . . . 12 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> u C_ ({(U.J \ S)} u. s))
48 ssundif 2955 . . . . . . . . . . . 12 |- (u C_ ({(U.J \ S)} u. s) <-> (u \ {(U.J \ S)}) C_ s)
4947, 48sylib 215 . . . . . . . . . . 11 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> (u \ {(U.J \ S)}) C_ s)
50 ssfi 5630 . . . . . . . . . . . . . 14 |- ((u e. Fin /\ (u \ {(U.J \ S)}) C_ u) -> (u \ {(U.J \ S)}) e. Fin)
5140, 50mpan2 760 . . . . . . . . . . . . 13 |- (u e. Fin -> (u \ {(U.J \ S)}) e. Fin)
5251ad2antll 443 . . . . . . . . . . . 12 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (s u. {(U.J \ S)}) /\ u e. Fin)) -> (u \ {(U.J \ S)}) e. Fin)
53523adant3 896 . . . . . . . . . . 11 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> (u \ {(U.J \ S)}) e. Fin)
5444, 49, 53sylanbrc 527 . . . . . . . . . 10 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> (u \ {(U.J \ S)}) e. (~Ps i^i Fin))
55123ad2ant1 897 . . . . . . . . . . . . . . . . . 18 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> S C_ U.s)
56143ad2ant1 897 . . . . . . . . . . . . . . . . . . 19 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> U.s C_ U.J)
57 simp3 878 . . . . . . . . . . . . . . . . . . 19 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> U.J = U.u)
5856, 57sseqtrd 2653 . . . . . . . . . . . . . . . . . 18 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> U.s C_ U.u)
5955, 58sstrd 2627 . . . . . . . . . . . . . . . . 17 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> S C_ U.u)
6059sseld 2619 . . . . . . . . . . . . . . . 16 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> (v e. S -> v e. U.u))
6160imp 377 . . . . . . . . . . . . . . 15 |- (((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) /\ v e. S) -> v e. U.u)
62 eluni 3180 . . . . . . . . . . . . . . 15 |- (v e. U.u <-> E.w(v e. w /\ w e. u))
6361, 62sylib 215 . . . . . . . . . . . . . 14 |- (((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) /\ v e. S) -> E.w(v e. w /\ w e. u))
64 simpl 346 . . . . . . . . . . . . . . . . 17 |- ((v e. w /\ w e. u) -> v e. w)
6564a1i 8 . . . . . . . . . . . . . . . 16 |- (((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) /\ v e. S) -> ((v e. w /\ w e. u) -> v e. w))
66 simpr 350 . . . . . . . . . . . . . . . . . . 19 |- ((v e. w /\ w e. u) -> w e. u)
6766a1i 8 . . . . . . . . . . . . . . . . . 18 |- (((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) /\ v e. S) -> ((v e. w /\ w e. u) -> w e. u))
68 elndif 2732 . . . . . . . . . . . . . . . . . . . . . . 23 |- (v e. S -> -. v e. (U.J \ S))
6968ad2antlr 441 . . . . . . . . . . . . . . . . . . . . . 22 |- ((((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) /\ v e. S) /\ v e. w) -> -. v e. (U.J \ S))
70 eleq2 1958 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (w = (U.J \ S) -> (v e. w <-> v e. (U.J \ S)))
7170biimpd 170 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (w = (U.J \ S) -> (v e. w -> v e. (U.J \ S)))
7271a1i 8 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (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))))
7372com23 36 . . . . . . . . . . . . . . . . . . . . . . 23 |- (((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (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))))
7473imp 377 . . . . . . . . . . . . . . . . . . . . . 22 |- ((((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (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)))
7569, 74mtod 123 . . . . . . . . . . . . . . . . . . . . 21 |- ((((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) /\ v e. S) /\ v e. w) -> -. w = (U.J \ S))
7675ex 402 . . . . . . . . . . . . . . . . . . . 20 |- (((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) /\ v e. S) -> (v e. w -> -. w = (U.J \ S)))
7776adantrd 427 . . . . . . . . . . . . . . . . . . 19 |- (((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (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)))
78 elsn 3058 . . . . . . . . . . . . . . . . . . . 20 |- (w e. {(U.J \ S)} <-> w = (U.J \ S))
7978notbii 204 . . . . . . . . . . . . . . . . . . 19 |- (-. w e. {(U.J \ S)} <-> -. w = (U.J \ S))
8077, 79syl6ibr 230 . . . . . . . . . . . . . . . . . 18 |- (((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (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)}))
8167, 80jcad 661 . . . . . . . . . . . . . . . . 17 |- (((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (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)})))
82 eldif 2609 . . . . . . . . . . . . . . . . 17 |- (w e. (u \ {(U.J \ S)}) <-> (w e. u /\ -. w e. {(U.J \ S)}))
8381, 82syl6ibr 230 . . . . . . . . . . . . . . . 16 |- (((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (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)})))
8465, 83jcad 661 . . . . . . . . . . . . . . 15 |- (((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (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)}))))
8584eximdv 1669 . . . . . . . . . . . . . 14 |- (((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (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)}))))
8663, 85mpd 29 . . . . . . . . . . . . 13 |- (((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (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)})))
8786ex 402 . . . . . . . . . . . 12 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (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)}))))
88 eluni 3180 . . . . . . . . . . . 12 |- (v e. U.(u \ {(U.J \ S)}) <-> E.w(v e. w /\ w e. (u \ {(U.J \ S)})))
8987, 88syl6ibr 230 . . . . . . . . . . 11 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> (v e. S -> v e. U.(u \ {(U.J \ S)})))
9089ssrdv 2622 . . . . . . . . . 10 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> S C_ U.(u \ {(U.J \ S)}))
91 unieq 3185 . . . . . . . . . . . 12 |- (t = (u \ {(U.J \ S)}) -> U.t = U.(u \ {(U.J \ S)}))
9291sseq2d 2645 . . . . . . . . . . 11 |- (t = (u \ {(U.J \ S)}) -> (S C_ U.t <-> S C_ U.(u \ {(U.J \ S)})))
9392rcla4ev 2381 . . . . . . . . . 10 |- (((u \ {(U.J \ S)}) e. (~Ps i^i Fin) /\ S C_ U.(u \ {(U.J \ S)})) -> E.t e. (~Ps i^i Fin)S C_ U.t)
9454, 90, 93syl11anc 524 . . . . . . . . 9 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ (u C_ (s u. {(U.J \ S)}) /\ u e. Fin) /\ U.J = U.u) -> E.t e. (~Ps i^i Fin)S C_ U.t)
95 elin 2786 . . . . . . . . . 10 |- (u e. (~P(s u. {(U.J \ S)}) i^i Fin) <-> (u e. ~P(s u. {(U.J \ S)}) /\ u e. Fin))
9639elpw 3037 . . . . . . . . . . 11 |- (u e. ~P(s u. {(U.J \ S)}) <-> u C_ (s u. {(U.J \ S)}))
9796anbi1i 539 . . . . . . . . . 10 |- ((u e. ~P(s u. {(U.J \ S)}) /\ u e. Fin) <-> (u C_ (s u. {(U.J \ S)}) /\ u e. Fin))
9895, 97bitri 190 . . . . . . . . 9 |- (u e. (~P(s u. {(U.J \ S)}) i^i Fin) <-> (u C_ (s u. {(U.J \ S)}) /\ u e. Fin))
9994, 98syl3an2b 1134 . . . . . . . 8 |- ((((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) /\ u e. (~P(s u. {(U.J \ S)}) i^i Fin) /\ U.J = U.u) -> E.t e. (~Ps i^i Fin)S C_ U.t)
100993exp 1066 . . . . . . 7 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) -> (u e. (~P(s u. {(U.J \ S)}) i^i Fin) -> (U.J = U.u -> E.t e. (~Ps i^i Fin)S C_ U.t)))
101100r19.23adv 2215 . . . . . 6 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) -> (E.u e. (~P(s u. {(U.J \ S)}) i^i Fin)U.J = U.u -> E.t e. (~Ps i^i Fin)S C_ U.t))
10237, 101mpd 29 . . . . 5 |- (((J e. Comp /\ S e. (Clsd` J)) /\ s C_ J /\ S C_ U.s) -> E.t e. (~Ps i^i Fin)S C_ U.t)
1031023exp 1066 . . . 4 |- ((J e. Comp /\ S e. (Clsd` J)) -> (s C_ J -> (S C_ U.s -> E.t e. (~Ps i^i Fin)S C_ U.t)))
104 visset 2295 . . . . 5 |- s e. _V
105104elpw 3037 . . . 4 |- (s e. ~PJ <-> s C_ J)
106103, 105syl5ib 223 . . 3 |- ((J e. Comp /\ S e. (Clsd` J)) -> (s e. ~PJ -> (S C_ U.s -> E.t e. (~Ps i^i Fin)S C_ U.t)))
107106r19.21aiv 2175 . 2 |- ((J e. Comp /\ S e. (Clsd` J)) -> A.s e. ~P J(S C_ U.s -> E.t e. (~Ps i^i Fin)S C_ U.t))
1083cldss 8947 . . . 4 |- ((J e. Top /\ S e. (Clsd` J)) -> S C_ U.J)
1093compsub 15431 . . . 4 |- ((J e. Top /\ S C_ U.J) -> ((subSp` <.S, J>.) e. Comp <-> A.s e. ~P J(S C_ U.s -> E.t e. (~Ps i^i Fin)S C_ U.t)))
110108, 109syldan 516 . . 3 |- ((J e. Top /\ S e. (Clsd` J)) -> ((subSp` <.S, J>.) e. Comp <-> A.s e. ~P J(S C_ U.s -> E.t e. (~Ps i^i Fin)S C_ U.t)))
111110, 5sylan 497 . 2 |- ((J e. Comp /\ S e. (Clsd` J)) -> ((subSp` <.S, J>.) e. Comp <-> A.s e. ~P J(S C_ U.s -> E.t e. (~Ps i^i Fin)S C_ U.t)))
112107, 111mpbird 213 1 |- ((J e. Comp /\ S e. (Clsd` J)) -> (subSp` <.S, J>.) e. Comp)
Colors of variables: wff set class
Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  A.wral 2105  E.wrex 2106  _Vcvv 2292   \ cdif 2590   u. cun 2591   i^i cin 2592   C_ wss 2593  ~Pcpw 3032  {csn 3044  <.cop 3046  U.cuni 3177  ` cfv 3998  Fincfn 5426  Topctop 8857  Clsdccld 8936  subSpcsubsp 10242  Compccomp 10328
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-3or 859  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-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  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-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-1o 5177  df-er 5318  df-en 5427  df-dom 5428  df-fin 5430  df-top 8861  df-topsp 8862  df-cld 8939  df-subsp 10243  df-comp 10329
Copyright terms: Public domain