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 ⊢ 𝐽 ∈ Top
kur14lem.x ⊢ 𝑋 = ∪ 𝐽
kur14lem.k ⊢ 𝐾 = ( cls ‘ 𝐽 )
kur14lem.i ⊢ 𝐼 = ( int ‘ 𝐽 )
kur14lem.a ⊢ 𝐴 ⊆ 𝑋
kur14lem.b ⊢ 𝐵 = ( 𝑋 ∖ ( 𝐾 ‘ 𝐴 ) )
kur14lem.c ⊢ 𝐶 = ( 𝐾 ‘ ( 𝑋 ∖ 𝐴 ) )
kur14lem.d ⊢ 𝐷 = ( 𝐼 ‘ ( 𝐾 ‘ 𝐴 ) )
kur14lem.t ⊢ 𝑇 = ( ( ( { 𝐴 , ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) } ∪ { 𝐵 , 𝐶 , ( 𝐼 ‘ 𝐴 ) } ) ∪ { ( 𝐾 ‘ 𝐵 ) , 𝐷 , ( 𝐾 ‘ ( 𝐼 ‘ 𝐴 ) ) } ) ∪ ( { ( 𝐼 ‘ 𝐶 ) , ( 𝐾 ‘ 𝐷 ) , ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) } ∪ { ( 𝐾 ‘ ( 𝐼 ‘ 𝐶 ) ) , ( 𝐼 ‘ ( 𝐾 ‘ ( 𝐼 ‘ 𝐴 ) ) ) } ) )
kur14lem.s ⊢ 𝑆 = ∩ { 𝑥 ∈ 𝒫 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 { ( 𝑋 ∖ 𝑦 ) , ( 𝐾 ‘ 𝑦 ) } ⊆ 𝑥 ) }
Assertion kur14lem9 ( 𝑆 ∈ 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 kur14lem.s ⊢ 𝑆 = ∩ { 𝑥 ∈ 𝒫 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 { ( 𝑋 ∖ 𝑦 ) , ( 𝐾 ‘ 𝑦 ) } ⊆ 𝑥 ) }
11 vex ⊢ 𝑠 ∈ V
12 11 elintrab ⊢ ( 𝑠 ∈ ∩ { 𝑥 ∈ 𝒫 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 { ( 𝑋 ∖ 𝑦 ) , ( 𝐾 ‘ 𝑦 ) } ⊆ 𝑥 ) } ↔ ∀ 𝑥 ∈ 𝒫 𝒫 𝑋 ( ( 𝐴 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 { ( 𝑋 ∖ 𝑦 ) , ( 𝐾 ‘ 𝑦 ) } ⊆ 𝑥 ) → 𝑠 ∈ 𝑥 ) )
13 ssun1 ⊢ { 𝐴 , ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) } ⊆ ( { 𝐴 , ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) } ∪ { 𝐵 , 𝐶 , ( 𝐼 ‘ 𝐴 ) } )
14 ssun1 ⊢ ( { 𝐴 , ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) } ∪ { 𝐵 , 𝐶 , ( 𝐼 ‘ 𝐴 ) } ) ⊆ ( ( { 𝐴 , ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) } ∪ { 𝐵 , 𝐶 , ( 𝐼 ‘ 𝐴 ) } ) ∪ { ( 𝐾 ‘ 𝐵 ) , 𝐷 , ( 𝐾 ‘ ( 𝐼 ‘ 𝐴 ) ) } )
15 ssun1 ⊢ ( ( { 𝐴 , ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) } ∪ { 𝐵 , 𝐶 , ( 𝐼 ‘ 𝐴 ) } ) ∪ { ( 𝐾 ‘ 𝐵 ) , 𝐷 , ( 𝐾 ‘ ( 𝐼 ‘ 𝐴 ) ) } ) ⊆ ( ( ( { 𝐴 , ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) } ∪ { 𝐵 , 𝐶 , ( 𝐼 ‘ 𝐴 ) } ) ∪ { ( 𝐾 ‘ 𝐵 ) , 𝐷 , ( 𝐾 ‘ ( 𝐼 ‘ 𝐴 ) ) } ) ∪ ( { ( 𝐼 ‘ 𝐶 ) , ( 𝐾 ‘ 𝐷 ) , ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) } ∪ { ( 𝐾 ‘ ( 𝐼 ‘ 𝐶 ) ) , ( 𝐼 ‘ ( 𝐾 ‘ ( 𝐼 ‘ 𝐴 ) ) ) } ) )
16 15 9 sseqtrri ⊢ ( ( { 𝐴 , ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) } ∪ { 𝐵 , 𝐶 , ( 𝐼 ‘ 𝐴 ) } ) ∪ { ( 𝐾 ‘ 𝐵 ) , 𝐷 , ( 𝐾 ‘ ( 𝐼 ‘ 𝐴 ) ) } ) ⊆ 𝑇
17 14 16 sstri ⊢ ( { 𝐴 , ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) } ∪ { 𝐵 , 𝐶 , ( 𝐼 ‘ 𝐴 ) } ) ⊆ 𝑇
18 13 17 sstri ⊢ { 𝐴 , ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) } ⊆ 𝑇
19 2 topopn ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
20 1 19 ax-mp ⊢ 𝑋 ∈ 𝐽
21 20 elexi ⊢ 𝑋 ∈ V
22 21 5 ssexi ⊢ 𝐴 ∈ V
23 22 tpid1 ⊢ 𝐴 ∈ { 𝐴 , ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) }
24 18 23 sselii ⊢ 𝐴 ∈ 𝑇
25 1 2 3 4 5 6 7 8 9 kur14lem7 ⊢ ( 𝑦 ∈ 𝑇 → ( 𝑦 ⊆ 𝑋 ∧ { ( 𝑋 ∖ 𝑦 ) , ( 𝐾 ‘ 𝑦 ) } ⊆ 𝑇 ) )
26 25 simprd ⊢ ( 𝑦 ∈ 𝑇 → { ( 𝑋 ∖ 𝑦 ) , ( 𝐾 ‘ 𝑦 ) } ⊆ 𝑇 )
27 26 rgen ⊢ ∀ 𝑦 ∈ 𝑇 { ( 𝑋 ∖ 𝑦 ) , ( 𝐾 ‘ 𝑦 ) } ⊆ 𝑇
28 25 simpld ⊢ ( 𝑦 ∈ 𝑇 → 𝑦 ⊆ 𝑋 )
29 21 elpw2 ⊢ ( 𝑦 ∈ 𝒫 𝑋 ↔ 𝑦 ⊆ 𝑋 )
30 28 29 sylibr ⊢ ( 𝑦 ∈ 𝑇 → 𝑦 ∈ 𝒫 𝑋 )
31 30 ssriv ⊢ 𝑇 ⊆ 𝒫 𝑋
32 21 pwex ⊢ 𝒫 𝑋 ∈ V
33 32 elpw2 ⊢ ( 𝑇 ∈ 𝒫 𝒫 𝑋 ↔ 𝑇 ⊆ 𝒫 𝑋 )
34 31 33 mpbir ⊢ 𝑇 ∈ 𝒫 𝒫 𝑋
35 eleq2 ⊢ ( 𝑥 = 𝑇 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑇 ) )
36 sseq2 ⊢ ( 𝑥 = 𝑇 → ( { ( 𝑋 ∖ 𝑦 ) , ( 𝐾 ‘ 𝑦 ) } ⊆ 𝑥 ↔ { ( 𝑋 ∖ 𝑦 ) , ( 𝐾 ‘ 𝑦 ) } ⊆ 𝑇 ) )
37 36 raleqbi1dv ⊢ ( 𝑥 = 𝑇 → ( ∀ 𝑦 ∈ 𝑥 { ( 𝑋 ∖ 𝑦 ) , ( 𝐾 ‘ 𝑦 ) } ⊆ 𝑥 ↔ ∀ 𝑦 ∈ 𝑇 { ( 𝑋 ∖ 𝑦 ) , ( 𝐾 ‘ 𝑦 ) } ⊆ 𝑇 ) )
38 35 37 anbi12d ⊢ ( 𝑥 = 𝑇 → ( ( 𝐴 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 { ( 𝑋 ∖ 𝑦 ) , ( 𝐾 ‘ 𝑦 ) } ⊆ 𝑥 ) ↔ ( 𝐴 ∈ 𝑇 ∧ ∀ 𝑦 ∈ 𝑇 { ( 𝑋 ∖ 𝑦 ) , ( 𝐾 ‘ 𝑦 ) } ⊆ 𝑇 ) ) )
39 eleq2 ⊢ ( 𝑥 = 𝑇 → ( 𝑠 ∈ 𝑥 ↔ 𝑠 ∈ 𝑇 ) )
40 38 39 imbi12d ⊢ ( 𝑥 = 𝑇 → ( ( ( 𝐴 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 { ( 𝑋 ∖ 𝑦 ) , ( 𝐾 ‘ 𝑦 ) } ⊆ 𝑥 ) → 𝑠 ∈ 𝑥 ) ↔ ( ( 𝐴 ∈ 𝑇 ∧ ∀ 𝑦 ∈ 𝑇 { ( 𝑋 ∖ 𝑦 ) , ( 𝐾 ‘ 𝑦 ) } ⊆ 𝑇 ) → 𝑠 ∈ 𝑇 ) ) )
41 40 rspccv ⊢ ( ∀ 𝑥 ∈ 𝒫 𝒫 𝑋 ( ( 𝐴 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 { ( 𝑋 ∖ 𝑦 ) , ( 𝐾 ‘ 𝑦 ) } ⊆ 𝑥 ) → 𝑠 ∈ 𝑥 ) → ( 𝑇 ∈ 𝒫 𝒫 𝑋 → ( ( 𝐴 ∈ 𝑇 ∧ ∀ 𝑦 ∈ 𝑇 { ( 𝑋 ∖ 𝑦 ) , ( 𝐾 ‘ 𝑦 ) } ⊆ 𝑇 ) → 𝑠 ∈ 𝑇 ) ) )
42 34 41 mpi ⊢ ( ∀ 𝑥 ∈ 𝒫 𝒫 𝑋 ( ( 𝐴 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 { ( 𝑋 ∖ 𝑦 ) , ( 𝐾 ‘ 𝑦 ) } ⊆ 𝑥 ) → 𝑠 ∈ 𝑥 ) → ( ( 𝐴 ∈ 𝑇 ∧ ∀ 𝑦 ∈ 𝑇 { ( 𝑋 ∖ 𝑦 ) , ( 𝐾 ‘ 𝑦 ) } ⊆ 𝑇 ) → 𝑠 ∈ 𝑇 ) )
43 24 27 42 mp2ani ⊢ ( ∀ 𝑥 ∈ 𝒫 𝒫 𝑋 ( ( 𝐴 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 { ( 𝑋 ∖ 𝑦 ) , ( 𝐾 ‘ 𝑦 ) } ⊆ 𝑥 ) → 𝑠 ∈ 𝑥 ) → 𝑠 ∈ 𝑇 )
44 12 43 sylbi ⊢ ( 𝑠 ∈ ∩ { 𝑥 ∈ 𝒫 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 { ( 𝑋 ∖ 𝑦 ) , ( 𝐾 ‘ 𝑦 ) } ⊆ 𝑥 ) } → 𝑠 ∈ 𝑇 )
45 44 ssriv ⊢ ∩ { 𝑥 ∈ 𝒫 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 { ( 𝑋 ∖ 𝑦 ) , ( 𝐾 ‘ 𝑦 ) } ⊆ 𝑥 ) } ⊆ 𝑇
46 10 45 eqsstri ⊢ 𝑆 ⊆ 𝑇
47 1 2 3 4 5 6 7 8 9 kur14lem8 ⊢ ( 𝑇 ∈ Fin ∧ ( ♯ ‘ 𝑇 ) ≤ 1 4 )
48 1nn0 ⊢ 1 ∈ ℕ0
49 4nn0 ⊢ 4 ∈ ℕ0
50 48 49 deccl ⊢ 1 4 ∈ ℕ0
51 46 47 50 hashsslei ⊢ ( 𝑆 ∈ Fin ∧ ( ♯ ‘ 𝑆 ) ≤ 1 4 )