Metamath Proof Explorer

Theorem inficl

Description: A set which is closed under pairwise intersection is closed under finite intersection. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 24-Nov-2013)

Ref Expression
Assertion inficl ⊢ A ∈ V → ∀ x ∈ A ∀ y ∈ A x ∩ y ∈ A ↔ fi ⁡ A = A

Proof

Step Hyp Ref Expression
1 ssfii ⊢ A ∈ V → A ⊆ fi ⁡ A
2 eqimss2 ⊢ z = A → A ⊆ z
3 2 biantrurd ⊢ z = A → ∀ x ∈ z ∀ y ∈ z x ∩ y ∈ z ↔ A ⊆ z ∧ ∀ x ∈ z ∀ y ∈ z x ∩ y ∈ z
4 eleq2 ⊢ z = A → x ∩ y ∈ z ↔ x ∩ y ∈ A
5 4 raleqbi1dv ⊢ z = A → ∀ y ∈ z x ∩ y ∈ z ↔ ∀ y ∈ A x ∩ y ∈ A
6 5 raleqbi1dv ⊢ z = A → ∀ x ∈ z ∀ y ∈ z x ∩ y ∈ z ↔ ∀ x ∈ A ∀ y ∈ A x ∩ y ∈ A
7 3 6 bitr3d ⊢ z = A → A ⊆ z ∧ ∀ x ∈ z ∀ y ∈ z x ∩ y ∈ z ↔ ∀ x ∈ A ∀ y ∈ A x ∩ y ∈ A
8 7 elabg ⊢ A ∈ V → A ∈ z | A ⊆ z ∧ ∀ x ∈ z ∀ y ∈ z x ∩ y ∈ z ↔ ∀ x ∈ A ∀ y ∈ A x ∩ y ∈ A
9 intss1 ⊢ A ∈ z | A ⊆ z ∧ ∀ x ∈ z ∀ y ∈ z x ∩ y ∈ z → ⋂ z | A ⊆ z ∧ ∀ x ∈ z ∀ y ∈ z x ∩ y ∈ z ⊆ A
10 8 9 syl6bir ⊢ A ∈ V → ∀ x ∈ A ∀ y ∈ A x ∩ y ∈ A → ⋂ z | A ⊆ z ∧ ∀ x ∈ z ∀ y ∈ z x ∩ y ∈ z ⊆ A
11 dffi2 ⊢ A ∈ V → fi ⁡ A = ⋂ z | A ⊆ z ∧ ∀ x ∈ z ∀ y ∈ z x ∩ y ∈ z
12 11 sseq1d ⊢ A ∈ V → fi ⁡ A ⊆ A ↔ ⋂ z | A ⊆ z ∧ ∀ x ∈ z ∀ y ∈ z x ∩ y ∈ z ⊆ A
13 10 12 sylibrd ⊢ A ∈ V → ∀ x ∈ A ∀ y ∈ A x ∩ y ∈ A → fi ⁡ A ⊆ A
14 eqss ⊢ fi ⁡ A = A ↔ fi ⁡ A ⊆ A ∧ A ⊆ fi ⁡ A
15 14 simplbi2com ⊢ A ⊆ fi ⁡ A → fi ⁡ A ⊆ A → fi ⁡ A = A
16 1 13 15 sylsyld ⊢ A ∈ V → ∀ x ∈ A ∀ y ∈ A x ∩ y ∈ A → fi ⁡ A = A
17 fiin ⊢ x ∈ fi ⁡ A ∧ y ∈ fi ⁡ A → x ∩ y ∈ fi ⁡ A
18 17 rgen2 ⊢ ∀ x ∈ fi ⁡ A ∀ y ∈ fi ⁡ A x ∩ y ∈ fi ⁡ A
19 eleq2 ⊢ fi ⁡ A = A → x ∩ y ∈ fi ⁡ A ↔ x ∩ y ∈ A
20 19 raleqbi1dv ⊢ fi ⁡ A = A → ∀ y ∈ fi ⁡ A x ∩ y ∈ fi ⁡ A ↔ ∀ y ∈ A x ∩ y ∈ A
21 20 raleqbi1dv ⊢ fi ⁡ A = A → ∀ x ∈ fi ⁡ A ∀ y ∈ fi ⁡ A x ∩ y ∈ fi ⁡ A ↔ ∀ x ∈ A ∀ y ∈ A x ∩ y ∈ A
22 18 21 mpbii ⊢ fi ⁡ A = A → ∀ x ∈ A ∀ y ∈ A x ∩ y ∈ A
23 16 22 impbid1 ⊢ A ∈ V → ∀ x ∈ A ∀ y ∈ A x ∩ y ∈ A ↔ fi ⁡ A = A