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	⊢ 𝐽 ∈ Top
	kur14lem.x	⊢ 𝑋 = ∪ 𝐽
	kur14lem.k	⊢ 𝐾 = ( cls ‘ 𝐽 )
	kur14lem.i	⊢ 𝐼 = ( int ‘ 𝐽 )
	kur14lem.a	⊢ 𝐴 ⊆ 𝑋
	kur14lem.b	⊢ 𝐵 = ( 𝑋 ∖ ( 𝐾 ‘ 𝐴 ) )
	kur14lem.c	⊢ 𝐶 = ( 𝐾 ‘ ( 𝑋 ∖ 𝐴 ) )
	kur14lem.d	⊢ 𝐷 = ( 𝐼 ‘ ( 𝐾 ‘ 𝐴 ) )
	kur14lem.t	⊢ 𝑇 = ( ( ( { 𝐴 , ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) } ∪ { 𝐵 , 𝐶 , ( 𝐼 ‘ 𝐴 ) } ) ∪ { ( 𝐾 ‘ 𝐵 ) , 𝐷 , ( 𝐾 ‘ ( 𝐼 ‘ 𝐴 ) ) } ) ∪ ( { ( 𝐼 ‘ 𝐶 ) , ( 𝐾 ‘ 𝐷 ) , ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) } ∪ { ( 𝐾 ‘ ( 𝐼 ‘ 𝐶 ) ) , ( 𝐼 ‘ ( 𝐾 ‘ ( 𝐼 ‘ 𝐴 ) ) ) } ) )
Assertion	kur14lem8	⊢ ( 𝑇 ∈ Fin ∧ ( ♯ ‘ 𝑇 ) ≤ ; 1 4 )

Proof

