Metamath Proof Explorer


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 eqtrdi ( ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ) → ( 𝑥𝑦 ) = 𝐴 )
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 ‘ { 𝐴 } ) = { 𝐴 }