Metamath Proof Explorer

Theorem dffi2

Description: The set of finite intersections is the smallest set that contains A and is closed under pairwise intersection. (Contributed by Mario Carneiro, 24-Nov-2013)

Ref Expression
Assertion dffi2 ⊢A∈V→fi⁡A=⋂z|A⊆z∧∀x∈z∀y∈zx∩y∈z

Proof

Step Hyp Ref Expression
1 elex ⊢A∈V→A∈V
2 vex ⊢t∈V
3 elfi ⊢t∈V∧A∈V→t∈fi⁡A↔∃x∈𝒫A∩Fint=⋂x
4 2 3 mpan ⊢A∈V→t∈fi⁡A↔∃x∈𝒫A∩Fint=⋂x
5 4 biimpd ⊢A∈V→t∈fi⁡A→∃x∈𝒫A∩Fint=⋂x
6 df-rex ⊢∃x∈𝒫A∩Fint=⋂x↔∃xx∈𝒫A∩Fin∧t=⋂x
7 fiint ⊢∀x∈z∀y∈zx∩y∈z↔∀xx⊆z∧x≠∅∧x∈Fin→⋂x∈z
8 elinel1 ⊢x∈𝒫A∩Fin→x∈𝒫A
9 8 elpwid ⊢x∈𝒫A∩Fin→x⊆A
10 9 3ad2ant2 ⊢A⊆z∧x∈𝒫A∩Fin∧t=⋂x→x⊆A
11 simp1 ⊢A⊆z∧x∈𝒫A∩Fin∧t=⋂x→A⊆z
12 10 11 sstrd ⊢A⊆z∧x∈𝒫A∩Fin∧t=⋂x→x⊆z
13 eqvisset ⊢t=⋂x→⋂x∈V
14 intex ⊢x≠∅↔⋂x∈V
15 13 14 sylibr ⊢t=⋂x→x≠∅
16 15 3ad2ant3 ⊢A⊆z∧x∈𝒫A∩Fin∧t=⋂x→x≠∅
17 elinel2 ⊢x∈𝒫A∩Fin→x∈Fin
18 17 3ad2ant2 ⊢A⊆z∧x∈𝒫A∩Fin∧t=⋂x→x∈Fin
19 12 16 18 3jca ⊢A⊆z∧x∈𝒫A∩Fin∧t=⋂x→x⊆z∧x≠∅∧x∈Fin
20 19 3expib ⊢A⊆z→x∈𝒫A∩Fin∧t=⋂x→x⊆z∧x≠∅∧x∈Fin
21 pm2.27 ⊢x⊆z∧x≠∅∧x∈Fin→x⊆z∧x≠∅∧x∈Fin→⋂x∈z→⋂x∈z
22 20 21 syl6 ⊢A⊆z→x∈𝒫A∩Fin∧t=⋂x→x⊆z∧x≠∅∧x∈Fin→⋂x∈z→⋂x∈z
23 eleq1 ⊢t=⋂x→t∈z↔⋂x∈z
24 23 biimprd ⊢t=⋂x→⋂x∈z→t∈z
25 24 adantl ⊢x∈𝒫A∩Fin∧t=⋂x→⋂x∈z→t∈z
26 25 a1i ⊢A⊆z→x∈𝒫A∩Fin∧t=⋂x→⋂x∈z→t∈z
27 22 26 syldd ⊢A⊆z→x∈𝒫A∩Fin∧t=⋂x→x⊆z∧x≠∅∧x∈Fin→⋂x∈z→t∈z
28 27 com23 ⊢A⊆z→x⊆z∧x≠∅∧x∈Fin→⋂x∈z→x∈𝒫A∩Fin∧t=⋂x→t∈z
29 28 alimdv ⊢A⊆z→∀xx⊆z∧x≠∅∧x∈Fin→⋂x∈z→∀xx∈𝒫A∩Fin∧t=⋂x→t∈z
30 7 29 biimtrid ⊢A⊆z→∀x∈z∀y∈zx∩y∈z→∀xx∈𝒫A∩Fin∧t=⋂x→t∈z
31 30 imp ⊢A⊆z∧∀x∈z∀y∈zx∩y∈z→∀xx∈𝒫A∩Fin∧t=⋂x→t∈z
32 19.23v ⊢∀xx∈𝒫A∩Fin∧t=⋂x→t∈z↔∃xx∈𝒫A∩Fin∧t=⋂x→t∈z
33 31 32 sylib ⊢A⊆z∧∀x∈z∀y∈zx∩y∈z→∃xx∈𝒫A∩Fin∧t=⋂x→t∈z
34 6 33 biimtrid ⊢A⊆z∧∀x∈z∀y∈zx∩y∈z→∃x∈𝒫A∩Fint=⋂x→t∈z
35 5 34 sylan9 ⊢A∈V∧A⊆z∧∀x∈z∀y∈zx∩y∈z→t∈fi⁡A→t∈z
36 35 ssrdv ⊢A∈V∧A⊆z∧∀x∈z∀y∈zx∩y∈z→fi⁡A⊆z
37 36 ex ⊢A∈V→A⊆z∧∀x∈z∀y∈zx∩y∈z→fi⁡A⊆z
38 37 alrimiv ⊢A∈V→∀zA⊆z∧∀x∈z∀y∈zx∩y∈z→fi⁡A⊆z
39 ssintab ⊢fi⁡A⊆⋂z|A⊆z∧∀x∈z∀y∈zx∩y∈z↔∀zA⊆z∧∀x∈z∀y∈zx∩y∈z→fi⁡A⊆z
40 38 39 sylibr ⊢A∈V→fi⁡A⊆⋂z|A⊆z∧∀x∈z∀y∈zx∩y∈z
41 ssfii ⊢A∈V→A⊆fi⁡A
42 fiin ⊢x∈fi⁡A∧y∈fi⁡A→x∩y∈fi⁡A
43 42 rgen2 ⊢∀x∈fi⁡A∀y∈fi⁡Ax∩y∈fi⁡A
44 fvex ⊢fi⁡A∈V
45 sseq2 ⊢z=fi⁡A→A⊆z↔A⊆fi⁡A
46 eleq2 ⊢z=fi⁡A→x∩y∈z↔x∩y∈fi⁡A
47 46 raleqbi1dv ⊢z=fi⁡A→∀y∈zx∩y∈z↔∀y∈fi⁡Ax∩y∈fi⁡A
48 47 raleqbi1dv ⊢z=fi⁡A→∀x∈z∀y∈zx∩y∈z↔∀x∈fi⁡A∀y∈fi⁡Ax∩y∈fi⁡A
49 45 48 anbi12d ⊢z=fi⁡A→A⊆z∧∀x∈z∀y∈zx∩y∈z↔A⊆fi⁡A∧∀x∈fi⁡A∀y∈fi⁡Ax∩y∈fi⁡A
50 44 49 elab ⊢fi⁡A∈z|A⊆z∧∀x∈z∀y∈zx∩y∈z↔A⊆fi⁡A∧∀x∈fi⁡A∀y∈fi⁡Ax∩y∈fi⁡A
51 41 43 50 sylanblrc ⊢A∈V→fi⁡A∈z|A⊆z∧∀x∈z∀y∈zx∩y∈z
52 intss1 ⊢fi⁡A∈z|A⊆z∧∀x∈z∀y∈zx∩y∈z→⋂z|A⊆z∧∀x∈z∀y∈zx∩y∈z⊆fi⁡A
53 51 52 syl ⊢A∈V→⋂z|A⊆z∧∀x∈z∀y∈zx∩y∈z⊆fi⁡A
54 40 53 eqssd ⊢A∈V→fi⁡A=⋂z|A⊆z∧∀x∈z∀y∈zx∩y∈z
55 1 54 syl ⊢A∈V→fi⁡A=⋂z|A⊆z∧∀x∈z∀y∈zx∩y∈z