Step	Hyp	Ref	Expression
1		kur14lem.j	⊢ 𝐽 ∈ Top
2		kur14lem.x	⊢ 𝑋 = ∪ 𝐽
3		kur14lem.k	⊢ 𝐾 = ( cls ‘ 𝐽 )
4		kur14lem.i	⊢ 𝐼 = ( int ‘ 𝐽 )
5		kur14lem.a	⊢ 𝐴 ⊆ 𝑋
6		kur14lem.b	⊢ 𝐵 = ( 𝑋 ∖ ( 𝐾 ‘ 𝐴 ) )
7		kur14lem.c	⊢ 𝐶 = ( 𝐾 ‘ ( 𝑋 ∖ 𝐴 ) )
8		kur14lem.d	⊢ 𝐷 = ( 𝐼 ‘ ( 𝐾 ‘ 𝐴 ) )
9		kur14lem.t	⊢ 𝑇 = ( ( ( { 𝐴 , ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) } ∪ { 𝐵 , 𝐶 , ( 𝐼 ‘ 𝐴 ) } ) ∪ { ( 𝐾 ‘ 𝐵 ) , 𝐷 , ( 𝐾 ‘ ( 𝐼 ‘ 𝐴 ) ) } ) ∪ ( { ( 𝐼 ‘ 𝐶 ) , ( 𝐾 ‘ 𝐷 ) , ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) } ∪ { ( 𝐾 ‘ ( 𝐼 ‘ 𝐶 ) ) , ( 𝐼 ‘ ( 𝐾 ‘ ( 𝐼 ‘ 𝐴 ) ) ) } ) )
10		eqid	⊢ ( ( { 𝐴 , ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) } ∪ { 𝐵 , 𝐶 , ( 𝐼 ‘ 𝐴 ) } ) ∪ { ( 𝐾 ‘ 𝐵 ) , 𝐷 , ( 𝐾 ‘ ( 𝐼 ‘ 𝐴 ) ) } ) = ( ( { 𝐴 , ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) } ∪ { 𝐵 , 𝐶 , ( 𝐼 ‘ 𝐴 ) } ) ∪ { ( 𝐾 ‘ 𝐵 ) , 𝐷 , ( 𝐾 ‘ ( 𝐼 ‘ 𝐴 ) ) } )
11		eqid	⊢ ( { 𝐴 , ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) } ∪ { 𝐵 , 𝐶 , ( 𝐼 ‘ 𝐴 ) } ) = ( { 𝐴 , ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) } ∪ { 𝐵 , 𝐶 , ( 𝐼 ‘ 𝐴 ) } )
12		hashtplei	⊢ ( { 𝐴 , ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) } ∈ Fin ∧ ( ♯ ‘ { 𝐴 , ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) } ) ≤ 3 )
13		hashtplei	⊢ ( { 𝐵 , 𝐶 , ( 𝐼 ‘ 𝐴 ) } ∈ Fin ∧ ( ♯ ‘ { 𝐵 , 𝐶 , ( 𝐼 ‘ 𝐴 ) } ) ≤ 3 )
14		3nn0	⊢ 3 ∈ ℕ0
15		3p3e6	⊢ ( 3 + 3 ) = 6
16	11 12 13 14 14 15	hashunlei	⊢ ( ( { 𝐴 , ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) } ∪ { 𝐵 , 𝐶 , ( 𝐼 ‘ 𝐴 ) } ) ∈ Fin ∧ ( ♯ ‘ ( { 𝐴 , ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) } ∪ { 𝐵 , 𝐶 , ( 𝐼 ‘ 𝐴 ) } ) ) ≤ 6 )
17		hashtplei	⊢ ( { ( 𝐾 ‘ 𝐵 ) , 𝐷 , ( 𝐾 ‘ ( 𝐼 ‘ 𝐴 ) ) } ∈ Fin ∧ ( ♯ ‘ { ( 𝐾 ‘ 𝐵 ) , 𝐷 , ( 𝐾 ‘ ( 𝐼 ‘ 𝐴 ) ) } ) ≤ 3 )
18		6nn0	⊢ 6 ∈ ℕ0
19		6p3e9	⊢ ( 6 + 3 ) = 9
20	10 16 17 18 14 19	hashunlei	⊢ ( ( ( { 𝐴 , ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) } ∪ { 𝐵 , 𝐶 , ( 𝐼 ‘ 𝐴 ) } ) ∪ { ( 𝐾 ‘ 𝐵 ) , 𝐷 , ( 𝐾 ‘ ( 𝐼 ‘ 𝐴 ) ) } ) ∈ Fin ∧ ( ♯ ‘ ( ( { 𝐴 , ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) } ∪ { 𝐵 , 𝐶 , ( 𝐼 ‘ 𝐴 ) } ) ∪ { ( 𝐾 ‘ 𝐵 ) , 𝐷 , ( 𝐾 ‘ ( 𝐼 ‘ 𝐴 ) ) } ) ) ≤ 9 )
21		eqid	⊢ ( { ( 𝐼 ‘ 𝐶 ) , ( 𝐾 ‘ 𝐷 ) , ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) } ∪ { ( 𝐾 ‘ ( 𝐼 ‘ 𝐶 ) ) , ( 𝐼 ‘ ( 𝐾 ‘ ( 𝐼 ‘ 𝐴 ) ) ) } ) = ( { ( 𝐼 ‘ 𝐶 ) , ( 𝐾 ‘ 𝐷 ) , ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) } ∪ { ( 𝐾 ‘ ( 𝐼 ‘ 𝐶 ) ) , ( 𝐼 ‘ ( 𝐾 ‘ ( 𝐼 ‘ 𝐴 ) ) ) } )
22		hashtplei	⊢ ( { ( 𝐼 ‘ 𝐶 ) , ( 𝐾 ‘ 𝐷 ) , ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) } ∈ Fin ∧ ( ♯ ‘ { ( 𝐼 ‘ 𝐶 ) , ( 𝐾 ‘ 𝐷 ) , ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) } ) ≤ 3 )
23		hashprlei	⊢ ( { ( 𝐾 ‘ ( 𝐼 ‘ 𝐶 ) ) , ( 𝐼 ‘ ( 𝐾 ‘ ( 𝐼 ‘ 𝐴 ) ) ) } ∈ Fin ∧ ( ♯ ‘ { ( 𝐾 ‘ ( 𝐼 ‘ 𝐶 ) ) , ( 𝐼 ‘ ( 𝐾 ‘ ( 𝐼 ‘ 𝐴 ) ) ) } ) ≤ 2 )
24		2nn0	⊢ 2 ∈ ℕ0
25		3p2e5	⊢ ( 3 + 2 ) = 5
26	21 22 23 14 24 25	hashunlei	⊢ ( ( { ( 𝐼 ‘ 𝐶 ) , ( 𝐾 ‘ 𝐷 ) , ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) } ∪ { ( 𝐾 ‘ ( 𝐼 ‘ 𝐶 ) ) , ( 𝐼 ‘ ( 𝐾 ‘ ( 𝐼 ‘ 𝐴 ) ) ) } ) ∈ Fin ∧ ( ♯ ‘ ( { ( 𝐼 ‘ 𝐶 ) , ( 𝐾 ‘ 𝐷 ) , ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) } ∪ { ( 𝐾 ‘ ( 𝐼 ‘ 𝐶 ) ) , ( 𝐼 ‘ ( 𝐾 ‘ ( 𝐼 ‘ 𝐴 ) ) ) } ) ) ≤ 5 )
27		9nn0	⊢ 9 ∈ ℕ0
28		5nn0	⊢ 5 ∈ ℕ0
29		9p5e14	⊢ ( 9 + 5 ) = ; 1 4
30	9 20 26 27 28 29	hashunlei	⊢ ( 𝑇 ∈ Fin ∧ ( ♯ ‘ 𝑇 ) ≤ ; 1 4 )