Theorem fisn

Description: A singleton is closed under finite intersections. (Contributed by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Assertion	fisn	$$⊢\mathrm{fi}\left(\left\{A\right\}\right)=\left\{A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		elsni	$$⊢x\in \left\{A\right\}\to x=A$$
2		elsni	$$⊢y\in \left\{A\right\}\to y=A$$
3	1 2	ineqan12d	$$⊢\left(x\in \left\{A\right\}\wedge y\in \left\{A\right\}\right)\to x\cap y=A\cap A$$
4		inidm	$$⊢A\cap A=A$$
5	3 4	eqtrdi	$$⊢\left(x\in \left\{A\right\}\wedge y\in \left\{A\right\}\right)\to x\cap y=A$$
6		vex	$$⊢x\in \mathrm{V}$$
7	6	inex1	$$⊢x\cap y\in \mathrm{V}$$
8	7	elsn	$$⊢x\cap y\in \left\{A\right\}\leftrightarrow x\cap y=A$$
9	5 8	sylibr	$$⊢\left(x\in \left\{A\right\}\wedge y\in \left\{A\right\}\right)\to x\cap y\in \left\{A\right\}$$
10	9	rgen2	$$⊢\forall x\in \left\{A\right\}\forall y\in \left\{A\right\}x\cap y\in \left\{A\right\}$$
11		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
12		inficl	$$⊢\left\{A\right\}\in \mathrm{V}\to \left(\forall x\in \left\{A\right\}\forall y\in \left\{A\right\}x\cap y\in \left\{A\right\}\leftrightarrow \mathrm{fi}\left(\left\{A\right\}\right)=\left\{A\right\}\right)$$
13	11 12	ax-mp	$$⊢\forall x\in \left\{A\right\}\forall y\in \left\{A\right\}x\cap y\in \left\{A\right\}\leftrightarrow \mathrm{fi}\left(\left\{A\right\}\right)=\left\{A\right\}$$
14	10 13	mpbi	$$⊢\mathrm{fi}\left(\left\{A\right\}\right)=\left\{A\right\}$$