restperf

Description: Perfection of a subspace. Note that the term "perfect set" is reserved forclosed sets which are perfect in the subspace topology. (Contributed by Mario Carneiro, 25-Dec-2016)

	Ref	Expression
Hypotheses	restcls.1	⊢ 𝑋 = ∪ 𝐽
	restcls.2	⊢ 𝐾 = ( 𝐽 ↾_t 𝑌 )
Assertion	restperf	⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐾 ∈ Perf ↔ 𝑌 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		restcls.1	⊢ 𝑋 = ∪ 𝐽
2		restcls.2	⊢ 𝐾 = ( 𝐽 ↾_t 𝑌 )
3	1	toptopon	⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
4		resttopon	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐽 ↾_t 𝑌 ) ∈ ( TopOn ‘ 𝑌 ) )
5	3 4	sylanb	⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐽 ↾_t 𝑌 ) ∈ ( TopOn ‘ 𝑌 ) )
6	2 5	eqeltrid	⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
7		topontop	⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝐾 ∈ Top )
8	6 7	syl	⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → 𝐾 ∈ Top )
9		eqid	⊢ ∪ 𝐾 = ∪ 𝐾
10	9	isperf	⊢ ( 𝐾 ∈ Perf ↔ ( 𝐾 ∈ Top ∧ ( ( limPt ‘ 𝐾 ) ‘ ∪ 𝐾 ) = ∪ 𝐾 ) )
11	10	baib	⊢ ( 𝐾 ∈ Top → ( 𝐾 ∈ Perf ↔ ( ( limPt ‘ 𝐾 ) ‘ ∪ 𝐾 ) = ∪ 𝐾 ) )
12	8 11	syl	⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐾 ∈ Perf ↔ ( ( limPt ‘ 𝐾 ) ‘ ∪ 𝐾 ) = ∪ 𝐾 ) )
13		sseqin2	⊢ ( 𝑌 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑌 ) ↔ ( ( ( limPt ‘ 𝐽 ) ‘ 𝑌 ) ∩ 𝑌 ) = 𝑌 )
14		ssid	⊢ 𝑌 ⊆ 𝑌
15	1 2	restlp	⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑌 ⊆ 𝑌 ) → ( ( limPt ‘ 𝐾 ) ‘ 𝑌 ) = ( ( ( limPt ‘ 𝐽 ) ‘ 𝑌 ) ∩ 𝑌 ) )
16	14 15	mp3an3	⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → ( ( limPt ‘ 𝐾 ) ‘ 𝑌 ) = ( ( ( limPt ‘ 𝐽 ) ‘ 𝑌 ) ∩ 𝑌 ) )
17		toponuni	⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 = ∪ 𝐾 )
18	6 17	syl	⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → 𝑌 = ∪ 𝐾 )
19	18	fveq2d	⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → ( ( limPt ‘ 𝐾 ) ‘ 𝑌 ) = ( ( limPt ‘ 𝐾 ) ‘ ∪ 𝐾 ) )
20	16 19	eqtr3d	⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → ( ( ( limPt ‘ 𝐽 ) ‘ 𝑌 ) ∩ 𝑌 ) = ( ( limPt ‘ 𝐾 ) ‘ ∪ 𝐾 ) )
21	20 18	eqeq12d	⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → ( ( ( ( limPt ‘ 𝐽 ) ‘ 𝑌 ) ∩ 𝑌 ) = 𝑌 ↔ ( ( limPt ‘ 𝐾 ) ‘ ∪ 𝐾 ) = ∪ 𝐾 ) )
22	13 21	bitrid	⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → ( 𝑌 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑌 ) ↔ ( ( limPt ‘ 𝐾 ) ‘ ∪ 𝐾 ) = ∪ 𝐾 ) )
23	12 22	bitr4d	⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐾 ∈ Perf ↔ 𝑌 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑌 ) ) )

Metamath Proof Explorer

Theorem restperf

Proof