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 ⁡ A = A

Proof

Step Hyp Ref Expression
1 elsni ⊢ x ∈ A → x = A
2 elsni ⊢ y ∈ A → y = A
3 1 2 ineqan12d ⊢ x ∈ A ∧ y ∈ A → x ∩ y = A ∩ A
4 inidm ⊢ A ∩ A = A
5 3 4 eqtrdi ⊢ x ∈ A ∧ y ∈ A → x ∩ y = A
6 vex ⊢ x ∈ V
7 6 inex1 ⊢ x ∩ y ∈ V
8 7 elsn ⊢ x ∩ y ∈ A ↔ x ∩ y = A
9 5 8 sylibr ⊢ x ∈ A ∧ y ∈ A → x ∩ y ∈ A
10 9 rgen2 ⊢ ∀ x ∈ A ∀ y ∈ A x ∩ y ∈ A
11 snex ⊢ A ∈ V
12 inficl ⊢ A ∈ V → ∀ x ∈ A ∀ y ∈ A x ∩ y ∈ A ↔ fi ⁡ A = A
13 11 12 ax-mp ⊢ ∀ x ∈ A ∀ y ∈ A x ∩ y ∈ A ↔ fi ⁡ A = A
14 10 13 mpbi ⊢ fi ⁡ A = A