Description: Property of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Hypothesis | lpfval.1 | ⊢ 𝑋 = ∪ 𝐽 | |
Assertion | perfi | ⊢ ( ( 𝐽 ∈ Perf ∧ 𝑃 ∈ 𝑋 ) → ¬ { 𝑃 } ∈ 𝐽 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lpfval.1 | ⊢ 𝑋 = ∪ 𝐽 | |
2 | 1 | isperf3 | ⊢ ( 𝐽 ∈ Perf ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝑋 ¬ { 𝑥 } ∈ 𝐽 ) ) |
3 | 2 | simprbi | ⊢ ( 𝐽 ∈ Perf → ∀ 𝑥 ∈ 𝑋 ¬ { 𝑥 } ∈ 𝐽 ) |
4 | sneq | ⊢ ( 𝑥 = 𝑃 → { 𝑥 } = { 𝑃 } ) | |
5 | 4 | eleq1d | ⊢ ( 𝑥 = 𝑃 → ( { 𝑥 } ∈ 𝐽 ↔ { 𝑃 } ∈ 𝐽 ) ) |
6 | 5 | notbid | ⊢ ( 𝑥 = 𝑃 → ( ¬ { 𝑥 } ∈ 𝐽 ↔ ¬ { 𝑃 } ∈ 𝐽 ) ) |
7 | 6 | rspccva | ⊢ ( ( ∀ 𝑥 ∈ 𝑋 ¬ { 𝑥 } ∈ 𝐽 ∧ 𝑃 ∈ 𝑋 ) → ¬ { 𝑃 } ∈ 𝐽 ) |
8 | 3 7 | sylan | ⊢ ( ( 𝐽 ∈ Perf ∧ 𝑃 ∈ 𝑋 ) → ¬ { 𝑃 } ∈ 𝐽 ) |