Table of ContentsTable of Contents Mathbox for Jeff Hankins < Previous   Next >
Related theorems
Unicode version
Theorem hscptsscld 15434
Description: A compact subspace of a T2 space is closed.
Hypothesis
Ref Expression
hscptsscld.1 |- X = U.J
Assertion
Ref Expression
hscptsscld |- ((J e. Haus /\ S C_ X /\ (subSp` <.S, J>.) e. Comp) -> S e. (Clsd` J))
Proof of Theorem hscptsscld
StepHypRef Expression
1 haustop 9063 . . . 4 |- (J e. Haus -> J e. Top)
2 hscptsscld.1 . . . . 5 |- X = U.J
32iscld 8945 . . . 4 |- (J e. Top -> (S e. (Clsd` J) <-> (S C_ X /\ (X \ S) e. J)))
41, 3syl 12 . . 3 |- (J e. Haus -> (S e. (Clsd` J) <-> (S C_ X /\ (X \ S) e. J)))
543ad2ant1 897 . 2 |- ((J e. Haus /\ S C_ X /\ (subSp` <.S, J>.) e. Comp) -> (S e. (Clsd` J) <-> (S C_ X /\ (X \ S) e. J)))
6 simp2 877 . 2 |- ((J e. Haus /\ S C_ X /\ (subSp` <.S, J>.) e. Comp) -> S C_ X)
72compsub 15431 . . . . . . . 8 |- ((J e. Top /\ S C_ X) -> ((subSp` <.S, J>.) e. Comp <-> A.s e. ~P J(S C_ U.s -> E.c e. (~Ps i^i Fin)S C_ U.c)))
87, 1sylan 497 . . . . . . 7 |- ((J e. Haus /\ S C_ X) -> ((subSp` <.S, J>.) e. Comp <-> A.s e. ~P J(S C_ U.s -> E.c e. (~Ps i^i Fin)S C_ U.c)))
9 simpll 448 . . . . . . . . . . . . . . . . 17 |- (((J e. Haus /\ S C_ X) /\ (x e. (X \ S) /\ y e. S)) -> J e. Haus)
10 eldifi 2730 . . . . . . . . . . . . . . . . . 18 |- (x e. (X \ S) -> x e. X)
1110ad2antrl 442 . . . . . . . . . . . . . . . . 17 |- (((J e. Haus /\ S C_ X) /\ (x e. (X \ S) /\ y e. S)) -> x e. X)
12 ssel2 2616 . . . . . . . . . . . . . . . . . 18 |- ((S C_ X /\ y e. S) -> y e. X)
1312ad2ant2l 444 . . . . . . . . . . . . . . . . 17 |- (((J e. Haus /\ S C_ X) /\ (x e. (X \ S) /\ y e. S)) -> y e. X)
14 eleq1 1957 . . . . . . . . . . . . . . . . . . . . . 22 |- (x = y -> (x e. S <-> y e. S))
1514notbid 673 . . . . . . . . . . . . . . . . . . . . 21 |- (x = y -> (-. x e. S <-> -. y e. S))
16 eldifn 2731 . . . . . . . . . . . . . . . . . . . . 21 |- (x e. (X \ S) -> -. x e. S)
1715, 16syl5cbi 226 . . . . . . . . . . . . . . . . . . . 20 |- (x e. (X \ S) -> (x = y -> -. y e. S))
1817necon2ad 2055 . . . . . . . . . . . . . . . . . . 19 |- (x e. (X \ S) -> (y e. S -> x =/= y))
1918imp 377 . . . . . . . . . . . . . . . . . 18 |- ((x e. (X \ S) /\ y e. S) -> x =/= y)
2019adantl 424 . . . . . . . . . . . . . . . . 17 |- (((J e. Haus /\ S C_ X) /\ (x e. (X \ S) /\ y e. S)) -> x =/= y)
212hausnei 9061 . . . . . . . . . . . . . . . . 17 |- ((J e. Haus /\ (x e. X /\ y e. X /\ x =/= y)) -> E.o e. J E.p e. J (x e. o /\ y e. p /\ (o i^i p) = (/)))
229, 11, 13, 20, 21syl13anc 1102 . . . . . . . . . . . . . . . 16 |- (((J e. Haus /\ S C_ X) /\ (x e. (X \ S) /\ y e. S)) -> E.o e. J E.p e. J (x e. o /\ y e. p /\ (o i^i p) = (/)))
23 simp2 877 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((x e. o /\ y e. p /\ (o i^i p) = (/)) -> y e. p)
2423a1i 8 . . . . . . . . . . . . . . . . . . . . . 22 |- (o e. J -> ((x e. o /\ y e. p /\ (o i^i p) = (/)) -> y e. p))
2524r19.23aiv 2211 . . . . . . . . . . . . . . . . . . . . 21 |- (E.o e. J (x e. o /\ y e. p /\ (o i^i p) = (/)) -> y e. p)
2625a1i 8 . . . . . . . . . . . . . . . . . . . 20 |- ((((J e. Haus /\ S C_ X) /\ (x e. (X \ S) /\ y e. S)) /\ p e. J) -> (E.o e. J (x e. o /\ y e. p /\ (o i^i p) = (/)) -> y e. p))
27 inelcm 2928 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((y e. S /\ y e. p) -> (S i^i p) =/= (/))
2827expcom 403 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (y e. p -> (y e. S -> (S i^i p) =/= (/)))
29283ad2ant2 898 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((x e. o /\ y e. p /\ (o i^i p) = (/)) -> (y e. S -> (S i^i p) =/= (/)))
3029com12 14 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (y e. S -> ((x e. o /\ y e. p /\ (o i^i p) = (/)) -> (S i^i p) =/= (/)))
3130a1d 15 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (y e. S -> (o e. J -> ((x e. o /\ y e. p /\ (o i^i p) = (/)) -> (S i^i p) =/= (/))))
3231r19.23adv 2215 . . . . . . . . . . . . . . . . . . . . . . 23 |- (y e. S -> (E.o e. J (x e. o /\ y e. p /\ (o i^i p) = (/)) -> (S i^i p) =/= (/)))
3332ad2antll 443 . . . . . . . . . . . . . . . . . . . . . 22 |- (((J e. Haus /\ S C_ X) /\ (x e. (X \ S) /\ y e. S)) -> (E.o e. J (x e. o /\ y e. p /\ (o i^i p) = (/)) -> (S i^i p) =/= (/)))
3433adantr 425 . . . . . . . . . . . . . . . . . . . . 21 |- ((((J e. Haus /\ S C_ X) /\ (x e. (X \ S) /\ y e. S)) /\ p e. J) -> (E.o e. J (x e. o /\ y e. p /\ (o i^i p) = (/)) -> (S i^i p) =/= (/)))
35 3simpb 873 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((x e. o /\ y e. p /\ (o i^i p) = (/)) -> (x e. o /\ (o i^i p) = (/)))
3635reximi 2198 . . . . . . . . . . . . . . . . . . . . . 22 |- (E.o e. J (x e. o /\ y e. p /\ (o i^i p) = (/)) -> E.o e. J (x e. o /\ (o i^i p) = (/)))
3736a1i 8 . . . . . . . . . . . . . . . . . . . . 21 |- ((((J e. Haus /\ S C_ X) /\ (x e. (X \ S) /\ y e. S)) /\ p e. J) -> (E.o e. J (x e. o /\ y e. p /\ (o i^i p) = (/)) -> E.o e. J (x e. o /\ (o i^i p) = (/))))
3834, 37jcad 661 . . . . . . . . . . . . . . . . . . . 20 |- ((((J e. Haus /\ S C_ X) /\ (x e. (X \ S) /\ y e. S)) /\ p e. J) -> (E.o e. J (x e. o /\ y e. p /\ (o i^i p) = (/)) -> ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))))
3926, 38jcad 661 . . . . . . . . . . . . . . . . . . 19 |- ((((J e. Haus /\ S C_ X) /\ (x e. (X \ S) /\ y e. S)) /\ p e. J) -> (E.o e. J (x e. o /\ y e. p /\ (o i^i p) = (/)) -> (y e. p /\ ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/))))))
4039ex 402 . . . . . . . . . . . . . . . . . 18 |- (((J e. Haus /\ S C_ X) /\ (x e. (X \ S) /\ y e. S)) -> (p e. J -> (E.o e. J (x e. o /\ y e. p /\ (o i^i p) = (/)) -> (y e. p /\ ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))))))
4140reximdvai 2201 . . . . . . . . . . . . . . . . 17 |- (((J e. Haus /\ S C_ X) /\ (x e. (X \ S) /\ y e. S)) -> (E.p e. J E.o e. J (x e. o /\ y e. p /\ (o i^i p) = (/)) -> E.p e. J (y e. p /\ ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/))))))
42 rexcom 2243 . . . . . . . . . . . . . . . . 17 |- (E.o e. J E.p e. J (x e. o /\ y e. p /\ (o i^i p) = (/)) <-> E.p e. J E.o e. J (x e. o /\ y e. p /\ (o i^i p) = (/)))
4341, 42syl5ib 223 . . . . . . . . . . . . . . . 16 |- (((J e. Haus /\ S C_ X) /\ (x e. (X \ S) /\ y e. S)) -> (E.o e. J E.p e. J (x e. o /\ y e. p /\ (o i^i p) = (/)) -> E.p e. J (y e. p /\ ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/))))))
4422, 43mpd 29 . . . . . . . . . . . . . . 15 |- (((J e. Haus /\ S C_ X) /\ (x e. (X \ S) /\ y e. S)) -> E.p e. J (y e. p /\ ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))))
4544exp32 408 . . . . . . . . . . . . . 14 |- ((J e. Haus /\ S C_ X) -> (x e. (X \ S) -> (y e. S -> E.p e. J (y e. p /\ ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))))))
46453impia 1064 . . . . . . . . . . . . 13 |- ((J e. Haus /\ S C_ X /\ x e. (X \ S)) -> (y e. S -> E.p e. J (y e. p /\ ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/))))))
47 elunirab 3190 . . . . . . . . . . . . 13 |- (y e. U.{p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} <-> E.p e. J (y e. p /\ ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))))
4846, 47syl6ibr 230 . . . . . . . . . . . 12 |- ((J e. Haus /\ S C_ X /\ x e. (X \ S)) -> (y e. S -> y e. U.{p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))}))
4948ssrdv 2622 . . . . . . . . . . 11 |- ((J e. Haus /\ S C_ X /\ x e. (X \ S)) -> S C_ U.{p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))})
50 ssrab2 2692 . . . . . . . . . . . . . 14 |- {p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} C_ J
51 elpw2g 3463 . . . . . . . . . . . . . 14 |- (J e. Haus -> ({p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} e. ~PJ <-> {p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} C_ J))
5250, 51mpbiri 211 . . . . . . . . . . . . 13 |- (J e. Haus -> {p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} e. ~PJ)
53 unieq 3185 . . . . . . . . . . . . . . . 16 |- (s = {p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} -> U.s = U.{p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))})
5453sseq2d 2645 . . . . . . . . . . . . . . 15 |- (s = {p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} -> (S C_ U.s <-> S C_ U.{p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))}))
55 pweq 3036 . . . . . . . . . . . . . . . . 17 |- (s = {p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} -> ~Ps = ~P{p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))})
5655ineq1d 2795 . . . . . . . . . . . . . . . 16 |- (s = {p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} -> (~Ps i^i Fin) = (~P{p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} i^i Fin))
5756rexeqdv 2270 . . . . . . . . . . . . . . 15 |- (s = {p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} -> (E.c e. (~Ps i^i Fin)S C_ U.c <-> E.c e. (~P{p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} i^i Fin)S C_ U.c))
5854, 57imbi12d 688 . . . . . . . . . . . . . 14 |- (s = {p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} -> ((S C_ U.s -> E.c e. (~Ps i^i Fin)S C_ U.c) <-> (S C_ U.{p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} -> E.c e. (~P{p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} i^i Fin)S C_ U.c)))
5958rcla4v 2376 . . . . . . . . . . . . 13 |- ({p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} e. ~PJ -> (A.s e. ~P J(S C_ U.s -> E.c e. (~Ps i^i Fin)S C_ U.c) -> (S C_ U.{p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} -> E.c e. (~P{p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} i^i Fin)S C_ U.c)))
6052, 59syl 12 . . . . . . . . . . . 12 |- (J e. Haus -> (A.s e. ~P J(S C_ U.s -> E.c e. (~Ps i^i Fin)S C_ U.c) -> (S C_ U.{p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} -> E.c e. (~P{p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} i^i Fin)S C_ U.c)))
61603ad2ant1 897 . . . . . . . . . . 11 |- ((J e. Haus /\ S C_ X /\ x e. (X \ S)) -> (A.s e. ~P J(S C_ U.s -> E.c e. (~Ps i^i Fin)S C_ U.c) -> (S C_ U.{p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} -> E.c e. (~P{p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} i^i Fin)S C_ U.c)))
6249, 61mpid 58 . . . . . . . . . 10 |- ((J e. Haus /\ S C_ X /\ x e. (X \ S)) -> (A.s e. ~P J(S C_ U.s -> E.c e. (~Ps i^i Fin)S C_ U.c) -> E.c e. (~P{p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} i^i Fin)S C_ U.c))
63 simplrr 455 . . . . . . . . . . . . . . . . . . . 20 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ c C_ {p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))}) -> c e. Fin)
64 simprrr 459 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ (q e. J /\ ((S i^i q) =/= (/) /\ E.o e. J (x e. o /\ (o i^i q) = (/))))) -> E.o e. J (x e. o /\ (o i^i q) = (/)))
65 ineq2 2790 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (p = q -> (S i^i p) = (S i^i q))
6665neeq1d 2028 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (p = q -> ((S i^i p) =/= (/) <-> (S i^i q) =/= (/)))
67 ineq2 2790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (p = q -> (o i^i p) = (o i^i q))
6867eqeq1d 1892 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (p = q -> ((o i^i p) = (/) <-> (o i^i q) = (/)))
6968anbi2d 678 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (p = q -> ((x e. o /\ (o i^i p) = (/)) <-> (x e. o /\ (o i^i q) = (/))))
7069rexbidv 2124 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (p = q -> (E.o e. J (x e. o /\ (o i^i p) = (/)) <-> E.o e. J (x e. o /\ (o i^i q) = (/))))
7166, 70anbi12d 690 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (p = q -> (((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/))) <-> ((S i^i q) =/= (/) /\ E.o e. J (x e. o /\ (o i^i q) = (/)))))
7271elrab 2414 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (q e. {p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} <-> (q e. J /\ ((S i^i q) =/= (/) /\ E.o e. J (x e. o /\ (o i^i q) = (/)))))
7364, 72sylan2b 501 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ q e. {p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))}) -> E.o e. J (x e. o /\ (o i^i q) = (/)))
74 ssel2 2616 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((c C_ {p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} /\ q e. c) -> q e. {p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))})
7573, 74sylan2 500 . . . . . . . . . . . . . . . . . . . . . 22 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ (c C_ {p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} /\ q e. c)) -> E.o e. J (x e. o /\ (o i^i q) = (/)))
7675expr 418 . . . . . . . . . . . . . . . . . . . . 21 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ c C_ {p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))}) -> (q e. c -> E.o e. J (x e. o /\ (o i^i q) = (/))))
7776r19.21aiv 2175 . . . . . . . . . . . . . . . . . . . 20 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ c C_ {p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))}) -> A.q e. c E.o e. J (x e. o /\ (o i^i q) = (/)))
78 eleq2 1958 . . . . . . . . . . . . . . . . . . . . . 22 |- (o = (f` q) -> (x e. o <-> x e. (f` q)))
79 ineq1 2789 . . . . . . . . . . . . . . . . . . . . . . 23 |- (o = (f` q) -> (o i^i q) = ((f` q) i^i q))
8079eqeq1d 1892 . . . . . . . . . . . . . . . . . . . . . 22 |- (o = (f` q) -> ((o i^i q) = (/) <-> ((f` q) i^i q) = (/)))
8178, 80anbi12d 690 . . . . . . . . . . . . . . . . . . . . 21 |- (o = (f` q) -> ((x e. o /\ (o i^i q) = (/)) <-> (x e. (f` q) /\ ((f` q) i^i q) = (/))))
8281ac6sfi 5509 . . . . . . . . . . . . . . . . . . . 20 |- ((c e. Fin /\ A.q e. c E.o e. J (x e. o /\ (o i^i q) = (/))) -> E.f(f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))))
8363, 77, 82syl11anc 524 . . . . . . . . . . . . . . . . . . 19 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ c C_ {p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))}) -> E.f(f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))))
8483ex 402 . . . . . . . . . . . . . . . . . 18 |- (((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) -> (c C_ {p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} -> E.f(f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/)))))
852topopn 8871 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (J e. Top -> X e. J)
861, 85syl 12 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (J e. Haus -> X e. J)
87863ad2ant1 897 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((J e. Haus /\ S C_ X /\ x e. (X \ S)) -> X e. J)
8887ad2antrr 440 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ c = (/)) -> X e. J)
89103ad2ant3 899 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((J e. Haus /\ S C_ X /\ x e. (X \ S)) -> x e. X)
9089ad2antrr 440 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ c = (/)) -> x e. X)
91 unieq 3185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (c = (/) -> U.c = U.(/))
92 uni0 3205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- U.(/) = (/)
9391, 92syl6eq 1944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (c = (/) -> U.c = (/))
94 sseq2 2639 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (U.c = (/) -> (S C_ U.c <-> S C_ (/)))
9594biimpd 170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (U.c = (/) -> (S C_ U.c -> S C_ (/)))
9693, 95syl 12 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (c = (/) -> (S C_ U.c -> S C_ (/)))
9796impcom 378 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((S C_ U.c /\ c = (/)) -> S C_ (/))
98 ss0 2902 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (S C_ (/) -> S = (/))
99 ssid 2634 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- X C_ X
100 difeq2 2719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (S = (/) -> (X \ S) = (X \ (/)))
101 dif0 2943 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (X \ (/)) = X
102100, 101syl6eq 1944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (S = (/) -> (X \ S) = X)
103102sseq2d 2645 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (S = (/) -> (X C_ (X \ S) <-> X C_ X))
10499, 103mpbiri 211 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (S = (/) -> X C_ (X \ S))
10597, 98, 1043syl 24 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((S C_ U.c /\ c = (/)) -> X C_ (X \ S))
106105adantlr 429 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((S C_ U.c /\ c e. Fin) /\ c = (/)) -> X C_ (X \ S))
107106adantll 428 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ c = (/)) -> X C_ (X \ S))
108 eleq2 1958 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (o = X -> (x e. o <-> x e. X))
109 sseq1 2637 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (o = X -> (o C_ (X \ S) <-> X C_ (X \ S)))
110108, 109anbi12d 690 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (o = X -> ((x e. o /\ o C_ (X \ S)) <-> (x e. X /\ X C_ (X \ S))))
111110rcla4ev 2381 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((X e. J /\ (x e. X /\ X C_ (X \ S))) -> E.o e. J (x e. o /\ o C_ (X \ S)))
11288, 90, 107, 111syl12anc 1098 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ c = (/)) -> E.o e. J (x e. o /\ o C_ (X \ S)))
113112ex 402 . . . . . . . . . . . . . . . . . . . . . 22 |- (((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) -> (c = (/) -> E.o e. J (x e. o /\ o C_ (X \ S))))
114113adantr 425 . . . . . . . . . . . . . . . . . . . . 21 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ (f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/)))) -> (c = (/) -> E.o e. J (x e. o /\ o C_ (X \ S))))
115 eleq1 1957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (s = (f` q) -> (s e. J <-> (f` q) e. J))
116 ffvelrn 4787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((f:c-->J /\ q e. c) -> (f` q) e. J)
117115, 116syl5cbir 228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((f:c-->J /\ q e. c) -> (s = (f` q) -> s e. J))
118117ex 402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (f:c-->J -> (q e. c -> (s = (f` q) -> s e. J)))
119118r19.23adv 2215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (f:c-->J -> (E.q e. c s = (f` q) -> s e. J))
12011919.21aiv 1664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f:c-->J -> A.s(E.q e. c s = (f` q) -> s e. J))
121 abss 2676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ({s | E.q e. c s = (f` q)} C_ J <-> A.s(E.q e. c s = (f` q) -> s e. J))
122120, 121sylibr 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (f:c-->J -> {s | E.q e. c s = (f` q)} C_ J)
123122adantr 425 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) -> {s | E.q e. c s = (f` q)} C_ J)
124123ad2antrl 442 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> {s | E.q e. c s = (f` q)} C_ J)
125 simplrr 455 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> c e. Fin)
126 df-fo 4012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f:c-onto->{s | E.q e. c s = (f` q)} <-> (f Fn c /\ ran f = {s | E.q e. c s = (f` q)}))
127 ffn 4562 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (f:c-->J -> f Fn c)
128127adantr 425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) -> f Fn c)
129128ad2antrl 442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> f Fn c)
130 fvelrnb 4719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (f Fn c -> (y e. ran f <-> E.q e. c (f` q) = y))
131127, 130syl 12 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (f:c-->J -> (y e. ran f <-> E.q e. c (f` q) = y))
132131adantr 425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) -> (y e. ran f <-> E.q e. c (f` q) = y))
133132ad2antrl 442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> (y e. ran f <-> E.q e. c (f` q) = y))
134 eqcom 1886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((f` q) = y <-> y = (f` q))
135134rexbii 2128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (E.q e. c (f` q) = y <-> E.q e. c y = (f` q))
136135a1i 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> (E.q e. c (f` q) = y <-> E.q e. c y = (f` q)))
137 visset 2295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- y e. _V
138 eqeq1 1890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (s = y -> (s = (f` q) <-> y = (f` q)))
139138rexbidv 2124 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (s = y -> (E.q e. c s = (f` q) <-> E.q e. c y = (f` q)))
140137, 139elab 2403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (y e. {s | E.q e. c s = (f` q)} <-> E.q e. c y = (f` q))
141136, 140syl6bbr 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> (E.q e. c (f` q) = y <-> y e. {s | E.q e. c s = (f` q)}))
142133, 141bitrd 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> (y e. ran f <-> y e. {s | E.q e. c s = (f` q)}))
143142eqrdv 1882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> ran f = {s | E.q e. c s = (f` q)})
144126, 129, 143sylanbrc 527 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> f:c-onto->{s | E.q e. c s = (f` q)})
145 fodomfi 5656 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((c e. Fin /\ f:c-onto->{s | E.q e. c s = (f` q)}) -> {s | E.q e. c s = (f` q)} ~<_ c)
146125, 144, 145syl11anc 524 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> {s | E.q e. c s = (f` q)} ~<_ c)
147 domfi 5631 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((c e. Fin /\ {s | E.q e. c s = (f` q)} ~<_ c) -> {s | E.q e. c s = (f` q)} e. Fin)
148125, 146, 147syl11anc 524 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> {s | E.q e. c s = (f` q)} e. Fin)
149 eqidd 1885 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> |^|{s | E.q e. c s = (f` q)} = |^|{s | E.q e. c s = (f` q)})
150 visset 2295 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- c e. _V
151150abrexex 4836 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- {s | E.q e. c s = (f` q)} e. _V
152 sseq1 2637 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (z = {s | E.q e. c s = (f` q)} -> (z C_ J <-> {s | E.q e. c s = (f` q)} C_ J))
153 eleq1 1957 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (z = {s | E.q e. c s = (f` q)} -> (z e. Fin <-> {s | E.q e. c s = (f` q)} e. Fin))
154 inteq 3217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (z = {s | E.q e. c s = (f` q)} -> |^|z = |^|{s | E.q e. c s = (f` q)})
155154eqeq2d 1895 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (z = {s | E.q e. c s = (f` q)} -> (|^|{s | E.q e. c s = (f` q)} = |^|z <-> |^|{s | E.q e. c s = (f` q)} = |^|{s | E.q e. c s = (f` q)}))
156152, 153, 1553anbi123d 1168 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (z = {s | E.q e. c s = (f` q)} -> ((z C_ J /\ z e. Fin /\ |^|{s | E.q e. c s = (f` q)} = |^|z) <-> ({s | E.q e. c s = (f` q)} C_ J /\ {s | E.q e. c s = (f` q)} e. Fin /\ |^|{s | E.q e. c s = (f` q)} = |^|{s | E.q e. c s = (f` q)})))
157151, 156cla4ev 2371 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (({s | E.q e. c s = (f` q)} C_ J /\ {s | E.q e. c s = (f` q)} e. Fin /\ |^|{s | E.q e. c s = (f` q)} = |^|{s | E.q e. c s = (f` q)}) -> E.z(z C_ J /\ z e. Fin /\ |^|{s | E.q e. c s = (f` q)} = |^|z))
158124, 148, 149, 157syl111anc 1100 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> E.z(z C_ J /\ z e. Fin /\ |^|{s | E.q e. c s = (f` q)} = |^|z))
159 n0 2884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (c =/= (/) <-> E.p p e. c)
160 eqid 1884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (f` p) = (f` p)
161 fveq2 4681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (q = p -> (f` q) = (f` p))
162161eqeq2d 1895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (q = p -> ((f` p) = (f` q) <-> (f` p) = (f` p)))
163162rcla4ev 2381 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((p e. c /\ (f` p) = (f` p)) -> E.q e. c (f` p) = (f` q))
164160, 163mpan2 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (p e. c -> E.q e. c (f` p) = (f` q))
165 fvex 4689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (f` p) e. _V
166 eqeq1 1890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (s = (f` p) -> (s = (f` q) <-> (f` p) = (f` q)))
167166rexbidv 2124 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (s = (f` p) -> (E.q e. c s = (f` q) <-> E.q e. c (f` p) = (f` q)))
168165, 167elab 2403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((f` p) e. {s | E.q e. c s = (f` q)} <-> E.q e. c (f` p) = (f` q))
169164, 168sylibr 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (p e. c -> (f` p) e. {s | E.q e. c s = (f` q)})
170 ne0i 2881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((f` p) e. {s | E.q e. c s = (f` q)} -> {s | E.q e. c s = (f` q)} =/= (/))
171169, 170syl 12 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (p e. c -> {s | E.q e. c s = (f` q)} =/= (/))
17217119.23aiv 1674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (E.p p e. c -> {s | E.q e. c s = (f` q)} =/= (/))
173159, 172sylbi 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (c =/= (/) -> {s | E.q e. c s = (f` q)} =/= (/))
174173adantl 424 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ c =/= (/)) -> {s | E.q e. c s = (f` q)} =/= (/))
175 intex 3465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ({s | E.q e. c s = (f` q)} =/= (/) <-> |^|{s | E.q e. c s = (f` q)} e. _V)
176174, 175sylib 215 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ c =/= (/)) -> |^|{s | E.q e. c s = (f` q)} e. _V)
177 simpl1 879 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ c =/= (/)) -> J e. Haus)
178 sppfi 10218 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((|^|{s | E.q e. c s = (f` q)} e. _V /\ J e. Haus) -> (|^|{s | E.q e. c s = (f` q)} e. ( fi ` J) <-> E.z(z C_ J /\ z e. Fin /\ |^|{s | E.q e. c s = (f` q)} = |^|z)))
179176, 177, 178syl11anc 524 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ c =/= (/)) -> (|^|{s | E.q e. c s = (f` q)} e. ( fi ` J) <-> E.z(z C_ J /\ z e. Fin /\ |^|{s | E.q e. c s = (f` q)} = |^|z)))
180179ad2ant2rl 447 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> (|^|{s | E.q e. c s = (f` q)} e. ( fi ` J) <-> E.z(z C_ J /\ z e. Fin /\ |^|{s | E.q e. c s = (f` q)} = |^|z)))
181158, 180mpbird 213 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> |^|{s | E.q e. c s = (f` q)} e. ( fi ` J))
182 fitop 15401 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (J e. Top -> ( fi ` J) = J)
1831, 182syl 12 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (J e. Haus -> ( fi ` J) = J)
1841833ad2ant1 897 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((J e. Haus /\ S C_ X /\ x e. (X \ S)) -> ( fi ` J) = J)
185184ad2antrr 440 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> ( fi ` J) = J)
186181, 185eleqtrd 1973 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> |^|{s | E.q e. c s = (f` q)} e. J)
187 hbra1 2147 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/)) -> A.qA.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/)))
188 ax-17 1317 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x e. s -> A.q x e. s)
189 ra4 2155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/)) -> (q e. c -> (x e. (f` q) /\ ((f` q) i^i q) = (/))))
190 eleq2 1958 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (s = (f` q) -> (x e. s <-> x e. (f` q)))
191190biimprcd 173 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (x e. (f` q) -> (s = (f` q) -> x e. s))
192191adantr 425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((x e. (f` q) /\ ((f` q) i^i q) = (/)) -> (s = (f` q) -> x e. s))
193189, 192syl6 25 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/)) -> (q e. c -> (s = (f` q) -> x e. s)))
194187, 188, 193r19.23ad 2213 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/)) -> (E.q e. c s = (f` q) -> x e. s))
195194adantl 424 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) -> (E.q e. c s = (f` q) -> x e. s))
196195ad2antrl 442 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> (E.q e. c s = (f` q) -> x e. s))
19719619.21aiv 1664 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> A.s(E.q e. c s = (f` q) -> x e. s))
198 visset 2295 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- x e. _V
199198elintab 3227 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (x e. |^|{s | E.q e. c s = (f` q)} <-> A.s(E.q e. c s = (f` q) -> x e. s))
200197, 199sylibr 217 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> x e. |^|{s | E.q e. c s = (f` q)})
201 pm2.27 76 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (E.q e. c (f` p) = (f` q) -> ((E.q e. c (f` p) = (f` q) -> y e. (f` p)) -> y e. (f` p)))
202164, 201syl 12 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (p e. c -> ((E.q e. c (f` p) = (f` q) -> y e. (f` p)) -> y e. (f` p)))
203202ad2antll 443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ p e. c)) -> ((E.q e. c (f` p) = (f` q) -> y e. (f` p)) -> y e. (f` p)))
204 eleq2 1958 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (s = (f` p) -> (y e. s <-> y e. (f` p)))
205167, 204imbi12d 688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (s = (f` p) -> ((E.q e. c s = (f` q) -> y e. s) <-> (E.q e. c (f` p) = (f` q) -> y e. (f` p))))
206165, 205cla4v 2370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (A.s(E.q e. c s = (f` q) -> y e. s) -> (E.q e. c (f` p) = (f` q) -> y e. (f` p)))
207203, 206syl5 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ p e. c)) -> (A.s(E.q e. c s = (f` q) -> y e. s) -> y e. (f` p)))
208 ffvelrn 4787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((f:c-->J /\ p e. c) -> (f` p) e. J)
209 elunii 3182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((y e. (f` p) /\ (f` p) e. J) -> y e. U.J)
210209, 2syl6eleqr 1982 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((y e. (f` p) /\ (f` p) e. J) -> y e. X)
211210expcom 403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((f` p) e. J -> (y e. (f` p) -> y e. X))
212208, 211syl 12 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((f:c-->J /\ p e. c) -> (y e. (f` p) -> y e. X))
213212adantlr 429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ p e. c) -> (y e. (f` p) -> y e. X))
214213adantl 424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ p e. c)) -> (y e. (f` p) -> y e. X))
215207, 214syld 30 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ p e. c)) -> (A.s(E.q e. c s = (f` q) -> y e. s) -> y e. X))
216215expr 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ (f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/)))) -> (p e. c -> (A.s(E.q e. c s = (f` q) -> y e. s) -> y e. X)))
21721619.23adv 1584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ (f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/)))) -> (E.p p e. c -> (A.s(E.q e. c s = (f` q) -> y e. s) -> y e. X)))
218217, 159syl5ib 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ (f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/)))) -> (c =/= (/) -> (A.s(E.q e. c s = (f` q) -> y e. s) -> y e. X)))
219218impr 422 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> (A.s(E.q e. c s = (f` q) -> y e. s) -> y e. X))
220137elintab 3227 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (y e. |^|{s | E.q e. c s = (f` q)} <-> A.s(E.q e. c s = (f` q) -> y e. s))
221219, 220syl5ib 223 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> (y e. |^|{s | E.q e. c s = (f` q)} -> y e. X))
222 ssel 2615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (S C_ U.c -> (y e. S -> y e. U.c))
223 eluni 3180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (y e. U.c <-> E.p(y e. p /\ p e. c))
224164adantl 424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((y e. p /\ p e. c) -> E.q e. c (f` p) = (f` q))
225224ad2antrr 440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((((y e. p /\ p e. c) /\ c e. Fin) /\ (((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/)) /\ (J e. Haus /\ S C_ X /\ x e. (X \ S)))) -> E.q e. c (f` p) = (f` q))
226161eleq2d 1964 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (q = p -> (x e. (f` q) <-> x e. (f` p)))
227 id 73 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (q = p -> q = p)
228161, 227ineq12d 2797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (q = p -> ((f` q) i^i q) = ((f` p) i^i p))
229228eqeq1d 1892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (q = p -> (((f` q) i^i q) = (/) <-> ((f` p) i^i p) = (/)))
230226, 229anbi12d 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (q = p -> ((x e. (f` q) /\ ((f` q) i^i q) = (/)) <-> (x e. (f` p) /\ ((f` p) i^i p) = (/))))
231230rcla4v 2376 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (p e. c -> (A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/)) -> (x e. (f` p) /\ ((f` p) i^i p) = (/))))
232 elin 2786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (y e. ((f` p) i^i p) <-> (y e. (f` p) /\ y e. p))
233 n0i 2880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (y e. ((f` p) i^i p) -> -. ((f` p) i^i p) = (/))
234232, 233sylbir 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ((y e. (f` p) /\ y e. p) -> -. ((f` p) i^i p) = (/))
235234expcom 403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (y e. p -> (y e. (f` p) -> -. ((f` p) i^i p) = (/)))
236235con2d 107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (y e. p -> (((f` p) i^i p) = (/) -> -. y e. (f` p)))
237236adantld 426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (y e. p -> ((x e. (f` p) /\ ((f` p) i^i p) = (/)) -> -. y e. (f` p)))
238231, 237syl9r 72 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (y e. p -> (p e. c -> (A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/)) -> -. y e. (f` p))))
239238imp31 389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (((y e. p /\ p e. c) /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) -> -. y e. (f` p))
240239adantrl 430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (((y e. p /\ p e. c) /\ (f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/)))) -> -. y e. (f` p))
241240adantrr 431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (((y e. p /\ p e. c) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> -. y e. (f` p))
242241ad2ant2r 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((((y e. p /\ p e. c) /\ c e. Fin) /\ (((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/)) /\ (J e. Haus /\ S C_ X /\ x e. (X \ S)))) -> -. y e. (f` p))
243204notbid 673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (s = (f` p) -> (-. y e. s <-> -. y e. (f` p)))
244167, 243anbi12d 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (s = (f` p) -> ((E.q e. c s = (f` q) /\ -. y e. s) <-> (E.q e. c (f` p) = (f` q) /\ -. y e. (f` p))))
245165, 244cla4ev 2371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((E.q e. c (f` p) = (f` q) /\ -. y e. (f` p)) -> E.s(E.q e. c s = (f` q) /\ -. y e. s))
246225, 242, 245syl11anc 524 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((((y e. p /\ p e. c) /\ c e. Fin) /\ (((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/)) /\ (J e. Haus /\ S C_ X /\ x e. (X \ S)))) -> E.s(E.q e. c s = (f` q) /\ -. y e. s))
247246exp43 415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((y e. p /\ p e. c) -> (c e. Fin -> (((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/)) -> ((J e. Haus /\ S C_ X /\ x e. (X \ S)) -> E.s(E.q e. c s = (f` q) /\ -. y e. s)))))
24824719.23aiv 1674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (E.p(y e. p /\ p e. c) -> (c e. Fin -> (((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/)) -> ((J e. Haus /\ S C_ X /\ x e. (X \ S)) -> E.s(E.q e. c s = (f` q) /\ -. y e. s)))))
249223, 248sylbi 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (y e. U.c -> (c e. Fin -> (((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/)) -> ((J e. Haus /\ S C_ X /\ x e. (X \ S)) -> E.s(E.q e. c s = (f` q) /\ -. y e. s)))))
250222, 249syl6com 64 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (y e. S -> (S C_ U.c -> (c e. Fin -> (((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/)) -> ((J e. Haus /\ S C_ X /\ x e. (X \ S)) -> E.s(E.q e. c s = (f` q) /\ -. y e. s))))))
251250imp3a 388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (y e. S -> ((S C_ U.c /\ c e. Fin) -> (((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/)) -> ((J e. Haus /\ S C_ X /\ x e. (X \ S)) -> E.s(E.q e. c s = (f` q) /\ -. y e. s)))))
252251com14 42 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((J e. Haus /\ S C_ X /\ x e. (X \ S)) -> ((S C_ U.c /\ c e. Fin) -> (((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/)) -> (y e. S -> E.s(E.q e. c s = (f` q) /\ -. y e. s)))))
253252imp31 389 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> (y e. S -> E.s(E.q e. c s = (f` q) /\ -. y e. s)))
254 exanali 1390 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (E.s(E.q e. c s = (f` q) /\ -. y e. s) <-> -. A.s(E.q e. c s = (f` q) -> y e. s))
255220notbii 204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (-. y e. |^|{s | E.q e. c s = (f` q)} <-> -. A.s(E.q e. c s = (f` q) -> y e. s))
256254, 255bitr4i 193 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (E.s(E.q e. c s = (f` q) /\ -. y e. s) <-> -. y e. |^|{s | E.q e. c s = (f` q)})
257253, 256syl6ib 229 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> (y e. S -> -. y e. |^|{s | E.q e. c s = (f` q)}))
258257con2d 107 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> (y e. |^|{s | E.q e. c s = (f` q)} -> -. y e. S))
259221, 258jcad 661 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> (y e. |^|{s | E.q e. c s = (f` q)} -> (y e. X /\ -. y e. S)))
260 eldif 2609 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (y e. (X \ S) <-> (y e. X /\ -. y e. S))
261259, 260syl6ibr 230 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> (y e. |^|{s | E.q e. c s = (f` q)} -> y e. (X \ S)))
262261ssrdv 2622 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> |^|{s | E.q e. c s = (f` q)} C_ (X \ S))
263 eleq2 1958 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (o = |^|{s | E.q e. c s = (f` q)} -> (x e. o <-> x e. |^|{s | E.q e. c s = (f` q)}))
264 sseq1 2637 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (o = |^|{s | E.q e. c s = (f` q)} -> (o C_ (X \ S) <-> |^|{s | E.q e. c s = (f` q)} C_ (X \ S)))
265263, 264anbi12d 690 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (o = |^|{s | E.q e. c s = (f` q)} -> ((x e. o /\ o C_ (X \ S)) <-> (x e. |^|{s | E.q e. c s = (f` q)} /\ |^|{s | E.q e. c s = (f` q)} C_ (X \ S))))
266265rcla4ev 2381 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((|^|{s | E.q e. c s = (f` q)} e. J /\ (x e. |^|{s | E.q e. c s = (f` q)} /\ |^|{s | E.q e. c s = (f` q)} C_ (X \ S))) -> E.o e. J (x e. o /\ o C_ (X \ S)))
267186, 200, 262, 266syl12anc 1098 . . . . . . . . . . . . . . . . . . . . . 22 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) /\ c =/= (/))) -> E.o e. J (x e. o /\ o C_ (X \ S)))
268267expr 418 . . . . . . . . . . . . . . . . . . . . 21 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ (f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/)))) -> (c =/= (/) -> E.o e. J (x e. o /\ o C_ (X \ S))))
269114, 268pm2.61dne 2091 . . . . . . . . . . . . . . . . . . . 20 |- ((((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) /\ (f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/)))) -> E.o e. J (x e. o /\ o C_ (X \ S)))
270269ex 402 . . . . . . . . . . . . . . . . . . 19 |- (((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) -> ((f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) -> E.o e. J (x e. o /\ o C_ (X \ S))))
27127019.23adv 1584 . . . . . . . . . . . . . . . . . 18 |- (((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) -> (E.f(f:c-->J /\ A.q e. c (x e. (f` q) /\ ((f` q) i^i q) = (/))) -> E.o e. J (x e. o /\ o C_ (X \ S))))
27284, 271syld 30 . . . . . . . . . . . . . . . . 17 |- (((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ (S C_ U.c /\ c e. Fin)) -> (c C_ {p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} -> E.o e. J (x e. o /\ o C_ (X \ S))))
273272expr 418 . . . . . . . . . . . . . . . 16 |- (((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ S C_ U.c) -> (c e. Fin -> (c C_ {p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} -> E.o e. J (x e. o /\ o C_ (X \ S)))))
274273com23 36 . . . . . . . . . . . . . . 15 |- (((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ S C_ U.c) -> (c C_ {p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} -> (c e. Fin -> E.o e. J (x e. o /\ o C_ (X \ S)))))
275274imp3a 388 . . . . . . . . . . . . . 14 |- (((J e. Haus /\ S C_ X /\ x e. (X \ S)) /\ S C_ U.c) -> ((c C_ {p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} /\ c e. Fin) -> E.o e. J (x e. o /\ o C_ (X \ S))))
276275ex 402 . . . . . . . . . . . . 13 |- ((J e. Haus /\ S C_ X /\ x e. (X \ S)) -> (S C_ U.c -> ((c C_ {p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} /\ c e. Fin) -> E.o e. J (x e. o /\ o C_ (X \ S)))))
277276com23 36 . . . . . . . . . . . 12 |- ((J e. Haus /\ S C_ X /\ x e. (X \ S)) -> ((c C_ {p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} /\ c e. Fin) -> (S C_ U.c -> E.o e. J (x e. o /\ o C_ (X \ S)))))
278 elin 2786 . . . . . . . . . . . . 13 |- (c e. (~P{p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} i^i Fin) <-> (c e. ~P{p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} /\ c e. Fin))
279150elpw 3037 . . . . . . . . . . . . . 14 |- (c e. ~P{p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} <-> c C_ {p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))})
280279anbi1i 539 . . . . . . . . . . . . 13 |- ((c e. ~P{p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} /\ c e. Fin) <-> (c C_ {p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} /\ c e. Fin))
281278, 280bitri 190 . . . . . . . . . . . 12 |- (c e. (~P{p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} i^i Fin) <-> (c C_ {p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} /\ c e. Fin))
282277, 281syl5ib 223 . . . . . . . . . . 11 |- ((J e. Haus /\ S C_ X /\ x e. (X \ S)) -> (c e. (~P{p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} i^i Fin) -> (S C_ U.c -> E.o e. J (x e. o /\ o C_ (X \ S)))))
283282r19.23adv 2215 . . . . . . . . . 10 |- ((J e. Haus /\ S C_ X /\ x e. (X \ S)) -> (E.c e. (~P{p e. J | ((S i^i p) =/= (/) /\ E.o e. J (x e. o /\ (o i^i p) = (/)))} i^i Fin)S C_ U.c -> E.o e. J (x e. o /\ o C_ (X \ S))))
28462, 283syld 30 . . . . . . . . 9 |- ((J e. Haus /\ S C_ X /\ x e. (X \ S)) -> (A.s e. ~P J(S C_ U.s -> E.c e. (~Ps i^i Fin)S C_ U.c) -> E.o e. J (x e. o /\ o C_ (X \ S))))
2852843expia 1069 . . . . . . . 8 |- ((J e. Haus /\ S C_ X) -> (x e. (X \ S) -> (A.s e. ~P J(S C_ U.s -> E.c e. (~Ps i^i Fin)S C_ U.c) -> E.o e. J (x e. o /\ o C_ (X \ S)))))
286285com23 36 . . . . . . 7 |- ((J e. Haus /\ S C_ X) -> (A.s e. ~P J(S C_ U.s -> E.c e. (~Ps i^i Fin)S C_ U.c) -> (x e. (X \ S) -> E.o e. J (x e. o /\ o C_ (X \ S)))))
2878, 286sylbid 220 . . . . . 6 |- ((J e. Haus /\ S C_ X) -> ((subSp` <.S, J>.) e. Comp -> (x e. (X \ S) -> E.o e. J (x e. o /\ o C_ (X \ S)))))
2882873impia 1064 . . . . 5 |- ((J e. Haus /\ S C_ X /\ (subSp` <.S, J>.) e. Comp) -> (x e. (X \ S) -> E.o e. J (x e. o /\ o C_ (X \ S))))
289288r19.21aiv 2175 . . . 4 |- ((J e. Haus /\ S C_ X /\ (subSp` <.S, J>.) e. Comp) -> A.x e. (X \ S)E.o e. J (x e. o /\ o C_ (X \ S)))
290 difss 2735 . . . . 5 |- (X \ S) C_ X
291290, 2sseqtri 2649 . . . 4 |- (X \ S) C_ U.J
292289, 291jctil 316 . . 3 |- ((J e. Haus /\ S C_ X /\ (subSp` <.S, J>.) e. Comp) -> ((X \ S) C_ U.J /\ A.x e. (X \ S)E.o e. J (x e. o /\ o C_ (X \ S))))
293 eltop2 8900 . . . . 5 |- (J e. Top -> ((X \ S) e. J <-> ((X \ S) C_ U.J /\ A.x e. (X \ S)E.o e. J (x e. o /\ o C_ (X \ S)))))
2941, 293syl 12 . . . 4 |- (J e. Haus -> ((X \ S) e. J <-> ((X \ S) C_ U.J /\ A.x e. (X \ S)E.o e. J (x e. o /\ o C_ (X \ S)))))
2952943ad2ant1 897 . . 3 |- ((J e. Haus /\ S C_ X /\ (subSp` <.S, J>.) e. Comp) -> ((X \ S) e. J <-> ((X \ S) C_ U.J /\ A.x e. (X \ S)E.o e. J (x e. o /\ o C_ (X \ S)))))
296292, 295mpbird 213 . 2 |- ((J e. Haus /\ S C_ X /\ (subSp` <.S, J>.) e. Comp) -> (X \ S) e. J)
2975, 6, 296mpbir2and 802 1 |- ((J e. Haus /\ S C_ X /\ (subSp` <.S, J>.) e. Comp) -> S e. (Clsd` J))
Colors of variables: wff set class
Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  {cab 1871   =/= wne 2017  A.wral 2105  E.wrex 2106  {crab 2108  _Vcvv 2292   \ cdif 2590   i^i cin 2592   C_ wss 2593  (/)c0 2875  ~Pcpw 3032  <.cop 3046  U.cuni 3177  |^|cint 3214   class class class wbr 3338  ran crn 3987   Fn wfn 3993  -->wf 3994  -onto->wfo 3996  ` cfv 3998   ~<_ cdom 5424  Fincfn 5426  Topctop 8857  Clsdccld 8936  Hauscha 9058   fi cfi 10210  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-reu 2111  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-int 3215  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-rdg 5140  df-1o 5177  df-oadd 5179  df-er 5318  df-en 5427  df-dom 5428  df-fin 5430  df-top 8861  df-topsp 8862  df-bases 8863  df-topgen 8864  df-cld 8939  df-haus 9059  df-fi 10211  df-subsp 10243  df-comp 10329
Copyright terms: Public domain