Metamath Proof Explorer

Theorem kur14lem10

Description: Lemma for kur14 . Discharge the set T . (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypotheses kur14lem10.j ⊢ J ∈ Top
kur14lem10.x ⊢ X = ⋃ J
kur14lem10.k ⊢ K = cls ⁡ J
kur14lem10.s ⊢ S = ⋂ x ∈ 𝒫 𝒫 X | A ∈ x ∧ ∀ y ∈ x X ∖ y K ⁡ y ⊆ x
kur14lem10.a ⊢ A ⊆ X
Assertion kur14lem10 ⊢ S ∈ Fin ∧ S ≤ 14

Proof

Step Hyp Ref Expression
1 kur14lem10.j ⊢ J ∈ Top
2 kur14lem10.x ⊢ X = ⋃ J
3 kur14lem10.k ⊢ K = cls ⁡ J
4 kur14lem10.s ⊢ S = ⋂ x ∈ 𝒫 𝒫 X | A ∈ x ∧ ∀ y ∈ x X ∖ y K ⁡ y ⊆ x
5 kur14lem10.a ⊢ A ⊆ X
6 eqid ⊢ int ⁡ J = int ⁡ J
7 eqid ⊢ X ∖ K ⁡ A = X ∖ K ⁡ A
8 eqid ⊢ K ⁡ X ∖ A = K ⁡ X ∖ A
9 eqid ⊢ int ⁡ J ⁡ K ⁡ A = int ⁡ J ⁡ K ⁡ A
10 eqid ⊢ A X ∖ A K ⁡ A ∪ X ∖ K ⁡ A K ⁡ X ∖ A int ⁡ J ⁡ A ∪ K ⁡ X ∖ K ⁡ A int ⁡ J ⁡ K ⁡ A K ⁡ int ⁡ J ⁡ A ∪ int ⁡ J ⁡ K ⁡ X ∖ A K ⁡ int ⁡ J ⁡ K ⁡ A int ⁡ J ⁡ K ⁡ X ∖ K ⁡ A ∪ K ⁡ int ⁡ J ⁡ K ⁡ X ∖ A int ⁡ J ⁡ K ⁡ int ⁡ J ⁡ A = A X ∖ A K ⁡ A ∪ X ∖ K ⁡ A K ⁡ X ∖ A int ⁡ J ⁡ A ∪ K ⁡ X ∖ K ⁡ A int ⁡ J ⁡ K ⁡ A K ⁡ int ⁡ J ⁡ A ∪ int ⁡ J ⁡ K ⁡ X ∖ A K ⁡ int ⁡ J ⁡ K ⁡ A int ⁡ J ⁡ K ⁡ X ∖ K ⁡ A ∪ K ⁡ int ⁡ J ⁡ K ⁡ X ∖ A int ⁡ J ⁡ K ⁡ int ⁡ J ⁡ A
11 1 2 3 6 5 7 8 9 10 4 kur14lem9 ⊢ S ∈ Fin ∧ S ≤ 14