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

Metamath Proof Explorer

Theorem fival

Description: The set of all the finite intersections of the elements of A . (Contributed by FL, 27-Apr-2008) (Revised by Mario Carneiro, 24-Nov-2013)

Ref Expression
Assertion fival ( 𝐴 ∈ 𝑉 → ( fi ‘ 𝐴 ) = { 𝑦 ∣ ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑦 = ∩ 𝑥 } )

Proof

Step Hyp Ref Expression
1 df-fi ⊢ fi = ( 𝑧 ∈ V ↦ { 𝑦 ∣ ∃ 𝑥 ∈ ( 𝒫 𝑧 ∩ Fin ) 𝑦 = ∩ 𝑥 } )
2 pweq ⊢ ( 𝑧 = 𝐴 → 𝒫 𝑧 = 𝒫 𝐴 )
3 2 ineq1d ⊢ ( 𝑧 = 𝐴 → ( 𝒫 𝑧 ∩ Fin ) = ( 𝒫 𝐴 ∩ Fin ) )
4 3 rexeqdv ⊢ ( 𝑧 = 𝐴 → ( ∃ 𝑥 ∈ ( 𝒫 𝑧 ∩ Fin ) 𝑦 = ∩ 𝑥 ↔ ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑦 = ∩ 𝑥 ) )
5 4 abbidv ⊢ ( 𝑧 = 𝐴 → { 𝑦 ∣ ∃ 𝑥 ∈ ( 𝒫 𝑧 ∩ Fin ) 𝑦 = ∩ 𝑥 } = { 𝑦 ∣ ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑦 = ∩ 𝑥 } )
6 elex ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
7 simpr ⊢ ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑦 = ∩ 𝑥 ) → 𝑦 = ∩ 𝑥 )
8 elinel1 ⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑥 ∈ 𝒫 𝐴 )
9 8 elpwid ⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑥 ⊆ 𝐴 )
10 eqvisset ⊢ ( 𝑦 = ∩ 𝑥 → ∩ 𝑥 ∈ V )
11 intex ⊢ ( 𝑥 ≠ ∅ ↔ ∩ 𝑥 ∈ V )
12 10 11 sylibr ⊢ ( 𝑦 = ∩ 𝑥 → 𝑥 ≠ ∅ )
13 intssuni2 ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∩ 𝑥 ⊆ ∪ 𝐴 )
14 9 12 13 syl2an ⊢ ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑦 = ∩ 𝑥 ) → ∩ 𝑥 ⊆ ∪ 𝐴 )
15 7 14 eqsstrd ⊢ ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑦 = ∩ 𝑥 ) → 𝑦 ⊆ ∪ 𝐴 )
16 velpw ⊢ ( 𝑦 ∈ 𝒫 ∪ 𝐴 ↔ 𝑦 ⊆ ∪ 𝐴 )
17 15 16 sylibr ⊢ ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑦 = ∩ 𝑥 ) → 𝑦 ∈ 𝒫 ∪ 𝐴 )
18 17 rexlimiva ⊢ ( ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑦 = ∩ 𝑥 → 𝑦 ∈ 𝒫 ∪ 𝐴 )
19 18 abssi ⊢ { 𝑦 ∣ ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑦 = ∩ 𝑥 } ⊆ 𝒫 ∪ 𝐴
20 uniexg ⊢ ( 𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V )
21 20 pwexd ⊢ ( 𝐴 ∈ 𝑉 → 𝒫 ∪ 𝐴 ∈ V )
22 ssexg ⊢ ( ( { 𝑦 ∣ ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑦 = ∩ 𝑥 } ⊆ 𝒫 ∪ 𝐴 ∧ 𝒫 ∪ 𝐴 ∈ V ) → { 𝑦 ∣ ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑦 = ∩ 𝑥 } ∈ V )
23 19 21 22 sylancr ⊢ ( 𝐴 ∈ 𝑉 → { 𝑦 ∣ ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑦 = ∩ 𝑥 } ∈ V )
24 1 5 6 23 fvmptd3 ⊢ ( 𝐴 ∈ 𝑉 → ( fi ‘ 𝐴 ) = { 𝑦 ∣ ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑦 = ∩ 𝑥 } )