Theorem fisn

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

	Ref	Expression
Assertion	fisn	⊢ ( fi ‘ { 𝐴 } ) = { 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		elsni	⊢ ( 𝑥 ∈ { 𝐴 } → 𝑥 = 𝐴 )
2		elsni	⊢ ( 𝑦 ∈ { 𝐴 } → 𝑦 = 𝐴 )
3	1 2	ineqan12d	⊢ ( ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ) → ( 𝑥 ∩ 𝑦 ) = ( 𝐴 ∩ 𝐴 ) )
4		inidm	⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
5	3 4	syl6eq	⊢ ( ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ) → ( 𝑥 ∩ 𝑦 ) = 𝐴 )
6		vex	⊢ 𝑥 ∈ V
7	6	inex1	⊢ ( 𝑥 ∩ 𝑦 ) ∈ V
8	7	elsn	⊢ ( ( 𝑥 ∩ 𝑦 ) ∈ { 𝐴 } ↔ ( 𝑥 ∩ 𝑦 ) = 𝐴 )
9	5 8	sylibr	⊢ ( ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ) → ( 𝑥 ∩ 𝑦 ) ∈ { 𝐴 } )
10	9	rgen2	⊢ ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐴 } ( 𝑥 ∩ 𝑦 ) ∈ { 𝐴 }
11		snex	⊢ { 𝐴 } ∈ V
12		inficl	⊢ ( { 𝐴 } ∈ V → ( ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐴 } ( 𝑥 ∩ 𝑦 ) ∈ { 𝐴 } ↔ ( fi ‘ { 𝐴 } ) = { 𝐴 } ) )
13	11 12	ax-mp	⊢ ( ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐴 } ( 𝑥 ∩ 𝑦 ) ∈ { 𝐴 } ↔ ( fi ‘ { 𝐴 } ) = { 𝐴 } )
14	10 13	mpbi	⊢ ( fi ‘ { 𝐴 } ) = { 𝐴 }