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 = U. J
kur14.k 
|- K = ( cls ` J )
kur14.s 
|- S = |^| { x e. ~P ~P X | ( A e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) }
Assertion kur14 
|- ( ( J e. Top /\ A C_ X ) -> ( S e. Fin /\ ( # ` S ) <_ ; 1 4 ) )

Proof

Step Hyp Ref Expression
1 kur14.x 
 |-  X = U. J
2 kur14.k 
 |-  K = ( cls ` J )
3 kur14.s 
 |-  S = |^| { x e. ~P ~P X | ( A e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) }
4 eleq1 
 |-  ( A = if ( A C_ X , A , (/) ) -> ( A e. x <-> if ( A C_ X , A , (/) ) e. x ) )
5 4 anbi1d 
 |-  ( A = if ( A C_ X , A , (/) ) -> ( ( A e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) <-> ( if ( A C_ X , A , (/) ) e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) ) )
6 5 rabbidv 
 |-  ( A = if ( A C_ X , A , (/) ) -> { x e. ~P ~P X | ( A e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) } = { x e. ~P ~P X | ( if ( A C_ X , A , (/) ) e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) } )
7 6 inteqd 
 |-  ( A = if ( A C_ X , A , (/) ) -> |^| { x e. ~P ~P X | ( A e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) } = |^| { x e. ~P ~P X | ( if ( A C_ X , A , (/) ) e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) } )
8 3 7 syl5eq 
 |-  ( A = if ( A C_ X , A , (/) ) -> S = |^| { x e. ~P ~P X | ( if ( A C_ X , A , (/) ) e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) } )
9 8 eleq1d 
 |-  ( A = if ( A C_ X , A , (/) ) -> ( S e. Fin <-> |^| { x e. ~P ~P X | ( if ( A C_ X , A , (/) ) e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) } e. Fin ) )
10 8 fveq2d 
 |-  ( A = if ( A C_ X , A , (/) ) -> ( # ` S ) = ( # ` |^| { x e. ~P ~P X | ( if ( A C_ X , A , (/) ) e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) } ) )
11 10 breq1d 
 |-  ( A = if ( A C_ X , A , (/) ) -> ( ( # ` S ) <_ ; 1 4 <-> ( # ` |^| { x e. ~P ~P X | ( if ( A C_ X , A , (/) ) e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) } ) <_ ; 1 4 ) )
12 9 11 anbi12d 
 |-  ( A = if ( A C_ X , A , (/) ) -> ( ( S e. Fin /\ ( # ` S ) <_ ; 1 4 ) <-> ( |^| { x e. ~P ~P X | ( if ( A C_ X , A , (/) ) e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) } e. Fin /\ ( # ` |^| { x e. ~P ~P X | ( if ( A C_ X , A , (/) ) e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) } ) <_ ; 1 4 ) ) )
13 unieq 
 |-  ( J = if ( J e. Top , J , { (/) } ) -> U. J = U. if ( J e. Top , J , { (/) } ) )
14 1 13 syl5eq 
 |-  ( J = if ( J e. Top , J , { (/) } ) -> X = U. if ( J e. Top , J , { (/) } ) )
15 14 pweqd 
 |-  ( J = if ( J e. Top , J , { (/) } ) -> ~P X = ~P U. if ( J e. Top , J , { (/) } ) )
16 15 pweqd 
 |-  ( J = if ( J e. Top , J , { (/) } ) -> ~P ~P X = ~P ~P U. if ( J e. Top , J , { (/) } ) )
17 14 sseq2d 
 |-  ( J = if ( J e. Top , J , { (/) } ) -> ( A C_ X <-> A C_ U. if ( J e. Top , J , { (/) } ) ) )
18 sn0top 
 |-  { (/) } e. Top
19 18 elimel 
 |-  if ( J e. Top , J , { (/) } ) e. Top
20 uniexg 
 |-  ( if ( J e. Top , J , { (/) } ) e. Top -> U. if ( J e. Top , J , { (/) } ) e. _V )
21 19 20 ax-mp 
 |-  U. if ( J e. Top , J , { (/) } ) e. _V
22 21 elpw2 
 |-  ( A e. ~P U. if ( J e. Top , J , { (/) } ) <-> A C_ U. if ( J e. Top , J , { (/) } ) )
23 17 22 bitr4di 
 |-  ( J = if ( J e. Top , J , { (/) } ) -> ( A C_ X <-> A e. ~P U. if ( J e. Top , J , { (/) } ) ) )
24 23 ifbid 
 |-  ( J = if ( J e. Top , J , { (/) } ) -> if ( A C_ X , A , (/) ) = if ( A e. ~P U. if ( J e. Top , J , { (/) } ) , A , (/) ) )
25 24 eleq1d 
 |-  ( J = if ( J e. Top , J , { (/) } ) -> ( if ( A C_ X , A , (/) ) e. x <-> if ( A e. ~P U. if ( J e. Top , J , { (/) } ) , A , (/) ) e. x ) )
26 14 difeq1d 
 |-  ( J = if ( J e. Top , J , { (/) } ) -> ( X \ y ) = ( U. if ( J e. Top , J , { (/) } ) \ y ) )
27 fveq2 
 |-  ( J = if ( J e. Top , J , { (/) } ) -> ( cls ` J ) = ( cls ` if ( J e. Top , J , { (/) } ) ) )
28 2 27 syl5eq 
 |-  ( J = if ( J e. Top , J , { (/) } ) -> K = ( cls ` if ( J e. Top , J , { (/) } ) ) )
29 28 fveq1d 
 |-  ( J = if ( J e. Top , J , { (/) } ) -> ( K ` y ) = ( ( cls ` if ( J e. Top , J , { (/) } ) ) ` y ) )
30 26 29 preq12d 
 |-  ( J = if ( J e. Top , J , { (/) } ) -> { ( X \ y ) , ( K ` y ) } = { ( U. if ( J e. Top , J , { (/) } ) \ y ) , ( ( cls ` if ( J e. Top , J , { (/) } ) ) ` y ) } )
31 30 sseq1d 
 |-  ( J = if ( J e. Top , J , { (/) } ) -> ( { ( X \ y ) , ( K ` y ) } C_ x <-> { ( U. if ( J e. Top , J , { (/) } ) \ y ) , ( ( cls ` if ( J e. Top , J , { (/) } ) ) ` y ) } C_ x ) )
32 31 ralbidv 
 |-  ( J = if ( J e. Top , J , { (/) } ) -> ( A. y e. x { ( X \ y ) , ( K ` y ) } C_ x <-> A. y e. x { ( U. if ( J e. Top , J , { (/) } ) \ y ) , ( ( cls ` if ( J e. Top , J , { (/) } ) ) ` y ) } C_ x ) )
33 25 32 anbi12d 
 |-  ( J = if ( J e. Top , J , { (/) } ) -> ( ( if ( A C_ X , A , (/) ) e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) <-> ( if ( A e. ~P U. if ( J e. Top , J , { (/) } ) , A , (/) ) e. x /\ A. y e. x { ( U. if ( J e. Top , J , { (/) } ) \ y ) , ( ( cls ` if ( J e. Top , J , { (/) } ) ) ` y ) } C_ x ) ) )
34 16 33 rabeqbidv 
 |-  ( J = if ( J e. Top , J , { (/) } ) -> { x e. ~P ~P X | ( if ( A C_ X , A , (/) ) e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) } = { x e. ~P ~P U. if ( J e. Top , J , { (/) } ) | ( if ( A e. ~P U. if ( J e. Top , J , { (/) } ) , A , (/) ) e. x /\ A. y e. x { ( U. if ( J e. Top , J , { (/) } ) \ y ) , ( ( cls ` if ( J e. Top , J , { (/) } ) ) ` y ) } C_ x ) } )
35 34 inteqd 
 |-  ( J = if ( J e. Top , J , { (/) } ) -> |^| { x e. ~P ~P X | ( if ( A C_ X , A , (/) ) e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) } = |^| { x e. ~P ~P U. if ( J e. Top , J , { (/) } ) | ( if ( A e. ~P U. if ( J e. Top , J , { (/) } ) , A , (/) ) e. x /\ A. y e. x { ( U. if ( J e. Top , J , { (/) } ) \ y ) , ( ( cls ` if ( J e. Top , J , { (/) } ) ) ` y ) } C_ x ) } )
36 35 eleq1d 
 |-  ( J = if ( J e. Top , J , { (/) } ) -> ( |^| { x e. ~P ~P X | ( if ( A C_ X , A , (/) ) e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) } e. Fin <-> |^| { x e. ~P ~P U. if ( J e. Top , J , { (/) } ) | ( if ( A e. ~P U. if ( J e. Top , J , { (/) } ) , A , (/) ) e. x /\ A. y e. x { ( U. if ( J e. Top , J , { (/) } ) \ y ) , ( ( cls ` if ( J e. Top , J , { (/) } ) ) ` y ) } C_ x ) } e. Fin ) )
37 35 fveq2d 
 |-  ( J = if ( J e. Top , J , { (/) } ) -> ( # ` |^| { x e. ~P ~P X | ( if ( A C_ X , A , (/) ) e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) } ) = ( # ` |^| { x e. ~P ~P U. if ( J e. Top , J , { (/) } ) | ( if ( A e. ~P U. if ( J e. Top , J , { (/) } ) , A , (/) ) e. x /\ A. y e. x { ( U. if ( J e. Top , J , { (/) } ) \ y ) , ( ( cls ` if ( J e. Top , J , { (/) } ) ) ` y ) } C_ x ) } ) )
38 37 breq1d 
 |-  ( J = if ( J e. Top , J , { (/) } ) -> ( ( # ` |^| { x e. ~P ~P X | ( if ( A C_ X , A , (/) ) e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) } ) <_ ; 1 4 <-> ( # ` |^| { x e. ~P ~P U. if ( J e. Top , J , { (/) } ) | ( if ( A e. ~P U. if ( J e. Top , J , { (/) } ) , A , (/) ) e. x /\ A. y e. x { ( U. if ( J e. Top , J , { (/) } ) \ y ) , ( ( cls ` if ( J e. Top , J , { (/) } ) ) ` y ) } C_ x ) } ) <_ ; 1 4 ) )
39 36 38 anbi12d 
 |-  ( J = if ( J e. Top , J , { (/) } ) -> ( ( |^| { x e. ~P ~P X | ( if ( A C_ X , A , (/) ) e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) } e. Fin /\ ( # ` |^| { x e. ~P ~P X | ( if ( A C_ X , A , (/) ) e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) } ) <_ ; 1 4 ) <-> ( |^| { x e. ~P ~P U. if ( J e. Top , J , { (/) } ) | ( if ( A e. ~P U. if ( J e. Top , J , { (/) } ) , A , (/) ) e. x /\ A. y e. x { ( U. if ( J e. Top , J , { (/) } ) \ y ) , ( ( cls ` if ( J e. Top , J , { (/) } ) ) ` y ) } C_ x ) } e. Fin /\ ( # ` |^| { x e. ~P ~P U. if ( J e. Top , J , { (/) } ) | ( if ( A e. ~P U. if ( J e. Top , J , { (/) } ) , A , (/) ) e. x /\ A. y e. x { ( U. if ( J e. Top , J , { (/) } ) \ y ) , ( ( cls ` if ( J e. Top , J , { (/) } ) ) ` y ) } C_ x ) } ) <_ ; 1 4 ) ) )
40 eqid 
 |-  U. if ( J e. Top , J , { (/) } ) = U. if ( J e. Top , J , { (/) } )
41 eqid 
 |-  ( cls ` if ( J e. Top , J , { (/) } ) ) = ( cls ` if ( J e. Top , J , { (/) } ) )
42 eqid 
 |-  |^| { x e. ~P ~P U. if ( J e. Top , J , { (/) } ) | ( if ( A e. ~P U. if ( J e. Top , J , { (/) } ) , A , (/) ) e. x /\ A. y e. x { ( U. if ( J e. Top , J , { (/) } ) \ y ) , ( ( cls ` if ( J e. Top , J , { (/) } ) ) ` y ) } C_ x ) } = |^| { x e. ~P ~P U. if ( J e. Top , J , { (/) } ) | ( if ( A e. ~P U. if ( J e. Top , J , { (/) } ) , A , (/) ) e. x /\ A. y e. x { ( U. if ( J e. Top , J , { (/) } ) \ y ) , ( ( cls ` if ( J e. Top , J , { (/) } ) ) ` y ) } C_ x ) }
43 0elpw 
 |-  (/) e. ~P U. if ( J e. Top , J , { (/) } )
44 43 elimel 
 |-  if ( A e. ~P U. if ( J e. Top , J , { (/) } ) , A , (/) ) e. ~P U. if ( J e. Top , J , { (/) } )
45 elpwi 
 |-  ( if ( A e. ~P U. if ( J e. Top , J , { (/) } ) , A , (/) ) e. ~P U. if ( J e. Top , J , { (/) } ) -> if ( A e. ~P U. if ( J e. Top , J , { (/) } ) , A , (/) ) C_ U. if ( J e. Top , J , { (/) } ) )
46 44 45 ax-mp 
 |-  if ( A e. ~P U. if ( J e. Top , J , { (/) } ) , A , (/) ) C_ U. if ( J e. Top , J , { (/) } )
47 19 40 41 42 46 kur14lem10 
 |-  ( |^| { x e. ~P ~P U. if ( J e. Top , J , { (/) } ) | ( if ( A e. ~P U. if ( J e. Top , J , { (/) } ) , A , (/) ) e. x /\ A. y e. x { ( U. if ( J e. Top , J , { (/) } ) \ y ) , ( ( cls ` if ( J e. Top , J , { (/) } ) ) ` y ) } C_ x ) } e. Fin /\ ( # ` |^| { x e. ~P ~P U. if ( J e. Top , J , { (/) } ) | ( if ( A e. ~P U. if ( J e. Top , J , { (/) } ) , A , (/) ) e. x /\ A. y e. x { ( U. if ( J e. Top , J , { (/) } ) \ y ) , ( ( cls ` if ( J e. Top , J , { (/) } ) ) ` y ) } C_ x ) } ) <_ ; 1 4 )
48 12 39 47 dedth2h 
 |-  ( ( A C_ X /\ J e. Top ) -> ( S e. Fin /\ ( # ` S ) <_ ; 1 4 ) )
49 48 ancoms 
 |-  ( ( J e. Top /\ A C_ X ) -> ( S e. Fin /\ ( # ` S ) <_ ; 1 4 ) )