| Step | Hyp | Ref
| Expression |
| 1 | | kur14lem.s |
. . 3
⊢ 𝑆 = ∩
{𝑥 ∈ 𝒫
𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑥)} |
| 2 | | vex 3484 |
. . . . . 6
⊢ 𝑠 ∈ V |
| 3 | 2 | elintrab 4960 |
. . . . 5
⊢ (𝑠 ∈ ∩ {𝑥
∈ 𝒫 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑥)} ↔ ∀𝑥 ∈ 𝒫 𝒫 𝑋((𝐴 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑥) → 𝑠 ∈ 𝑥)) |
| 4 | | ssun1 4178 |
. . . . . . . 8
⊢ {𝐴, (𝑋 ∖ 𝐴), (𝐾‘𝐴)} ⊆ ({𝐴, (𝑋 ∖ 𝐴), (𝐾‘𝐴)} ∪ {𝐵, 𝐶, (𝐼‘𝐴)}) |
| 5 | | ssun1 4178 |
. . . . . . . . 9
⊢ ({𝐴, (𝑋 ∖ 𝐴), (𝐾‘𝐴)} ∪ {𝐵, 𝐶, (𝐼‘𝐴)}) ⊆ (({𝐴, (𝑋 ∖ 𝐴), (𝐾‘𝐴)} ∪ {𝐵, 𝐶, (𝐼‘𝐴)}) ∪ {(𝐾‘𝐵), 𝐷, (𝐾‘(𝐼‘𝐴))}) |
| 6 | | ssun1 4178 |
. . . . . . . . . 10
⊢ (({𝐴, (𝑋 ∖ 𝐴), (𝐾‘𝐴)} ∪ {𝐵, 𝐶, (𝐼‘𝐴)}) ∪ {(𝐾‘𝐵), 𝐷, (𝐾‘(𝐼‘𝐴))}) ⊆ ((({𝐴, (𝑋 ∖ 𝐴), (𝐾‘𝐴)} ∪ {𝐵, 𝐶, (𝐼‘𝐴)}) ∪ {(𝐾‘𝐵), 𝐷, (𝐾‘(𝐼‘𝐴))}) ∪ ({(𝐼‘𝐶), (𝐾‘𝐷), (𝐼‘(𝐾‘𝐵))} ∪ {(𝐾‘(𝐼‘𝐶)), (𝐼‘(𝐾‘(𝐼‘𝐴)))})) |
| 7 | | kur14lem.t |
. . . . . . . . . 10
⊢ 𝑇 = ((({𝐴, (𝑋 ∖ 𝐴), (𝐾‘𝐴)} ∪ {𝐵, 𝐶, (𝐼‘𝐴)}) ∪ {(𝐾‘𝐵), 𝐷, (𝐾‘(𝐼‘𝐴))}) ∪ ({(𝐼‘𝐶), (𝐾‘𝐷), (𝐼‘(𝐾‘𝐵))} ∪ {(𝐾‘(𝐼‘𝐶)), (𝐼‘(𝐾‘(𝐼‘𝐴)))})) |
| 8 | 6, 7 | sseqtrri 4033 |
. . . . . . . . 9
⊢ (({𝐴, (𝑋 ∖ 𝐴), (𝐾‘𝐴)} ∪ {𝐵, 𝐶, (𝐼‘𝐴)}) ∪ {(𝐾‘𝐵), 𝐷, (𝐾‘(𝐼‘𝐴))}) ⊆ 𝑇 |
| 9 | 5, 8 | sstri 3993 |
. . . . . . . 8
⊢ ({𝐴, (𝑋 ∖ 𝐴), (𝐾‘𝐴)} ∪ {𝐵, 𝐶, (𝐼‘𝐴)}) ⊆ 𝑇 |
| 10 | 4, 9 | sstri 3993 |
. . . . . . 7
⊢ {𝐴, (𝑋 ∖ 𝐴), (𝐾‘𝐴)} ⊆ 𝑇 |
| 11 | | kur14lem.j |
. . . . . . . . . . 11
⊢ 𝐽 ∈ Top |
| 12 | | kur14lem.x |
. . . . . . . . . . . 12
⊢ 𝑋 = ∪
𝐽 |
| 13 | 12 | topopn 22912 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽) |
| 14 | 11, 13 | ax-mp 5 |
. . . . . . . . . 10
⊢ 𝑋 ∈ 𝐽 |
| 15 | 14 | elexi 3503 |
. . . . . . . . 9
⊢ 𝑋 ∈ V |
| 16 | | kur14lem.a |
. . . . . . . . 9
⊢ 𝐴 ⊆ 𝑋 |
| 17 | 15, 16 | ssexi 5322 |
. . . . . . . 8
⊢ 𝐴 ∈ V |
| 18 | 17 | tpid1 4768 |
. . . . . . 7
⊢ 𝐴 ∈ {𝐴, (𝑋 ∖ 𝐴), (𝐾‘𝐴)} |
| 19 | 10, 18 | sselii 3980 |
. . . . . 6
⊢ 𝐴 ∈ 𝑇 |
| 20 | | kur14lem.k |
. . . . . . . . 9
⊢ 𝐾 = (cls‘𝐽) |
| 21 | | kur14lem.i |
. . . . . . . . 9
⊢ 𝐼 = (int‘𝐽) |
| 22 | | kur14lem.b |
. . . . . . . . 9
⊢ 𝐵 = (𝑋 ∖ (𝐾‘𝐴)) |
| 23 | | kur14lem.c |
. . . . . . . . 9
⊢ 𝐶 = (𝐾‘(𝑋 ∖ 𝐴)) |
| 24 | | kur14lem.d |
. . . . . . . . 9
⊢ 𝐷 = (𝐼‘(𝐾‘𝐴)) |
| 25 | 11, 12, 20, 21, 16, 22, 23, 24, 7 | kur14lem7 35217 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝑇 → (𝑦 ⊆ 𝑋 ∧ {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑇)) |
| 26 | 25 | simprd 495 |
. . . . . . 7
⊢ (𝑦 ∈ 𝑇 → {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑇) |
| 27 | 26 | rgen 3063 |
. . . . . 6
⊢
∀𝑦 ∈
𝑇 {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑇 |
| 28 | 25 | simpld 494 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑇 → 𝑦 ⊆ 𝑋) |
| 29 | 15 | elpw2 5334 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝒫 𝑋 ↔ 𝑦 ⊆ 𝑋) |
| 30 | 28, 29 | sylibr 234 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝑇 → 𝑦 ∈ 𝒫 𝑋) |
| 31 | 30 | ssriv 3987 |
. . . . . . . 8
⊢ 𝑇 ⊆ 𝒫 𝑋 |
| 32 | 15 | pwex 5380 |
. . . . . . . . 9
⊢ 𝒫
𝑋 ∈ V |
| 33 | 32 | elpw2 5334 |
. . . . . . . 8
⊢ (𝑇 ∈ 𝒫 𝒫
𝑋 ↔ 𝑇 ⊆ 𝒫 𝑋) |
| 34 | 31, 33 | mpbir 231 |
. . . . . . 7
⊢ 𝑇 ∈ 𝒫 𝒫
𝑋 |
| 35 | | eleq2 2830 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑇 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑇)) |
| 36 | | sseq2 4010 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑇 → ({(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑥 ↔ {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑇)) |
| 37 | 36 | raleqbi1dv 3338 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑇 → (∀𝑦 ∈ 𝑥 {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑥 ↔ ∀𝑦 ∈ 𝑇 {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑇)) |
| 38 | 35, 37 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑥 = 𝑇 → ((𝐴 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑥) ↔ (𝐴 ∈ 𝑇 ∧ ∀𝑦 ∈ 𝑇 {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑇))) |
| 39 | | eleq2 2830 |
. . . . . . . . 9
⊢ (𝑥 = 𝑇 → (𝑠 ∈ 𝑥 ↔ 𝑠 ∈ 𝑇)) |
| 40 | 38, 39 | imbi12d 344 |
. . . . . . . 8
⊢ (𝑥 = 𝑇 → (((𝐴 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑥) → 𝑠 ∈ 𝑥) ↔ ((𝐴 ∈ 𝑇 ∧ ∀𝑦 ∈ 𝑇 {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑇) → 𝑠 ∈ 𝑇))) |
| 41 | 40 | rspccv 3619 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝒫 𝒫 𝑋((𝐴 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑥) → 𝑠 ∈ 𝑥) → (𝑇 ∈ 𝒫 𝒫 𝑋 → ((𝐴 ∈ 𝑇 ∧ ∀𝑦 ∈ 𝑇 {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑇) → 𝑠 ∈ 𝑇))) |
| 42 | 34, 41 | mpi 20 |
. . . . . 6
⊢
(∀𝑥 ∈
𝒫 𝒫 𝑋((𝐴 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑥) → 𝑠 ∈ 𝑥) → ((𝐴 ∈ 𝑇 ∧ ∀𝑦 ∈ 𝑇 {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑇) → 𝑠 ∈ 𝑇)) |
| 43 | 19, 27, 42 | mp2ani 698 |
. . . . 5
⊢
(∀𝑥 ∈
𝒫 𝒫 𝑋((𝐴 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑥) → 𝑠 ∈ 𝑥) → 𝑠 ∈ 𝑇) |
| 44 | 3, 43 | sylbi 217 |
. . . 4
⊢ (𝑠 ∈ ∩ {𝑥
∈ 𝒫 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑥)} → 𝑠 ∈ 𝑇) |
| 45 | 44 | ssriv 3987 |
. . 3
⊢ ∩ {𝑥
∈ 𝒫 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑥)} ⊆ 𝑇 |
| 46 | 1, 45 | eqsstri 4030 |
. 2
⊢ 𝑆 ⊆ 𝑇 |
| 47 | 11, 12, 20, 21, 16, 22, 23, 24, 7 | kur14lem8 35218 |
. 2
⊢ (𝑇 ∈ Fin ∧
(♯‘𝑇) ≤
;14) |
| 48 | | 1nn0 12542 |
. . 3
⊢ 1 ∈
ℕ0 |
| 49 | | 4nn0 12545 |
. . 3
⊢ 4 ∈
ℕ0 |
| 50 | 48, 49 | deccl 12748 |
. 2
⊢ ;14 ∈
ℕ0 |
| 51 | 46, 47, 50 | hashsslei 14465 |
1
⊢ (𝑆 ∈ Fin ∧
(♯‘𝑆) ≤
;14) |