Theorem kur14lem4

Description: Lemma for kur14 . Complementation is an involution on the set of subsets of a topology. (Contributed by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Hypotheses	kur14lem.j	⊢ 𝐽 ∈ Top
	kur14lem.x	⊢ 𝑋 = ∪ 𝐽
	kur14lem.k	⊢ 𝐾 = ( cls ‘ 𝐽 )
	kur14lem.i	⊢ 𝐼 = ( int ‘ 𝐽 )
	kur14lem.a	⊢ 𝐴 ⊆ 𝑋
Assertion	kur14lem4	⊢ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) = 𝐴

Proof

Step	Hyp	Ref	Expression
1		kur14lem.j	⊢ 𝐽 ∈ Top
2		kur14lem.x	⊢ 𝑋 = ∪ 𝐽
3		kur14lem.k	⊢ 𝐾 = ( cls ‘ 𝐽 )
4		kur14lem.i	⊢ 𝐼 = ( int ‘ 𝐽 )
5		kur14lem.a	⊢ 𝐴 ⊆ 𝑋
6		dfss4	⊢ ( 𝐴 ⊆ 𝑋 ↔ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) = 𝐴 )
7	5 6	mpbi	⊢ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) = 𝐴