# Metamath Proof Explorer

## 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}↔{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)$