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	$⊢ A \in V \to fi (A) = \{y \| \exists x \in (𝒫 A \cap Fin) y = ⋂ x\}$

Proof

Step	Hyp	Ref	Expression
1		df-fi	$⊢ fi = (z \in V ⟼ \{y \| \exists x \in (𝒫 z \cap Fin) y = ⋂ x\})$
2		pweq	$⊢ z = A \to 𝒫 z = 𝒫 A$
3	2	ineq1d	$⊢ z = A \to 𝒫 z \cap Fin = 𝒫 A \cap Fin$
4	3	rexeqdv	$⊢ z = A \to (\exists x \in (𝒫 z \cap Fin) y = ⋂ x \leftrightarrow \exists x \in (𝒫 A \cap Fin) y = ⋂ x)$
5	4	abbidv	$⊢ z = A \to \{y \| \exists x \in (𝒫 z \cap Fin) y = ⋂ x\} = \{y \| \exists x \in (𝒫 A \cap Fin) y = ⋂ x\}$
6		elex	$⊢ A \in V \to A \in V$
7		simpr	$⊢ (x \in (𝒫 A \cap Fin) \land y = ⋂ x) \to y = ⋂ x$
8		elinel1	$⊢ x \in (𝒫 A \cap Fin) \to x \in 𝒫 A$
9	8	elpwid	$⊢ x \in (𝒫 A \cap Fin) \to x \subseteq A$
10		eqvisset	$⊢ y = ⋂ x \to ⋂ x \in V$
11		intex	$⊢ x \neq \emptyset \leftrightarrow ⋂ x \in V$
12	10 11	sylibr	$⊢ y = ⋂ x \to x \neq \emptyset$
13		intssuni2	$⊢ (x \subseteq A \land x \neq \emptyset) \to ⋂ x \subseteq ⋃ A$
14	9 12 13	syl2an	$⊢ (x \in (𝒫 A \cap Fin) \land y = ⋂ x) \to ⋂ x \subseteq ⋃ A$
15	7 14	eqsstrd	$⊢ (x \in (𝒫 A \cap Fin) \land y = ⋂ x) \to y \subseteq ⋃ A$
16		velpw	$⊢ y \in 𝒫 ⋃ A \leftrightarrow y \subseteq ⋃ A$
17	15 16	sylibr	$⊢ (x \in (𝒫 A \cap Fin) \land y = ⋂ x) \to y \in 𝒫 ⋃ A$
18	17	rexlimiva	$⊢ \exists x \in (𝒫 A \cap Fin) y = ⋂ x \to y \in 𝒫 ⋃ A$
19	18	abssi	$⊢ \{y \| \exists x \in (𝒫 A \cap Fin) y = ⋂ x\} \subseteq 𝒫 ⋃ A$
20		uniexg	$⊢ A \in V \to ⋃ A \in V$
21	20	pwexd	$⊢ A \in V \to 𝒫 ⋃ A \in V$
22		ssexg	$⊢ (\{y \| \exists x \in (𝒫 A \cap Fin) y = ⋂ x\} \subseteq 𝒫 ⋃ A \land 𝒫 ⋃ A \in V) \to \{y \| \exists x \in (𝒫 A \cap Fin) y = ⋂ x\} \in V$
23	19 21 22	sylancr	$⊢ A \in V \to \{y \| \exists x \in (𝒫 A \cap Fin) y = ⋂ x\} \in V$
24	1 5 6 23	fvmptd3	$⊢ A \in V \to fi (A) = \{y \| \exists x \in (𝒫 A \cap Fin) y = ⋂ x\}$

Metamath Proof Explorer

Theorem fival

Proof