This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ { 𝐴 } ) = { 𝐴 }