Metamath Proof Explorer

Theorem kur14lem9

Description: Lemma for kur14 . Since the set T is closed under closure and complement, it contains the minimal set S as a subset, so S also has at most 1 4 elements. (Indeed S = T , and it's not hard to prove this, but we don't need it for this proof.) (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypotheses kur14lem.j 
|- J e. Top
kur14lem.x 
|- X = U. J
kur14lem.k 
|- K = ( cls ` J )
kur14lem.i 
|- I = ( int ` J )
kur14lem.a 
|- A C_ X
kur14lem.b 
|- B = ( X \ ( K ` A ) )
kur14lem.c 
|- C = ( K ` ( X \ A ) )
kur14lem.d 
|- D = ( I ` ( K ` A ) )
kur14lem.t 
|- T = ( ( ( { A , ( X \ A ) , ( K ` A ) } u. { B , C , ( I ` A ) } ) u. { ( K ` B ) , D , ( K ` ( I ` A ) ) } ) u. ( { ( I ` C ) , ( K ` D ) , ( I ` ( K ` B ) ) } u. { ( K ` ( I ` C ) ) , ( I ` ( K ` ( I ` A ) ) ) } ) )
kur14lem.s 
|- S = |^| { x e. ~P ~P X | ( A e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) }
Assertion kur14lem9 
|- ( S e. Fin /\ ( # ` S ) <_ ; 1 4 )

Proof

Step Hyp Ref Expression
1 kur14lem.j 
 |-  J e. Top
2 kur14lem.x 
 |-  X = U. J
3 kur14lem.k 
 |-  K = ( cls ` J )
4 kur14lem.i 
 |-  I = ( int ` J )
5 kur14lem.a 
 |-  A C_ X
6 kur14lem.b 
 |-  B = ( X \ ( K ` A ) )
7 kur14lem.c 
 |-  C = ( K ` ( X \ A ) )
8 kur14lem.d 
 |-  D = ( I ` ( K ` A ) )
9 kur14lem.t 
 |-  T = ( ( ( { A , ( X \ A ) , ( K ` A ) } u. { B , C , ( I ` A ) } ) u. { ( K ` B ) , D , ( K ` ( I ` A ) ) } ) u. ( { ( I ` C ) , ( K ` D ) , ( I ` ( K ` B ) ) } u. { ( K ` ( I ` C ) ) , ( I ` ( K ` ( I ` A ) ) ) } ) )
10 kur14lem.s 
 |-  S = |^| { x e. ~P ~P X | ( A e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) }
11 vex 
 |-  s e. _V
12 11 elintrab 
 |-  ( s e. |^| { x e. ~P ~P X | ( A e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) } <-> A. x e. ~P ~P X ( ( A e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) -> s e. x ) )
13 ssun1 
 |-  { A , ( X \ A ) , ( K ` A ) } C_ ( { A , ( X \ A ) , ( K ` A ) } u. { B , C , ( I ` A ) } )
14 ssun1 
 |-  ( { A , ( X \ A ) , ( K ` A ) } u. { B , C , ( I ` A ) } ) C_ ( ( { A , ( X \ A ) , ( K ` A ) } u. { B , C , ( I ` A ) } ) u. { ( K ` B ) , D , ( K ` ( I ` A ) ) } )
15 ssun1 
 |-  ( ( { A , ( X \ A ) , ( K ` A ) } u. { B , C , ( I ` A ) } ) u. { ( K ` B ) , D , ( K ` ( I ` A ) ) } ) C_ ( ( ( { A , ( X \ A ) , ( K ` A ) } u. { B , C , ( I ` A ) } ) u. { ( K ` B ) , D , ( K ` ( I ` A ) ) } ) u. ( { ( I ` C ) , ( K ` D ) , ( I ` ( K ` B ) ) } u. { ( K ` ( I ` C ) ) , ( I ` ( K ` ( I ` A ) ) ) } ) )
16 15 9 sseqtrri 
 |-  ( ( { A , ( X \ A ) , ( K ` A ) } u. { B , C , ( I ` A ) } ) u. { ( K ` B ) , D , ( K ` ( I ` A ) ) } ) C_ T
17 14 16 sstri 
 |-  ( { A , ( X \ A ) , ( K ` A ) } u. { B , C , ( I ` A ) } ) C_ T
18 13 17 sstri 
 |-  { A , ( X \ A ) , ( K ` A ) } C_ T
19 2 topopn 
 |-  ( J e. Top -> X e. J )
20 1 19 ax-mp 
 |-  X e. J
21 20 elexi 
 |-  X e. _V
22 21 5 ssexi 
 |-  A e. _V
23 22 tpid1 
 |-  A e. { A , ( X \ A ) , ( K ` A ) }
24 18 23 sselii 
 |-  A e. T
25 1 2 3 4 5 6 7 8 9 kur14lem7 
 |-  ( y e. T -> ( y C_ X /\ { ( X \ y ) , ( K ` y ) } C_ T ) )
26 25 simprd 
 |-  ( y e. T -> { ( X \ y ) , ( K ` y ) } C_ T )
27 26 rgen 
 |-  A. y e. T { ( X \ y ) , ( K ` y ) } C_ T
28 25 simpld 
 |-  ( y e. T -> y C_ X )
29 21 elpw2 
 |-  ( y e. ~P X <-> y C_ X )
30 28 29 sylibr 
 |-  ( y e. T -> y e. ~P X )
31 30 ssriv 
 |-  T C_ ~P X
32 21 pwex 
 |-  ~P X e. _V
33 32 elpw2 
 |-  ( T e. ~P ~P X <-> T C_ ~P X )
34 31 33 mpbir 
 |-  T e. ~P ~P X
35 eleq2 
 |-  ( x = T -> ( A e. x <-> A e. T ) )
36 sseq2 
 |-  ( x = T -> ( { ( X \ y ) , ( K ` y ) } C_ x <-> { ( X \ y ) , ( K ` y ) } C_ T ) )
37 36 raleqbi1dv 
 |-  ( x = T -> ( A. y e. x { ( X \ y ) , ( K ` y ) } C_ x <-> A. y e. T { ( X \ y ) , ( K ` y ) } C_ T ) )
38 35 37 anbi12d 
 |-  ( x = T -> ( ( A e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) <-> ( A e. T /\ A. y e. T { ( X \ y ) , ( K ` y ) } C_ T ) ) )
39 eleq2 
 |-  ( x = T -> ( s e. x <-> s e. T ) )
40 38 39 imbi12d 
 |-  ( x = T -> ( ( ( A e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) -> s e. x ) <-> ( ( A e. T /\ A. y e. T { ( X \ y ) , ( K ` y ) } C_ T ) -> s e. T ) ) )
41 40 rspccv 
 |-  ( A. x e. ~P ~P X ( ( A e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) -> s e. x ) -> ( T e. ~P ~P X -> ( ( A e. T /\ A. y e. T { ( X \ y ) , ( K ` y ) } C_ T ) -> s e. T ) ) )
42 34 41 mpi 
 |-  ( A. x e. ~P ~P X ( ( A e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) -> s e. x ) -> ( ( A e. T /\ A. y e. T { ( X \ y ) , ( K ` y ) } C_ T ) -> s e. T ) )
43 24 27 42 mp2ani 
 |-  ( A. x e. ~P ~P X ( ( A e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) -> s e. x ) -> s e. T )
44 12 43 sylbi 
 |-  ( s e. |^| { x e. ~P ~P X | ( A e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) } -> s e. T )
45 44 ssriv 
 |-  |^| { x e. ~P ~P X | ( A e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) } C_ T
46 10 45 eqsstri 
 |-  S C_ T
47 1 2 3 4 5 6 7 8 9 kur14lem8 
 |-  ( T e. Fin /\ ( # ` T ) <_ ; 1 4 )
48 1nn0 
 |-  1 e. NN0
49 4nn0 
 |-  4 e. NN0
50 48 49 deccl 
 |-  ; 1 4 e. NN0
51 46 47 50 hashsslei 
 |-  ( S e. Fin /\ ( # ` S ) <_ ; 1 4 )