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∩FinA=⋂x
12 vprc ⊢¬V∈V
13 elsni ⊢x∈∅→x=∅
14 13 inteqd ⊢x∈∅→⋂x=⋂∅
15 int0 ⊢⋂∅=V
16 14 15 eqtrdi ⊢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 bitr4di ⊢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∩FinA=⋂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