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 ( 𝐵𝑉 → ( 𝐴 ∈ ( fi ‘ 𝐵 ) ↔ ∃ 𝑥 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) 𝐴 = 𝑥 ) )

Proof

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