Metamath Proof Explorer

Theorem elfi2

Description: The empty intersection need not be considered in the set of finite intersections. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion elfi2 ⊢ B ∈ V → A ∈ fi ⁡ B ↔ ∃ x ∈ 𝒫 B ∩ Fin ∖ ∅ A = ⋂ x

Proof

Step Hyp Ref Expression
1 elex ⊢ A ∈ fi ⁡ B → A ∈ V
2 1 a1i ⊢ B ∈ V → A ∈ fi ⁡ B → A ∈ V
3 simpr ⊢ x ∈ 𝒫 B ∩ Fin ∖ ∅ ∧ A = ⋂ x → A = ⋂ x
4 eldifsni ⊢ x ∈ 𝒫 B ∩ Fin ∖ ∅ → x ≠ ∅
5 4 adantr ⊢ x ∈ 𝒫 B ∩ Fin ∖ ∅ ∧ A = ⋂ x → x ≠ ∅
6 intex ⊢ x ≠ ∅ ↔ ⋂ x ∈ V
7 5 6 sylib ⊢ x ∈ 𝒫 B ∩ Fin ∖ ∅ ∧ A = ⋂ x → ⋂ x ∈ V
8 3 7 eqeltrd ⊢ x ∈ 𝒫 B ∩ Fin ∖ ∅ ∧ A = ⋂ x → A ∈ V
9 8 rexlimiva ⊢ ∃ x ∈ 𝒫 B ∩ Fin ∖ ∅ A = ⋂ x → A ∈ V
10 9 a1i ⊢ B ∈ V → ∃ x ∈ 𝒫 B ∩ Fin ∖ ∅ A = ⋂ x → A ∈ V
11 elfi ⊢ A ∈ V ∧ B ∈ V → A ∈ fi ⁡ B ↔ ∃ x ∈ 𝒫 B ∩ Fin A = ⋂ x
12 vprc ⊢ ¬ V ∈ V
13 elsni ⊢ x ∈ ∅ → x = ∅
14 13 inteqd ⊢ x ∈ ∅ → ⋂ x = ⋂ ∅
15 int0 ⊢ ⋂ ∅ = V
16 14 15 syl6eq ⊢ x ∈ ∅ → ⋂ x = V
17 16 eleq1d ⊢ x ∈ ∅ → ⋂ x ∈ V ↔ V ∈ V
18 12 17 mtbiri ⊢ x ∈ ∅ → ¬ ⋂ x ∈ V
19 simpr ⊢ A ∈ V ∧ B ∈ V ∧ A = ⋂ x → A = ⋂ x
20 simpll ⊢ A ∈ V ∧ B ∈ V ∧ A = ⋂ x → A ∈ V
21 19 20 eqeltrrd ⊢ A ∈ V ∧ B ∈ V ∧ A = ⋂ x → ⋂ x ∈ V
22 18 21 nsyl3 ⊢ A ∈ V ∧ B ∈ V ∧ A = ⋂ x → ¬ x ∈ ∅
23 22 biantrud ⊢ A ∈ V ∧ B ∈ V ∧ A = ⋂ x → x ∈ 𝒫 B ∩ Fin ↔ x ∈ 𝒫 B ∩ Fin ∧ ¬ x ∈ ∅
24 eldif ⊢ x ∈ 𝒫 B ∩ Fin ∖ ∅ ↔ x ∈ 𝒫 B ∩ Fin ∧ ¬ x ∈ ∅
25 23 24 syl6bbr ⊢ A ∈ V ∧ B ∈ V ∧ A = ⋂ x → x ∈ 𝒫 B ∩ Fin ↔ x ∈ 𝒫 B ∩ Fin ∖ ∅
26 25 pm5.32da ⊢ A ∈ V ∧ B ∈ V → A = ⋂ x ∧ x ∈ 𝒫 B ∩ Fin ↔ A = ⋂ x ∧ x ∈ 𝒫 B ∩ Fin ∖ ∅
27 ancom ⊢ x ∈ 𝒫 B ∩ Fin ∧ A = ⋂ x ↔ A = ⋂ x ∧ x ∈ 𝒫 B ∩ Fin
28 ancom ⊢ x ∈ 𝒫 B ∩ Fin ∖ ∅ ∧ A = ⋂ x ↔ A = ⋂ x ∧ x ∈ 𝒫 B ∩ Fin ∖ ∅
29 26 27 28 3bitr4g ⊢ A ∈ V ∧ B ∈ V → x ∈ 𝒫 B ∩ Fin ∧ A = ⋂ x ↔ x ∈ 𝒫 B ∩ Fin ∖ ∅ ∧ A = ⋂ x
30 29 rexbidv2 ⊢ A ∈ V ∧ B ∈ V → ∃ x ∈ 𝒫 B ∩ Fin A = ⋂ x ↔ ∃ x ∈ 𝒫 B ∩ Fin ∖ ∅ A = ⋂ x
31 11 30 bitrd ⊢ A ∈ V ∧ B ∈ V → A ∈ fi ⁡ B ↔ ∃ x ∈ 𝒫 B ∩ Fin ∖ ∅ A = ⋂ x
32 31 expcom ⊢ B ∈ V → A ∈ V → A ∈ fi ⁡ B ↔ ∃ x ∈ 𝒫 B ∩ Fin ∖ ∅ A = ⋂ x
33 2 10 32 pm5.21ndd ⊢ B ∈ V → A ∈ fi ⁡ B ↔ ∃ x ∈ 𝒫 B ∩ Fin ∖ ∅ A = ⋂ x