Theorem fi0

Description: The set of finite intersections of the empty set. (Contributed by Mario Carneiro, 30-Aug-2015)

	Ref	Expression
Assertion	fi0	⊢ ( fi ‘ ∅ ) = ∅

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2		fival	⊢ ( ∅ ∈ V → ( fi ‘ ∅ ) = { 𝑦 ∣ ∃ 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) 𝑦 = ∩ 𝑥 } )
3	1 2	ax-mp	⊢ ( fi ‘ ∅ ) = { 𝑦 ∣ ∃ 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) 𝑦 = ∩ 𝑥 }
4		vprc	⊢ ¬ V ∈ V
5		id	⊢ ( 𝑦 = ∩ 𝑥 → 𝑦 = ∩ 𝑥 )
6		elinel1	⊢ ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) → 𝑥 ∈ 𝒫 ∅ )
7		elpwi	⊢ ( 𝑥 ∈ 𝒫 ∅ → 𝑥 ⊆ ∅ )
8		ss0	⊢ ( 𝑥 ⊆ ∅ → 𝑥 = ∅ )
9	6 7 8	3syl	⊢ ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) → 𝑥 = ∅ )
10	9	inteqd	⊢ ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) → ∩ 𝑥 = ∩ ∅ )
11		int0	⊢ ∩ ∅ = V
12	10 11	syl6eq	⊢ ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) → ∩ 𝑥 = V )
13	5 12	sylan9eqr	⊢ ( ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ∧ 𝑦 = ∩ 𝑥 ) → 𝑦 = V )
14	13	rexlimiva	⊢ ( ∃ 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) 𝑦 = ∩ 𝑥 → 𝑦 = V )
15		vex	⊢ 𝑦 ∈ V
16	14 15	eqeltrrdi	⊢ ( ∃ 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) 𝑦 = ∩ 𝑥 → V ∈ V )
17	4 16	mto	⊢ ¬ ∃ 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) 𝑦 = ∩ 𝑥
18	17	abf	⊢ { 𝑦 ∣ ∃ 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) 𝑦 = ∩ 𝑥 } = ∅
19	3 18	eqtri	⊢ ( fi ‘ ∅ ) = ∅