Theorem kur14lem10

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

	Ref	Expression
Hypotheses	kur14lem10.j	|- J e. Top
	kur14lem10.x	|- X = U. J
	kur14lem10.k	|- K = ( cls ` J )
	kur14lem10.s	|- S = |^| { x e. ~P ~P X | ( A e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) }
	kur14lem10.a	|- A C_ X
Assertion	kur14lem10	|- ( S e. Fin /\ ( # ` S ) <_ ; 1 4 )

Proof

Step	Hyp	Ref	Expression
1		kur14lem10.j	|- J e. Top
2		kur14lem10.x	|- X = U. J
3		kur14lem10.k	|- K = ( cls ` J )
4		kur14lem10.s	|- S = |^| { x e. ~P ~P X | ( A e. x /\ A. y e. x { ( X \ y ) , ( K ` y ) } C_ x ) }
5		kur14lem10.a	|- A C_ 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 ) } u. { ( X \ ( K ` A ) ) , ( K ` ( X \ A ) ) , ( ( int ` J ) ` A ) } ) u. { ( K ` ( X \ ( K ` A ) ) ) , ( ( int ` J ) ` ( K ` A ) ) , ( K ` ( ( int ` J ) ` A ) ) } ) u. ( { ( ( int ` J ) ` ( K ` ( X \ A ) ) ) , ( K ` ( ( int ` J ) ` ( K ` A ) ) ) , ( ( int ` J ) ` ( K ` ( X \ ( K ` A ) ) ) ) } u. { ( K ` ( ( int ` J ) ` ( K ` ( X \ A ) ) ) ) , ( ( int ` J ) ` ( K ` ( ( int ` J ) ` A ) ) ) } ) ) = ( ( ( { A , ( X \ A ) , ( K ` A ) } u. { ( X \ ( K ` A ) ) , ( K ` ( X \ A ) ) , ( ( int ` J ) ` A ) } ) u. { ( K ` ( X \ ( K ` A ) ) ) , ( ( int ` J ) ` ( K ` A ) ) , ( K ` ( ( int ` J ) ` A ) ) } ) u. ( { ( ( int ` J ) ` ( K ` ( X \ A ) ) ) , ( K ` ( ( int ` J ) ` ( K ` A ) ) ) , ( ( int ` J ) ` ( K ` ( X \ ( K ` A ) ) ) ) } u. { ( 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 e. Fin /\ ( # ` S ) <_ ; 1 4 )