This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrdi ⊢ ( ( ( 𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑌 ) → ( { 𝑥 } ∈ ( 𝐽 ↾t 𝑌 ) → { 𝑥 } ∈ 𝐽 ) )
25 19 24 biimtrid ⊢ ( ( ( 𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑌 ) → ( { 𝑥 } ∈ 𝐾 → { 𝑥 } ∈ 𝐽 ) )
26 18 25 mtod ⊢ ( ( ( 𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑌 ) → ¬ { 𝑥 } ∈ 𝐾 )
27 26 ralrimiva ⊢ ( ( 𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽 ) → ∀ 𝑥 ∈ 𝑌 ¬ { 𝑥 } ∈ 𝐾 )
28 toponuni ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 = ∪ 𝐾 )
29 12 28 syl ⊢ ( ( 𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽 ) → 𝑌 = ∪ 𝐾 )
30 27 29 raleqtrdv ⊢ ( ( 𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽 ) → ∀ 𝑥 ∈ ∪ 𝐾 ¬ { 𝑥 } ∈ 𝐾 )
31 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
32 31 isperf3 ⊢ ( 𝐾 ∈ Perf ↔ ( 𝐾 ∈ Top ∧ ∀ 𝑥 ∈ ∪ 𝐾 ¬ { 𝑥 } ∈ 𝐾 ) )
33 14 30 32 sylanbrc ⊢ ( ( 𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽 ) → 𝐾 ∈ Perf )