| Step | Hyp | Ref
| Expression |
| 1 | | topontop 22919 |
. . 3
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) |
| 2 | 1 | 3ad2ant1 1134 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾) → 𝐽 ∈ Top) |
| 3 | | elpwi 4607 |
. . . 4
⊢ (𝑥 ∈ 𝒫 𝐽 → 𝑥 ⊆ 𝐽) |
| 4 | | simpl2 1193 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾) ∧ (𝑥 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑥)) → 𝐾 ∈ Comp) |
| 5 | | simprl 771 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾) ∧ (𝑥 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑥)) → 𝑥 ⊆ 𝐽) |
| 6 | | simpl3 1194 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾) ∧ (𝑥 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑥)) → 𝐽 ⊆ 𝐾) |
| 7 | 5, 6 | sstrd 3994 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾) ∧ (𝑥 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑥)) → 𝑥 ⊆ 𝐾) |
| 8 | | simpl1 1192 |
. . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾) ∧ (𝑥 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑥)) → 𝐽 ∈ (TopOn‘𝑋)) |
| 9 | | toponuni 22920 |
. . . . . . . . 9
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
| 10 | 8, 9 | syl 17 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾) ∧ (𝑥 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑥)) → 𝑋 = ∪
𝐽) |
| 11 | | simprr 773 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾) ∧ (𝑥 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑥)) → ∪ 𝐽 =
∪ 𝑥) |
| 12 | 10, 11 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾) ∧ (𝑥 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑥)) → 𝑋 = ∪
𝑥) |
| 13 | | sscmp.1 |
. . . . . . . 8
⊢ 𝑋 = ∪
𝐾 |
| 14 | 13 | cmpcov 23397 |
. . . . . . 7
⊢ ((𝐾 ∈ Comp ∧ 𝑥 ⊆ 𝐾 ∧ 𝑋 = ∪ 𝑥) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) |
| 15 | 4, 7, 12, 14 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾) ∧ (𝑥 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑥)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) |
| 16 | 10 | eqeq1d 2739 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾) ∧ (𝑥 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑥)) → (𝑋 = ∪
𝑦 ↔ ∪ 𝐽 =
∪ 𝑦)) |
| 17 | 16 | rexbidv 3179 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾) ∧ (𝑥 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑥)) → (∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦 ↔ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∪ 𝐽 =
∪ 𝑦)) |
| 18 | 15, 17 | mpbid 232 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾) ∧ (𝑥 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑥)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∪ 𝐽 =
∪ 𝑦) |
| 19 | 18 | expr 456 |
. . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾) ∧ 𝑥 ⊆ 𝐽) → (∪ 𝐽 = ∪
𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∪ 𝐽 =
∪ 𝑦)) |
| 20 | 3, 19 | sylan2 593 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾) ∧ 𝑥 ∈ 𝒫 𝐽) → (∪ 𝐽 = ∪
𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∪ 𝐽 =
∪ 𝑦)) |
| 21 | 20 | ralrimiva 3146 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾) → ∀𝑥 ∈ 𝒫 𝐽(∪ 𝐽 = ∪
𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∪ 𝐽 =
∪ 𝑦)) |
| 22 | | eqid 2737 |
. . 3
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 23 | 22 | iscmp 23396 |
. 2
⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝒫 𝐽(∪
𝐽 = ∪ 𝑥
→ ∃𝑦 ∈
(𝒫 𝑥 ∩
Fin)∪ 𝐽 = ∪ 𝑦))) |
| 24 | 2, 21, 23 | sylanbrc 583 |
1
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾) → 𝐽 ∈ Comp) |