Theorem indislem

Description: A lemma to eliminate some sethood hypotheses when dealing with the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Assertion	indislem	⊢ { ∅ , ( I ‘ 𝐴 ) } = { ∅ , 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		fvi	⊢ ( 𝐴 ∈ V → ( I ‘ 𝐴 ) = 𝐴 )
2	1	preq2d	⊢ ( 𝐴 ∈ V → { ∅ , ( I ‘ 𝐴 ) } = { ∅ , 𝐴 } )
3		dfsn2	⊢ { ∅ } = { ∅ , ∅ }
4	3	eqcomi	⊢ { ∅ , ∅ } = { ∅ }
5		fvprc	⊢ ( ¬ 𝐴 ∈ V → ( I ‘ 𝐴 ) = ∅ )
6	5	preq2d	⊢ ( ¬ 𝐴 ∈ V → { ∅ , ( I ‘ 𝐴 ) } = { ∅ , ∅ } )
7		prprc2	⊢ ( ¬ 𝐴 ∈ V → { ∅ , 𝐴 } = { ∅ } )
8	4 6 7	3eqtr4a	⊢ ( ¬ 𝐴 ∈ V → { ∅ , ( I ‘ 𝐴 ) } = { ∅ , 𝐴 } )
9	2 8	pm2.61i	⊢ { ∅ , ( I ‘ 𝐴 ) } = { ∅ , 𝐴 }