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 ) 𝑦 = ∩ 𝑥 } )