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∈Ax∩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∈zx∩y∈z↔A⊆z∧∀x∈z∀y∈zx∩y∈z
4 eleq2 ⊢z=A→x∩y∈z↔x∩y∈A
5 4 raleqbi1dv ⊢z=A→∀y∈zx∩y∈z↔∀y∈Ax∩y∈A
6 5 raleqbi1dv ⊢z=A→∀x∈z∀y∈zx∩y∈z↔∀x∈A∀y∈Ax∩y∈A
7 3 6 bitr3d ⊢z=A→A⊆z∧∀x∈z∀y∈zx∩y∈z↔∀x∈A∀y∈Ax∩y∈A
8 7 elabg ⊢A∈V→A∈z|A⊆z∧∀x∈z∀y∈zx∩y∈z↔∀x∈A∀y∈Ax∩y∈A
9 intss1 ⊢A∈z|A⊆z∧∀x∈z∀y∈zx∩y∈z→⋂z|A⊆z∧∀x∈z∀y∈zx∩y∈z⊆A
10 8 9 syl6bir ⊢A∈V→∀x∈A∀y∈Ax∩y∈A→⋂z|A⊆z∧∀x∈z∀y∈zx∩y∈z⊆A
11 dffi2 ⊢A∈V→fi⁡A=⋂z|A⊆z∧∀x∈z∀y∈zx∩y∈z
12 11 sseq1d ⊢A∈V→fi⁡A⊆A↔⋂z|A⊆z∧∀x∈z∀y∈zx∩y∈z⊆A
13 10 12 sylibrd ⊢A∈V→∀x∈A∀y∈Ax∩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∈Ax∩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⁡Ax∩y∈fi⁡A
19 eleq2 ⊢fi⁡A=A→x∩y∈fi⁡A↔x∩y∈A
20 19 raleqbi1dv ⊢fi⁡A=A→∀y∈fi⁡Ax∩y∈fi⁡A↔∀y∈Ax∩y∈A
21 20 raleqbi1dv ⊢fi⁡A=A→∀x∈fi⁡A∀y∈fi⁡Ax∩y∈fi⁡A↔∀x∈A∀y∈Ax∩y∈A
22 18 21 mpbii ⊢fi⁡A=A→∀x∈A∀y∈Ax∩y∈A
23 16 22 impbid1 ⊢A∈V→∀x∈A∀y∈Ax∩y∈A↔fi⁡A=A