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 ⊢ 𝑋 = ∪ 𝐽
kur14.k ⊢ 𝐾 = ( cls ‘ 𝐽 )
kur14.s ⊢ 𝑆 = ∩ { 𝑥 ∈ 𝒫 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 { ( 𝑋 ∖ 𝑦 ) , ( 𝐾 ‘ 𝑦 ) } ⊆ 𝑥 ) }
Assertion kur14 ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑆 ∈ Fin ∧ ( ♯ ‘ 𝑆 ) ≤ 1 4 ) )

Proof

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