Theorem kur14lem8

Description: Lemma for kur14 . Show that the set T contains at most 1 4 elements. (It could be less if some of the operators take the same value for a given set, but Kuratowski showed that this upper bound of 1 4 is tight in the sense that there exist topological spaces and subsets of these spaces for which all 1 4 generated sets are distinct, and indeed the real numbers form such a topological space.) (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 ) ) ) } ) )
Assertion	kur14lem8	|- ( T e. Fin /\ ( # ` T ) <_ ; 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		eqid	|- ( ( { A , ( X \ A ) , ( K ` A ) } u. { B , C , ( I ` A ) } ) u. { ( K ` B ) , D , ( K ` ( I ` A ) ) } ) = ( ( { A , ( X \ A ) , ( K ` A ) } u. { B , C , ( I ` A ) } ) u. { ( K ` B ) , D , ( K ` ( I ` A ) ) } )
11		eqid	|- ( { A , ( X \ A ) , ( K ` A ) } u. { B , C , ( I ` A ) } ) = ( { A , ( X \ A ) , ( K ` A ) } u. { B , C , ( I ` A ) } )
12		hashtplei	|- ( { A , ( X \ A ) , ( K ` A ) } e. Fin /\ ( # ` { A , ( X \ A ) , ( K ` A ) } ) <_ 3 )
13		hashtplei	|- ( { B , C , ( I ` A ) } e. Fin /\ ( # ` { B , C , ( I ` A ) } ) <_ 3 )
14		3nn0	|- 3 e. NN0
15		3p3e6	|- ( 3 + 3 ) = 6
16	11 12 13 14 14 15	hashunlei	|- ( ( { A , ( X \ A ) , ( K ` A ) } u. { B , C , ( I ` A ) } ) e. Fin /\ ( # ` ( { A , ( X \ A ) , ( K ` A ) } u. { B , C , ( I ` A ) } ) ) <_ 6 )
17		hashtplei	|- ( { ( K ` B ) , D , ( K ` ( I ` A ) ) } e. Fin /\ ( # ` { ( K ` B ) , D , ( K ` ( I ` A ) ) } ) <_ 3 )
18		6nn0	|- 6 e. NN0
19		6p3e9	|- ( 6 + 3 ) = 9
20	10 16 17 18 14 19	hashunlei	|- ( ( ( { A , ( X \ A ) , ( K ` A ) } u. { B , C , ( I ` A ) } ) u. { ( K ` B ) , D , ( K ` ( I ` A ) ) } ) e. Fin /\ ( # ` ( ( { A , ( X \ A ) , ( K ` A ) } u. { B , C , ( I ` A ) } ) u. { ( K ` B ) , D , ( K ` ( I ` A ) ) } ) ) <_ 9 )
21		eqid	|- ( { ( I ` C ) , ( K ` D ) , ( I ` ( K ` B ) ) } u. { ( K ` ( I ` C ) ) , ( I ` ( K ` ( I ` A ) ) ) } ) = ( { ( I ` C ) , ( K ` D ) , ( I ` ( K ` B ) ) } u. { ( K ` ( I ` C ) ) , ( I ` ( K ` ( I ` A ) ) ) } )
22		hashtplei	|- ( { ( I ` C ) , ( K ` D ) , ( I ` ( K ` B ) ) } e. Fin /\ ( # ` { ( I ` C ) , ( K ` D ) , ( I ` ( K ` B ) ) } ) <_ 3 )
23		hashprlei	|- ( { ( K ` ( I ` C ) ) , ( I ` ( K ` ( I ` A ) ) ) } e. Fin /\ ( # ` { ( K ` ( I ` C ) ) , ( I ` ( K ` ( I ` A ) ) ) } ) <_ 2 )
24		2nn0	|- 2 e. NN0
25		3p2e5	|- ( 3 + 2 ) = 5
26	21 22 23 14 24 25	hashunlei	|- ( ( { ( I ` C ) , ( K ` D ) , ( I ` ( K ` B ) ) } u. { ( K ` ( I ` C ) ) , ( I ` ( K ` ( I ` A ) ) ) } ) e. Fin /\ ( # ` ( { ( I ` C ) , ( K ` D ) , ( I ` ( K ` B ) ) } u. { ( K ` ( I ` C ) ) , ( I ` ( K ` ( I ` A ) ) ) } ) ) <_ 5 )
27		9nn0	|- 9 e. NN0
28		5nn0	|- 5 e. NN0
29		9p5e14	|- ( 9 + 5 ) = ; 1 4
30	9 20 26 27 28 29	hashunlei	|- ( T e. Fin /\ ( # ` T ) <_ ; 1 4 )