Theorem kur14lem1

Description: Lemma for kur14 . (Contributed by Mario Carneiro, 17-Feb-2015)

	Ref	Expression
Hypotheses	kur14lem1.a	|- A C_ X
	kur14lem1.c	|- ( X \ A ) e. T
	kur14lem1.k	|- ( K ` A ) e. T
Assertion	kur14lem1	|- ( N = A -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )

Proof

Step	Hyp	Ref	Expression
1		kur14lem1.a	|- A C_ X
2		kur14lem1.c	|- ( X \ A ) e. T
3		kur14lem1.k	|- ( K ` A ) e. T
4		sseq1	|- ( N = A -> ( N C_ X <-> A C_ X ) )
5	1 4	mpbiri	|- ( N = A -> N C_ X )
6		difeq2	|- ( N = A -> ( X \ N ) = ( X \ A ) )
7		fveq2	|- ( N = A -> ( K ` N ) = ( K ` A ) )
8	6 7	preq12d	|- ( N = A -> { ( X \ N ) , ( K ` N ) } = { ( X \ A ) , ( K ` A ) } )
9		prssi	|- ( ( ( X \ A ) e. T /\ ( K ` A ) e. T ) -> { ( X \ A ) , ( K ` A ) } C_ T )
10	2 3 9	mp2an	|- { ( X \ A ) , ( K ` A ) } C_ T
11	8 10	eqsstrdi	|- ( N = A -> { ( X \ N ) , ( K ` N ) } C_ T )
12	5 11	jca	|- ( N = A -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )