Metamath Proof Explorer

Theorem fiin

Description: The elements of ( fiC ) are closed under finite intersection. (Contributed by Mario Carneiro, 24-Nov-2013)

Ref Expression
Assertion fiin ⊢A∈fi⁡C∧B∈fi⁡C→A∩B∈fi⁡C

Proof

Step Hyp Ref Expression
1 elfvex ⊢A∈fi⁡C→C∈V
2 elfi ⊢A∈fi⁡C∧C∈V→A∈fi⁡C↔∃x∈𝒫C∩FinA=⋂x
3 1 2 mpdan ⊢A∈fi⁡C→A∈fi⁡C↔∃x∈𝒫C∩FinA=⋂x
4 3 ibi ⊢A∈fi⁡C→∃x∈𝒫C∩FinA=⋂x
5 4 adantr ⊢A∈fi⁡C∧B∈fi⁡C→∃x∈𝒫C∩FinA=⋂x
6 simpr ⊢A∈fi⁡C∧B∈fi⁡C→B∈fi⁡C
7 elfi ⊢B∈fi⁡C∧C∈V→B∈fi⁡C↔∃y∈𝒫C∩FinB=⋂y
8 7 ancoms ⊢C∈V∧B∈fi⁡C→B∈fi⁡C↔∃y∈𝒫C∩FinB=⋂y
9 1 8 sylan ⊢A∈fi⁡C∧B∈fi⁡C→B∈fi⁡C↔∃y∈𝒫C∩FinB=⋂y
10 6 9 mpbid ⊢A∈fi⁡C∧B∈fi⁡C→∃y∈𝒫C∩FinB=⋂y
11 elin ⊢x∈𝒫C∩Fin↔x∈𝒫C∧x∈Fin
12 elin ⊢y∈𝒫C∩Fin↔y∈𝒫C∧y∈Fin
13 pwuncl ⊢x∈𝒫C∧y∈𝒫C→x∪y∈𝒫C
14 unfi ⊢x∈Fin∧y∈Fin→x∪y∈Fin
15 13 14 anim12i ⊢x∈𝒫C∧y∈𝒫C∧x∈Fin∧y∈Fin→x∪y∈𝒫C∧x∪y∈Fin
16 15 an4s ⊢x∈𝒫C∧x∈Fin∧y∈𝒫C∧y∈Fin→x∪y∈𝒫C∧x∪y∈Fin
17 11 12 16 syl2anb ⊢x∈𝒫C∩Fin∧y∈𝒫C∩Fin→x∪y∈𝒫C∧x∪y∈Fin
18 elin ⊢x∪y∈𝒫C∩Fin↔x∪y∈𝒫C∧x∪y∈Fin
19 17 18 sylibr ⊢x∈𝒫C∩Fin∧y∈𝒫C∩Fin→x∪y∈𝒫C∩Fin
20 ineq12 ⊢A=⋂x∧B=⋂y→A∩B=⋂x∩⋂y
21 intun ⊢⋂x∪y=⋂x∩⋂y
22 20 21 eqtr4di ⊢A=⋂x∧B=⋂y→A∩B=⋂x∪y
23 inteq ⊢z=x∪y→⋂z=⋂x∪y
24 23 rspceeqv ⊢x∪y∈𝒫C∩Fin∧A∩B=⋂x∪y→∃z∈𝒫C∩FinA∩B=⋂z
25 19 22 24 syl2an ⊢x∈𝒫C∩Fin∧y∈𝒫C∩Fin∧A=⋂x∧B=⋂y→∃z∈𝒫C∩FinA∩B=⋂z
26 25 an4s ⊢x∈𝒫C∩Fin∧A=⋂x∧y∈𝒫C∩Fin∧B=⋂y→∃z∈𝒫C∩FinA∩B=⋂z
27 26 rexlimdvaa ⊢x∈𝒫C∩Fin∧A=⋂x→∃y∈𝒫C∩FinB=⋂y→∃z∈𝒫C∩FinA∩B=⋂z
28 27 rexlimiva ⊢∃x∈𝒫C∩FinA=⋂x→∃y∈𝒫C∩FinB=⋂y→∃z∈𝒫C∩FinA∩B=⋂z
29 5 10 28 sylc ⊢A∈fi⁡C∧B∈fi⁡C→∃z∈𝒫C∩FinA∩B=⋂z
30 inex1g ⊢A∈fi⁡C→A∩B∈V
31 elfi ⊢A∩B∈V∧C∈V→A∩B∈fi⁡C↔∃z∈𝒫C∩FinA∩B=⋂z
32 30 1 31 syl2anc ⊢A∈fi⁡C→A∩B∈fi⁡C↔∃z∈𝒫C∩FinA∩B=⋂z
33 32 adantr ⊢A∈fi⁡C∧B∈fi⁡C→A∩B∈fi⁡C↔∃z∈𝒫C∩FinA∩B=⋂z
34 29 33 mpbird ⊢A∈fi⁡C∧B∈fi⁡C→A∩B∈fi⁡C