perfopn

Description: An open subset of a perfect space is perfect. (Contributed by Mario Carneiro, 25-Dec-2016)

	Ref	Expression
Hypotheses	restcls.1	$⊢ X = ⋃ J$
	restcls.2	$⊢ K = J ↾_{𝑡} Y$
Assertion	perfopn	$⊢ (J \in Perf \land Y \in J) \to K \in Perf$

Proof

Step	Hyp	Ref	Expression
1		restcls.1	$⊢ X = ⋃ J$
2		restcls.2	$⊢ K = J ↾_{𝑡} Y$
3		perftop	$⊢ J \in Perf \to J \in Top$
4	3	adantr	$⊢ (J \in Perf \land Y \in J) \to J \in Top$
5	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
6	4 5	sylib	$⊢ (J \in Perf \land Y \in J) \to J \in TopOn (X)$
7		elssuni	$⊢ Y \in J \to Y \subseteq ⋃ J$
8	7	adantl	$⊢ (J \in Perf \land Y \in J) \to Y \subseteq ⋃ J$
9	8 1	sseqtrrdi	$⊢ (J \in Perf \land Y \in J) \to Y \subseteq X$
10		resttopon	$⊢ (J \in TopOn (X) \land Y \subseteq X) \to J ↾_{𝑡} Y \in TopOn (Y)$
11	6 9 10	syl2anc	$⊢ (J \in Perf \land Y \in J) \to J ↾_{𝑡} Y \in TopOn (Y)$
12	2 11	eqeltrid	$⊢ (J \in Perf \land Y \in J) \to K \in TopOn (Y)$
13		topontop	$⊢ K \in TopOn (Y) \to K \in Top$
14	12 13	syl	$⊢ (J \in Perf \land Y \in J) \to K \in Top$
15	9	sselda	$⊢ ((J \in Perf \land Y \in J) \land x \in Y) \to x \in X$
16	1	perfi	$⊢ (J \in Perf \land x \in X) \to \neg \{x\} \in J$
17	16	adantlr	$⊢ ((J \in Perf \land Y \in J) \land x \in X) \to \neg \{x\} \in J$
18	15 17	syldan	$⊢ ((J \in Perf \land Y \in J) \land x \in Y) \to \neg \{x\} \in J$
19	2	eleq2i	$⊢ \{x\} \in K \leftrightarrow \{x\} \in (J ↾_{𝑡} Y)$
20		restopn2	$⊢ (J \in Top \land Y \in J) \to (\{x\} \in (J ↾_{𝑡} Y) \leftrightarrow (\{x\} \in J \land \{x\} \subseteq Y))$
21	3 20	sylan	$⊢ (J \in Perf \land Y \in J) \to (\{x\} \in (J ↾_{𝑡} Y) \leftrightarrow (\{x\} \in J \land \{x\} \subseteq Y))$
22	21	adantr	$⊢ ((J \in Perf \land Y \in J) \land x \in Y) \to (\{x\} \in (J ↾_{𝑡} Y) \leftrightarrow (\{x\} \in J \land \{x\} \subseteq Y))$
23		simpl	$⊢ (\{x\} \in J \land \{x\} \subseteq Y) \to \{x\} \in J$
24	22 23	syl6bi	$⊢ ((J \in Perf \land Y \in J) \land x \in Y) \to (\{x\} \in (J ↾_{𝑡} Y) \to \{x\} \in J)$
25	19 24	biimtrid	$⊢ ((J \in Perf \land Y \in J) \land x \in Y) \to (\{x\} \in K \to \{x\} \in J)$
26	18 25	mtod	$⊢ ((J \in Perf \land Y \in J) \land x \in Y) \to \neg \{x\} \in K$
27	26	ralrimiva	$⊢ (J \in Perf \land Y \in J) \to \forall x \in Y \neg \{x\} \in K$
28		toponuni	$⊢ K \in TopOn (Y) \to Y = ⋃ K$
29	12 28	syl	$⊢ (J \in Perf \land Y \in J) \to Y = ⋃ K$
30	29	raleqdv	$⊢ (J \in Perf \land Y \in J) \to (\forall x \in Y \neg \{x\} \in K \leftrightarrow \forall x \in ⋃ K \neg \{x\} \in K)$
31	27 30	mpbid	$⊢ (J \in Perf \land Y \in J) \to \forall x \in ⋃ K \neg \{x\} \in K$
32		eqid	$⊢ ⋃ K = ⋃ K$
33	32	isperf3	$⊢ K \in Perf \leftrightarrow (K \in Top \land \forall x \in ⋃ K \neg \{x\} \in K)$
34	14 31 33	sylanbrc	$⊢ (J \in Perf \land Y \in J) \to K \in Perf$

Metamath Proof Explorer

Theorem perfopn

Proof