Theorem kur14lem1

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

	Ref	Expression
Hypotheses	kur14lem1.a	⊢ 𝐴 ⊆ 𝑋
	kur14lem1.c	⊢ ( 𝑋 ∖ 𝐴 ) ∈ 𝑇
	kur14lem1.k	⊢ ( 𝐾 ‘ 𝐴 ) ∈ 𝑇
Assertion	kur14lem1	⊢ ( 𝑁 = 𝐴 → ( 𝑁 ⊆ 𝑋 ∧ { ( 𝑋 ∖ 𝑁 ) , ( 𝐾 ‘ 𝑁 ) } ⊆ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		kur14lem1.a	⊢ 𝐴 ⊆ 𝑋
2		kur14lem1.c	⊢ ( 𝑋 ∖ 𝐴 ) ∈ 𝑇
3		kur14lem1.k	⊢ ( 𝐾 ‘ 𝐴 ) ∈ 𝑇
4		sseq1	⊢ ( 𝑁 = 𝐴 → ( 𝑁 ⊆ 𝑋 ↔ 𝐴 ⊆ 𝑋 ) )
5	1 4	mpbiri	⊢ ( 𝑁 = 𝐴 → 𝑁 ⊆ 𝑋 )
6		difeq2	⊢ ( 𝑁 = 𝐴 → ( 𝑋 ∖ 𝑁 ) = ( 𝑋 ∖ 𝐴 ) )
7		fveq2	⊢ ( 𝑁 = 𝐴 → ( 𝐾 ‘ 𝑁 ) = ( 𝐾 ‘ 𝐴 ) )
8	6 7	preq12d	⊢ ( 𝑁 = 𝐴 → { ( 𝑋 ∖ 𝑁 ) , ( 𝐾 ‘ 𝑁 ) } = { ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) } )
9		prssi	⊢ ( ( ( 𝑋 ∖ 𝐴 ) ∈ 𝑇 ∧ ( 𝐾 ‘ 𝐴 ) ∈ 𝑇 ) → { ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) } ⊆ 𝑇 )
10	2 3 9	mp2an	⊢ { ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) } ⊆ 𝑇
11	8 10	eqsstrdi	⊢ ( 𝑁 = 𝐴 → { ( 𝑋 ∖ 𝑁 ) , ( 𝐾 ‘ 𝑁 ) } ⊆ 𝑇 )
12	5 11	jca	⊢ ( 𝑁 = 𝐴 → ( 𝑁 ⊆ 𝑋 ∧ { ( 𝑋 ∖ 𝑁 ) , ( 𝐾 ‘ 𝑁 ) } ⊆ 𝑇 ) )