Step | Hyp | Ref
| Expression |
1 | | restcls.2 |
. . . 4
⊢ 𝐾 = (𝐽 ↾t 𝑌) |
2 | | perftop 20960 |
. . . . . . 7
⊢ (𝐽 ∈ Perf → 𝐽 ∈ Top) |
3 | 2 | adantr 481 |
. . . . . 6
⊢ ((𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽) → 𝐽 ∈ Top) |
4 | | restcls.1 |
. . . . . . 7
⊢ 𝑋 = ∪
𝐽 |
5 | 4 | toptopon 20722 |
. . . . . 6
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
6 | 3, 5 | sylib 208 |
. . . . 5
⊢ ((𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽) → 𝐽 ∈ (TopOn‘𝑋)) |
7 | | elssuni 4467 |
. . . . . . 7
⊢ (𝑌 ∈ 𝐽 → 𝑌 ⊆ ∪ 𝐽) |
8 | 7 | adantl 482 |
. . . . . 6
⊢ ((𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽) → 𝑌 ⊆ ∪ 𝐽) |
9 | 8, 4 | syl6sseqr 3652 |
. . . . 5
⊢ ((𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽) → 𝑌 ⊆ 𝑋) |
10 | | resttopon 20965 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝐽 ↾t 𝑌) ∈ (TopOn‘𝑌)) |
11 | 6, 9, 10 | syl2anc 693 |
. . . 4
⊢ ((𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽) → (𝐽 ↾t 𝑌) ∈ (TopOn‘𝑌)) |
12 | 1, 11 | syl5eqel 2705 |
. . 3
⊢ ((𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽) → 𝐾 ∈ (TopOn‘𝑌)) |
13 | | topontop 20718 |
. . 3
⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top) |
14 | 12, 13 | syl 17 |
. 2
⊢ ((𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽) → 𝐾 ∈ Top) |
15 | 9 | sselda 3603 |
. . . . . 6
⊢ (((𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽) ∧ 𝑥 ∈ 𝑌) → 𝑥 ∈ 𝑋) |
16 | 4 | perfi 20959 |
. . . . . . 7
⊢ ((𝐽 ∈ Perf ∧ 𝑥 ∈ 𝑋) → ¬ {𝑥} ∈ 𝐽) |
17 | 16 | adantlr 751 |
. . . . . 6
⊢ (((𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽) ∧ 𝑥 ∈ 𝑋) → ¬ {𝑥} ∈ 𝐽) |
18 | 15, 17 | syldan 487 |
. . . . 5
⊢ (((𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽) ∧ 𝑥 ∈ 𝑌) → ¬ {𝑥} ∈ 𝐽) |
19 | 1 | eleq2i 2693 |
. . . . . 6
⊢ ({𝑥} ∈ 𝐾 ↔ {𝑥} ∈ (𝐽 ↾t 𝑌)) |
20 | | restopn2 20981 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ 𝑌 ∈ 𝐽) → ({𝑥} ∈ (𝐽 ↾t 𝑌) ↔ ({𝑥} ∈ 𝐽 ∧ {𝑥} ⊆ 𝑌))) |
21 | 2, 20 | sylan 488 |
. . . . . . . 8
⊢ ((𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽) → ({𝑥} ∈ (𝐽 ↾t 𝑌) ↔ ({𝑥} ∈ 𝐽 ∧ {𝑥} ⊆ 𝑌))) |
22 | 21 | adantr 481 |
. . . . . . 7
⊢ (((𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽) ∧ 𝑥 ∈ 𝑌) → ({𝑥} ∈ (𝐽 ↾t 𝑌) ↔ ({𝑥} ∈ 𝐽 ∧ {𝑥} ⊆ 𝑌))) |
23 | | simpl 473 |
. . . . . . 7
⊢ (({𝑥} ∈ 𝐽 ∧ {𝑥} ⊆ 𝑌) → {𝑥} ∈ 𝐽) |
24 | 22, 23 | syl6bi 243 |
. . . . . 6
⊢ (((𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽) ∧ 𝑥 ∈ 𝑌) → ({𝑥} ∈ (𝐽 ↾t 𝑌) → {𝑥} ∈ 𝐽)) |
25 | 19, 24 | syl5bi 232 |
. . . . 5
⊢ (((𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽) ∧ 𝑥 ∈ 𝑌) → ({𝑥} ∈ 𝐾 → {𝑥} ∈ 𝐽)) |
26 | 18, 25 | mtod 189 |
. . . 4
⊢ (((𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽) ∧ 𝑥 ∈ 𝑌) → ¬ {𝑥} ∈ 𝐾) |
27 | 26 | ralrimiva 2966 |
. . 3
⊢ ((𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽) → ∀𝑥 ∈ 𝑌 ¬ {𝑥} ∈ 𝐾) |
28 | | toponuni 20719 |
. . . . 5
⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 = ∪ 𝐾) |
29 | 12, 28 | syl 17 |
. . . 4
⊢ ((𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽) → 𝑌 = ∪ 𝐾) |
30 | 29 | raleqdv 3144 |
. . 3
⊢ ((𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽) → (∀𝑥 ∈ 𝑌 ¬ {𝑥} ∈ 𝐾 ↔ ∀𝑥 ∈ ∪ 𝐾 ¬ {𝑥} ∈ 𝐾)) |
31 | 27, 30 | mpbid 222 |
. 2
⊢ ((𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽) → ∀𝑥 ∈ ∪ 𝐾 ¬ {𝑥} ∈ 𝐾) |
32 | | eqid 2622 |
. . 3
⊢ ∪ 𝐾 =
∪ 𝐾 |
33 | 32 | isperf3 20957 |
. 2
⊢ (𝐾 ∈ Perf ↔ (𝐾 ∈ Top ∧ ∀𝑥 ∈ ∪ 𝐾
¬ {𝑥} ∈ 𝐾)) |
34 | 14, 31, 33 | sylanbrc 698 |
1
⊢ ((𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽) → 𝐾 ∈ Perf) |