Metamath Proof Explorer

Theorem kur14

Description: Kuratowski's closure-complement theorem. There are at most 14 sets which can be obtained by the application of the closure and complement operations to a set in a topological space. (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypotheses kur14.x ⊢ X = ⋃ J
kur14.k ⊢ K = cls ⁡ J
kur14.s ⊢ S = ⋂ x ∈ 𝒫 𝒫 X | A ∈ x ∧ ∀ y ∈ x X ∖ y K ⁡ y ⊆ x
Assertion kur14 ⊢ J ∈ Top ∧ A ⊆ X → S ∈ Fin ∧ S ≤ 14

Proof

Step Hyp Ref Expression
1 kur14.x ⊢ X = ⋃ J
2 kur14.k ⊢ K = cls ⁡ J
3 kur14.s ⊢ S = ⋂ x ∈ 𝒫 𝒫 X | A ∈ x ∧ ∀ y ∈ x X ∖ y K ⁡ y ⊆ x
4 eleq1 ⊢ A = if A ⊆ X A ∅ → A ∈ x ↔ if A ⊆ X A ∅ ∈ x
5 4 anbi1d ⊢ A = if A ⊆ X A ∅ → A ∈ x ∧ ∀ y ∈ x X ∖ y K ⁡ y ⊆ x ↔ if A ⊆ X A ∅ ∈ x ∧ ∀ y ∈ x X ∖ y K ⁡ y ⊆ x
6 5 rabbidv ⊢ A = if A ⊆ X A ∅ → x ∈ 𝒫 𝒫 X | A ∈ x ∧ ∀ y ∈ x X ∖ y K ⁡ y ⊆ x = x ∈ 𝒫 𝒫 X | if A ⊆ X A ∅ ∈ x ∧ ∀ y ∈ x X ∖ y K ⁡ y ⊆ x
7 6 inteqd ⊢ A = if A ⊆ X A ∅ → ⋂ x ∈ 𝒫 𝒫 X | A ∈ x ∧ ∀ y ∈ x X ∖ y K ⁡ y ⊆ x = ⋂ x ∈ 𝒫 𝒫 X | if A ⊆ X A ∅ ∈ x ∧ ∀ y ∈ x X ∖ y K ⁡ y ⊆ x
8 3 7 syl5eq ⊢ A = if A ⊆ X A ∅ → S = ⋂ x ∈ 𝒫 𝒫 X | if A ⊆ X A ∅ ∈ x ∧ ∀ y ∈ x X ∖ y K ⁡ y ⊆ x
9 8 eleq1d ⊢ A = if A ⊆ X A ∅ → S ∈ Fin ↔ ⋂ x ∈ 𝒫 𝒫 X | if A ⊆ X A ∅ ∈ x ∧ ∀ y ∈ x X ∖ y K ⁡ y ⊆ x ∈ Fin
10 8 fveq2d ⊢ A = if A ⊆ X A ∅ → S = ⋂ x ∈ 𝒫 𝒫 X | if A ⊆ X A ∅ ∈ x ∧ ∀ y ∈ x X ∖ y K ⁡ y ⊆ x
11 10 breq1d ⊢ A = if A ⊆ X A ∅ → S ≤ 14 ↔ ⋂ x ∈ 𝒫 𝒫 X | if A ⊆ X A ∅ ∈ x ∧ ∀ y ∈ x X ∖ y K ⁡ y ⊆ x ≤ 14
12 9 11 anbi12d ⊢ A = if A ⊆ X A ∅ → S ∈ Fin ∧ S ≤ 14 ↔ ⋂ x ∈ 𝒫 𝒫 X | if A ⊆ X A ∅ ∈ x ∧ ∀ y ∈ x X ∖ y K ⁡ y ⊆ x ∈ Fin ∧ ⋂ x ∈ 𝒫 𝒫 X | if A ⊆ X A ∅ ∈ x ∧ ∀ y ∈ x X ∖ y K ⁡ y ⊆ x ≤ 14
13 unieq ⊢ J = if J ∈ Top J ∅ → ⋃ J = ⋃ if J ∈ Top J ∅
14 1 13 syl5eq ⊢ J = if J ∈ Top J ∅ → X = ⋃ if J ∈ Top J ∅
15 14 pweqd ⊢ J = if J ∈ Top J ∅ → 𝒫 X = 𝒫 ⋃ if J ∈ Top J ∅
16 15 pweqd ⊢ J = if J ∈ Top J ∅ → 𝒫 𝒫 X = 𝒫 𝒫 ⋃ if J ∈ Top J ∅
17 14 sseq2d ⊢ J = if J ∈ Top J ∅ → A ⊆ X ↔ A ⊆ ⋃ if J ∈ Top J ∅
18 sn0top ⊢ ∅ ∈ Top
19 18 elimel ⊢ if J ∈ Top J ∅ ∈ Top
20 uniexg ⊢ if J ∈ Top J ∅ ∈ Top → ⋃ if J ∈ Top J ∅ ∈ V
21 19 20 ax-mp ⊢ ⋃ if J ∈ Top J ∅ ∈ V
22 21 elpw2 ⊢ A ∈ 𝒫 ⋃ if J ∈ Top J ∅ ↔ A ⊆ ⋃ if J ∈ Top J ∅
23 17 22 bitr4di ⊢ J = if J ∈ Top J ∅ → A ⊆ X ↔ A ∈ 𝒫 ⋃ if J ∈ Top J ∅
24 23 ifbid ⊢ J = if J ∈ Top J ∅ → if A ⊆ X A ∅ = if A ∈ 𝒫 ⋃ if J ∈ Top J ∅ A ∅
25 24 eleq1d ⊢ J = if J ∈ Top J ∅ → if A ⊆ X A ∅ ∈ x ↔ if A ∈ 𝒫 ⋃ if J ∈ Top J ∅ A ∅ ∈ x
26 14 difeq1d ⊢ J = if J ∈ Top J ∅ → X ∖ y = ⋃ if J ∈ Top J ∅ ∖ y
27 fveq2 ⊢ J = if J ∈ Top J ∅ → cls ⁡ J = cls ⁡ if J ∈ Top J ∅
28 2 27 syl5eq ⊢ J = if J ∈ Top J ∅ → K = cls ⁡ if J ∈ Top J ∅
29 28 fveq1d ⊢ J = if J ∈ Top J ∅ → K ⁡ y = cls ⁡ if J ∈ Top J ∅ ⁡ y
30 26 29 preq12d ⊢ J = if J ∈ Top J ∅ → X ∖ y K ⁡ y = ⋃ if J ∈ Top J ∅ ∖ y cls ⁡ if J ∈ Top J ∅ ⁡ y
31 30 sseq1d ⊢ J = if J ∈ Top J ∅ → X ∖ y K ⁡ y ⊆ x ↔ ⋃ if J ∈ Top J ∅ ∖ y cls ⁡ if J ∈ Top J ∅ ⁡ y ⊆ x
32 31 ralbidv ⊢ J = if J ∈ Top J ∅ → ∀ y ∈ x X ∖ y K ⁡ y ⊆ x ↔ ∀ y ∈ x ⋃ if J ∈ Top J ∅ ∖ y cls ⁡ if J ∈ Top J ∅ ⁡ y ⊆ x
33 25 32 anbi12d ⊢ J = if J ∈ Top J ∅ → if A ⊆ X A ∅ ∈ x ∧ ∀ y ∈ x X ∖ y K ⁡ y ⊆ x ↔ if A ∈ 𝒫 ⋃ if J ∈ Top J ∅ A ∅ ∈ x ∧ ∀ y ∈ x ⋃ if J ∈ Top J ∅ ∖ y cls ⁡ if J ∈ Top J ∅ ⁡ y ⊆ x
34 16 33 rabeqbidv ⊢ J = if J ∈ Top J ∅ → x ∈ 𝒫 𝒫 X | if A ⊆ X A ∅ ∈ x ∧ ∀ y ∈ x X ∖ y K ⁡ y ⊆ x = x ∈ 𝒫 𝒫 ⋃ if J ∈ Top J ∅ | if A ∈ 𝒫 ⋃ if J ∈ Top J ∅ A ∅ ∈ x ∧ ∀ y ∈ x ⋃ if J ∈ Top J ∅ ∖ y cls ⁡ if J ∈ Top J ∅ ⁡ y ⊆ x
35 34 inteqd ⊢ J = if J ∈ Top J ∅ → ⋂ x ∈ 𝒫 𝒫 X | if A ⊆ X A ∅ ∈ x ∧ ∀ y ∈ x X ∖ y K ⁡ y ⊆ x = ⋂ x ∈ 𝒫 𝒫 ⋃ if J ∈ Top J ∅ | if A ∈ 𝒫 ⋃ if J ∈ Top J ∅ A ∅ ∈ x ∧ ∀ y ∈ x ⋃ if J ∈ Top J ∅ ∖ y cls ⁡ if J ∈ Top J ∅ ⁡ y ⊆ x
36 35 eleq1d ⊢ J = if J ∈ Top J ∅ → ⋂ x ∈ 𝒫 𝒫 X | if A ⊆ X A ∅ ∈ x ∧ ∀ y ∈ x X ∖ y K ⁡ y ⊆ x ∈ Fin ↔ ⋂ x ∈ 𝒫 𝒫 ⋃ if J ∈ Top J ∅ | if A ∈ 𝒫 ⋃ if J ∈ Top J ∅ A ∅ ∈ x ∧ ∀ y ∈ x ⋃ if J ∈ Top J ∅ ∖ y cls ⁡ if J ∈ Top J ∅ ⁡ y ⊆ x ∈ Fin
37 35 fveq2d ⊢ J = if J ∈ Top J ∅ → ⋂ x ∈ 𝒫 𝒫 X | if A ⊆ X A ∅ ∈ x ∧ ∀ y ∈ x X ∖ y K ⁡ y ⊆ x = ⋂ x ∈ 𝒫 𝒫 ⋃ if J ∈ Top J ∅ | if A ∈ 𝒫 ⋃ if J ∈ Top J ∅ A ∅ ∈ x ∧ ∀ y ∈ x ⋃ if J ∈ Top J ∅ ∖ y cls ⁡ if J ∈ Top J ∅ ⁡ y ⊆ x
38 37 breq1d ⊢ J = if J ∈ Top J ∅ → ⋂ x ∈ 𝒫 𝒫 X | if A ⊆ X A ∅ ∈ x ∧ ∀ y ∈ x X ∖ y K ⁡ y ⊆ x ≤ 14 ↔ ⋂ x ∈ 𝒫 𝒫 ⋃ if J ∈ Top J ∅ | if A ∈ 𝒫 ⋃ if J ∈ Top J ∅ A ∅ ∈ x ∧ ∀ y ∈ x ⋃ if J ∈ Top J ∅ ∖ y cls ⁡ if J ∈ Top J ∅ ⁡ y ⊆ x ≤ 14
39 36 38 anbi12d ⊢ J = if J ∈ Top J ∅ → ⋂ x ∈ 𝒫 𝒫 X | if A ⊆ X A ∅ ∈ x ∧ ∀ y ∈ x X ∖ y K ⁡ y ⊆ x ∈ Fin ∧ ⋂ x ∈ 𝒫 𝒫 X | if A ⊆ X A ∅ ∈ x ∧ ∀ y ∈ x X ∖ y K ⁡ y ⊆ x ≤ 14 ↔ ⋂ x ∈ 𝒫 𝒫 ⋃ if J ∈ Top J ∅ | if A ∈ 𝒫 ⋃ if J ∈ Top J ∅ A ∅ ∈ x ∧ ∀ y ∈ x ⋃ if J ∈ Top J ∅ ∖ y cls ⁡ if J ∈ Top J ∅ ⁡ y ⊆ x ∈ Fin ∧ ⋂ x ∈ 𝒫 𝒫 ⋃ if J ∈ Top J ∅ | if A ∈ 𝒫 ⋃ if J ∈ Top J ∅ A ∅ ∈ x ∧ ∀ y ∈ x ⋃ if J ∈ Top J ∅ ∖ y cls ⁡ if J ∈ Top J ∅ ⁡ y ⊆ x ≤ 14
40 eqid ⊢ ⋃ if J ∈ Top J ∅ = ⋃ if J ∈ Top J ∅
41 eqid ⊢ cls ⁡ if J ∈ Top J ∅ = cls ⁡ if J ∈ Top J ∅
42 eqid ⊢ ⋂ x ∈ 𝒫 𝒫 ⋃ if J ∈ Top J ∅ | if A ∈ 𝒫 ⋃ if J ∈ Top J ∅ A ∅ ∈ x ∧ ∀ y ∈ x ⋃ if J ∈ Top J ∅ ∖ y cls ⁡ if J ∈ Top J ∅ ⁡ y ⊆ x = ⋂ x ∈ 𝒫 𝒫 ⋃ if J ∈ Top J ∅ | if A ∈ 𝒫 ⋃ if J ∈ Top J ∅ A ∅ ∈ x ∧ ∀ y ∈ x ⋃ if J ∈ Top J ∅ ∖ y cls ⁡ if J ∈ Top J ∅ ⁡ y ⊆ x
43 0elpw ⊢ ∅ ∈ 𝒫 ⋃ if J ∈ Top J ∅
44 43 elimel ⊢ if A ∈ 𝒫 ⋃ if J ∈ Top J ∅ A ∅ ∈ 𝒫 ⋃ if J ∈ Top J ∅
45 elpwi ⊢ if A ∈ 𝒫 ⋃ if J ∈ Top J ∅ A ∅ ∈ 𝒫 ⋃ if J ∈ Top J ∅ → if A ∈ 𝒫 ⋃ if J ∈ Top J ∅ A ∅ ⊆ ⋃ if J ∈ Top J ∅
46 44 45 ax-mp ⊢ if A ∈ 𝒫 ⋃ if J ∈ Top J ∅ A ∅ ⊆ ⋃ if J ∈ Top J ∅
47 19 40 41 42 46 kur14lem10 ⊢ ⋂ x ∈ 𝒫 𝒫 ⋃ if J ∈ Top J ∅ | if A ∈ 𝒫 ⋃ if J ∈ Top J ∅ A ∅ ∈ x ∧ ∀ y ∈ x ⋃ if J ∈ Top J ∅ ∖ y cls ⁡ if J ∈ Top J ∅ ⁡ y ⊆ x ∈ Fin ∧ ⋂ x ∈ 𝒫 𝒫 ⋃ if J ∈ Top J ∅ | if A ∈ 𝒫 ⋃ if J ∈ Top J ∅ A ∅ ∈ x ∧ ∀ y ∈ x ⋃ if J ∈ Top J ∅ ∖ y cls ⁡ if J ∈ Top J ∅ ⁡ y ⊆ x ≤ 14
48 12 39 47 dedth2h ⊢ A ⊆ X ∧ J ∈ Top → S ∈ Fin ∧ S ≤ 14
49 48 ancoms ⊢ J ∈ Top ∧ A ⊆ X → S ∈ Fin ∧ S ≤ 14