This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ∖ { ∅ } ) 𝐴 = ∩ 𝑥 ) )