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 ∩ Fin A = ⋂ x
3 1 2 mpdan ⊢ A ∈ fi ⁡ C → A ∈ fi ⁡ C ↔ ∃ x ∈ 𝒫 C ∩ Fin A = ⋂ x
4 3 ibi ⊢ A ∈ fi ⁡ C → ∃ x ∈ 𝒫 C ∩ Fin A = ⋂ x
5 4 adantr ⊢ A ∈ fi ⁡ C ∧ B ∈ fi ⁡ C → ∃ x ∈ 𝒫 C ∩ Fin A = ⋂ x
6 simpr ⊢ A ∈ fi ⁡ C ∧ B ∈ fi ⁡ C → B ∈ fi ⁡ C
7 elfi ⊢ B ∈ fi ⁡ C ∧ C ∈ V → B ∈ fi ⁡ C ↔ ∃ y ∈ 𝒫 C ∩ Fin B = ⋂ y
8 7 ancoms ⊢ C ∈ V ∧ B ∈ fi ⁡ C → B ∈ fi ⁡ C ↔ ∃ y ∈ 𝒫 C ∩ Fin B = ⋂ y
9 1 8 sylan ⊢ A ∈ fi ⁡ C ∧ B ∈ fi ⁡ C → B ∈ fi ⁡ C ↔ ∃ y ∈ 𝒫 C ∩ Fin B = ⋂ y
10 6 9 mpbid ⊢ A ∈ fi ⁡ C ∧ B ∈ fi ⁡ C → ∃ y ∈ 𝒫 C ∩ Fin B = ⋂ 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 ∩ Fin A ∩ B = ⋂ z
25 19 22 24 syl2an ⊢ x ∈ 𝒫 C ∩ Fin ∧ y ∈ 𝒫 C ∩ Fin ∧ A = ⋂ x ∧ B = ⋂ y → ∃ z ∈ 𝒫 C ∩ Fin A ∩ B = ⋂ z
26 25 an4s ⊢ x ∈ 𝒫 C ∩ Fin ∧ A = ⋂ x ∧ y ∈ 𝒫 C ∩ Fin ∧ B = ⋂ y → ∃ z ∈ 𝒫 C ∩ Fin A ∩ B = ⋂ z
27 26 rexlimdvaa ⊢ x ∈ 𝒫 C ∩ Fin ∧ A = ⋂ x → ∃ y ∈ 𝒫 C ∩ Fin B = ⋂ y → ∃ z ∈ 𝒫 C ∩ Fin A ∩ B = ⋂ z
28 27 rexlimiva ⊢ ∃ x ∈ 𝒫 C ∩ Fin A = ⋂ x → ∃ y ∈ 𝒫 C ∩ Fin B = ⋂ y → ∃ z ∈ 𝒫 C ∩ Fin A ∩ B = ⋂ z
29 5 10 28 sylc ⊢ A ∈ fi ⁡ C ∧ B ∈ fi ⁡ C → ∃ z ∈ 𝒫 C ∩ Fin A ∩ B = ⋂ z
30 inex1g ⊢ A ∈ fi ⁡ C → A ∩ B ∈ V
31 elfi ⊢ A ∩ B ∈ V ∧ C ∈ V → A ∩ B ∈ fi ⁡ C ↔ ∃ z ∈ 𝒫 C ∩ Fin A ∩ B = ⋂ z
32 30 1 31 syl2anc ⊢ A ∈ fi ⁡ C → A ∩ B ∈ fi ⁡ C ↔ ∃ z ∈ 𝒫 C ∩ Fin A ∩ B = ⋂ z
33 32 adantr ⊢ A ∈ fi ⁡ C ∧ B ∈ fi ⁡ C → A ∩ B ∈ fi ⁡ C ↔ ∃ z ∈ 𝒫 C ∩ Fin A ∩ B = ⋂ z
34 29 33 mpbird ⊢ A ∈ fi ⁡ C ∧ B ∈ fi ⁡ C → A ∩ B ∈ fi ⁡ C