Theorem perfopn

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

	Ref	Expression
Hypotheses	restcls.1	⊢ 𝑋 = ∪ 𝐽
	restcls.2	⊢ 𝐾 = ( 𝐽 ↾t 𝑌 )
Assertion	perfopn	⊢ ( ( 𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽 ) → 𝐾 ∈ Perf )

Proof

Step	Hyp	Ref	Expression
1		restcls.1	⊢ 𝑋 = ∪ 𝐽
2		restcls.2	⊢ 𝐾 = ( 𝐽 ↾t 𝑌 )
3		perftop	⊢ ( 𝐽 ∈ Perf → 𝐽 ∈ Top )
4	3	adantr	⊢ ( ( 𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽 ) → 𝐽 ∈ Top )
5	1	toptopon	⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
6	4 5	sylib	⊢ ( ( 𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
7		elssuni	⊢ ( 𝑌 ∈ 𝐽 → 𝑌 ⊆ ∪ 𝐽 )
8	7	adantl	⊢ ( ( 𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽 ) → 𝑌 ⊆ ∪ 𝐽 )
9	8 1	sseqtrrdi	⊢ ( ( 𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽 ) → 𝑌 ⊆ 𝑋 )
10		resttopon	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝑌 ) ∈ ( TopOn ‘ 𝑌 ) )
11	6 9 10	syl2anc	⊢ ( ( 𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽 ) → ( 𝐽 ↾t 𝑌 ) ∈ ( TopOn ‘ 𝑌 ) )
12	2 11	eqeltrid	⊢ ( ( 𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
13		topontop	⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝐾 ∈ Top )
14	12 13	syl	⊢ ( ( 𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽 ) → 𝐾 ∈ Top )
15	9	sselda	⊢ ( ( ( 𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ∈ 𝑋 )
16	1	perfi	⊢ ( ( 𝐽 ∈ Perf ∧ 𝑥 ∈ 𝑋 ) → ¬ { 𝑥 } ∈ 𝐽 )
17	16	adantlr	⊢ ( ( ( 𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑋 ) → ¬ { 𝑥 } ∈ 𝐽 )
18	15 17	syldan	⊢ ( ( ( 𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑌 ) → ¬ { 𝑥 } ∈ 𝐽 )
19	2	eleq2i	⊢ ( { 𝑥 } ∈ 𝐾 ↔ { 𝑥 } ∈ ( 𝐽 ↾t 𝑌 ) )
20		restopn2	⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ∈ 𝐽 ) → ( { 𝑥 } ∈ ( 𝐽 ↾t 𝑌 ) ↔ ( { 𝑥 } ∈ 𝐽 ∧ { 𝑥 } ⊆ 𝑌 ) ) )
21	3 20	sylan	⊢ ( ( 𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽 ) → ( { 𝑥 } ∈ ( 𝐽 ↾t 𝑌 ) ↔ ( { 𝑥 } ∈ 𝐽 ∧ { 𝑥 } ⊆ 𝑌 ) ) )
22	21	adantr	⊢ ( ( ( 𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑌 ) → ( { 𝑥 } ∈ ( 𝐽 ↾t 𝑌 ) ↔ ( { 𝑥 } ∈ 𝐽 ∧ { 𝑥 } ⊆ 𝑌 ) ) )
23		simpl	⊢ ( ( { 𝑥 } ∈ 𝐽 ∧ { 𝑥 } ⊆ 𝑌 ) → { 𝑥 } ∈ 𝐽 )
24	22 23	syl6bi	⊢ ( ( ( 𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑌 ) → ( { 𝑥 } ∈ ( 𝐽 ↾t 𝑌 ) → { 𝑥 } ∈ 𝐽 ) )
25	19 24	syl5bi	⊢ ( ( ( 𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑌 ) → ( { 𝑥 } ∈ 𝐾 → { 𝑥 } ∈ 𝐽 ) )
26	18 25	mtod	⊢ ( ( ( 𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑌 ) → ¬ { 𝑥 } ∈ 𝐾 )
27	26	ralrimiva	⊢ ( ( 𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽 ) → ∀ 𝑥 ∈ 𝑌 ¬ { 𝑥 } ∈ 𝐾 )
28		toponuni	⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 = ∪ 𝐾 )
29	12 28	syl	⊢ ( ( 𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽 ) → 𝑌 = ∪ 𝐾 )
30	29	raleqdv	⊢ ( ( 𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽 ) → ( ∀ 𝑥 ∈ 𝑌 ¬ { 𝑥 } ∈ 𝐾 ↔ ∀ 𝑥 ∈ ∪ 𝐾 ¬ { 𝑥 } ∈ 𝐾 ) )
31	27 30	mpbid	⊢ ( ( 𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽 ) → ∀ 𝑥 ∈ ∪ 𝐾 ¬ { 𝑥 } ∈ 𝐾 )
32		eqid	⊢ ∪ 𝐾 = ∪ 𝐾
33	32	isperf3	⊢ ( 𝐾 ∈ Perf ↔ ( 𝐾 ∈ Top ∧ ∀ 𝑥 ∈ ∪ 𝐾 ¬ { 𝑥 } ∈ 𝐾 ) )
34	14 31 33	sylanbrc	⊢ ( ( 𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽 ) → 𝐾 ∈ Perf )