Theorem kur14lem1

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

	Ref	Expression
Hypotheses	kur14lem1.a	$$⊢A\subseteq X$$
	kur14lem1.c	$$⊢X\setminus A\in T$$
	kur14lem1.k	$$⊢K\left(A\right)\in T$$
Assertion	kur14lem1	$$⊢N=A\to \left(N\subseteq X\wedge \left\{X\setminus N,K\left(N\right)\right\}\subseteq T\right)$$

Proof

Step	Hyp	Ref	Expression
1		kur14lem1.a	$$⊢A\subseteq X$$
2		kur14lem1.c	$$⊢X\setminus A\in T$$
3		kur14lem1.k	$$⊢K\left(A\right)\in T$$
4		sseq1	$$⊢N=A\to \left(N\subseteq X\leftrightarrow A\subseteq X\right)$$
5	1 4	mpbiri	$$⊢N=A\to N\subseteq X$$
6		difeq2	$$⊢N=A\to X\setminus N=X\setminus A$$
7		fveq2	$$⊢N=A\to K\left(N\right)=K\left(A\right)$$
8	6 7	preq12d	$$⊢N=A\to \left\{X\setminus N,K\left(N\right)\right\}=\left\{X\setminus A,K\left(A\right)\right\}$$
9		prssi	$$⊢\left(X\setminus A\in T\wedge K\left(A\right)\in T\right)\to \left\{X\setminus A,K\left(A\right)\right\}\subseteq T$$
10	2 3 9	mp2an	$$⊢\left\{X\setminus A,K\left(A\right)\right\}\subseteq T$$
11	8 10	eqsstrdi	$$⊢N=A\to \left\{X\setminus N,K\left(N\right)\right\}\subseteq T$$
12	5 11	jca	$$⊢N=A\to \left(N\subseteq X\wedge \left\{X\setminus N,K\left(N\right)\right\}\subseteq T\right)$$