Theorem kur14lem10

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

	Ref	Expression
Hypotheses	kur14lem10.j	⊢ 𝐽 ∈ Top
	kur14lem10.x	⊢ 𝑋 = ∪ 𝐽
	kur14lem10.k	⊢ 𝐾 = ( cls ‘ 𝐽 )
	kur14lem10.s	⊢ 𝑆 = ∩ { 𝑥 ∈ 𝒫 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 { ( 𝑋 ∖ 𝑦 ) , ( 𝐾 ‘ 𝑦 ) } ⊆ 𝑥 ) }
	kur14lem10.a	⊢ 𝐴 ⊆ 𝑋
Assertion	kur14lem10	⊢ ( 𝑆 ∈ Fin ∧ ( ♯ ‘ 𝑆 ) ≤ ; 1 4 )

Proof

Step	Hyp	Ref	Expression
1		kur14lem10.j	⊢ 𝐽 ∈ Top
2		kur14lem10.x	⊢ 𝑋 = ∪ 𝐽
3		kur14lem10.k	⊢ 𝐾 = ( cls ‘ 𝐽 )
4		kur14lem10.s	⊢ 𝑆 = ∩ { 𝑥 ∈ 𝒫 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 { ( 𝑋 ∖ 𝑦 ) , ( 𝐾 ‘ 𝑦 ) } ⊆ 𝑥 ) }
5		kur14lem10.a	⊢ 𝐴 ⊆ 𝑋
6		eqid	⊢ ( int ‘ 𝐽 ) = ( int ‘ 𝐽 )
7		eqid	⊢ ( 𝑋 ∖ ( 𝐾 ‘ 𝐴 ) ) = ( 𝑋 ∖ ( 𝐾 ‘ 𝐴 ) )
8		eqid	⊢ ( 𝐾 ‘ ( 𝑋 ∖ 𝐴 ) ) = ( 𝐾 ‘ ( 𝑋 ∖ 𝐴 ) )
9		eqid	⊢ ( ( int ‘ 𝐽 ) ‘ ( 𝐾 ‘ 𝐴 ) ) = ( ( int ‘ 𝐽 ) ‘ ( 𝐾 ‘ 𝐴 ) )
10		eqid	⊢ ( ( ( { 𝐴 , ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) } ∪ { ( 𝑋 ∖ ( 𝐾 ‘ 𝐴 ) ) , ( 𝐾 ‘ ( 𝑋 ∖ 𝐴 ) ) , ( ( int ‘ 𝐽 ) ‘ 𝐴 ) } ) ∪ { ( 𝐾 ‘ ( 𝑋 ∖ ( 𝐾 ‘ 𝐴 ) ) ) , ( ( int ‘ 𝐽 ) ‘ ( 𝐾 ‘ 𝐴 ) ) , ( 𝐾 ‘ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) } ) ∪ ( { ( ( int ‘ 𝐽 ) ‘ ( 𝐾 ‘ ( 𝑋 ∖ 𝐴 ) ) ) , ( 𝐾 ‘ ( ( int ‘ 𝐽 ) ‘ ( 𝐾 ‘ 𝐴 ) ) ) , ( ( int ‘ 𝐽 ) ‘ ( 𝐾 ‘ ( 𝑋 ∖ ( 𝐾 ‘ 𝐴 ) ) ) ) } ∪ { ( 𝐾 ‘ ( ( int ‘ 𝐽 ) ‘ ( 𝐾 ‘ ( 𝑋 ∖ 𝐴 ) ) ) ) , ( ( int ‘ 𝐽 ) ‘ ( 𝐾 ‘ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) } ) ) = ( ( ( { 𝐴 , ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) } ∪ { ( 𝑋 ∖ ( 𝐾 ‘ 𝐴 ) ) , ( 𝐾 ‘ ( 𝑋 ∖ 𝐴 ) ) , ( ( int ‘ 𝐽 ) ‘ 𝐴 ) } ) ∪ { ( 𝐾 ‘ ( 𝑋 ∖ ( 𝐾 ‘ 𝐴 ) ) ) , ( ( int ‘ 𝐽 ) ‘ ( 𝐾 ‘ 𝐴 ) ) , ( 𝐾 ‘ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) } ) ∪ ( { ( ( int ‘ 𝐽 ) ‘ ( 𝐾 ‘ ( 𝑋 ∖ 𝐴 ) ) ) , ( 𝐾 ‘ ( ( int ‘ 𝐽 ) ‘ ( 𝐾 ‘ 𝐴 ) ) ) , ( ( int ‘ 𝐽 ) ‘ ( 𝐾 ‘ ( 𝑋 ∖ ( 𝐾 ‘ 𝐴 ) ) ) ) } ∪ { ( 𝐾 ‘ ( ( int ‘ 𝐽 ) ‘ ( 𝐾 ‘ ( 𝑋 ∖ 𝐴 ) ) ) ) , ( ( int ‘ 𝐽 ) ‘ ( 𝐾 ‘ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) } ) )
11	1 2 3 6 5 7 8 9 10 4	kur14lem9	⊢ ( 𝑆 ∈ Fin ∧ ( ♯ ‘ 𝑆 ) ≤ ; 1 4 )