ackbij1lem7

		Ref	Expression
	Hypothesis	ackbij.f	$⊢ F = (x \in (𝒫 ω \cap Fin) ⟼ card (⋃_{y \in x} (\{y\} \times 𝒫 y)))$
	Assertion	ackbij1lem7	$⊢ A \in (𝒫 ω \cap Fin) \to F (A) = card (⋃_{y \in A} (\{y\} \times 𝒫 y))$

Step	Hyp	Ref	Expression
1		ackbij.f	$⊢ F = (x \in (𝒫 ω \cap Fin) ⟼ card (⋃_{y \in x} (\{y\} \times 𝒫 y)))$
2		iuneq1	$⊢ x = A \to ⋃_{y \in x} (\{y\} \times 𝒫 y) = ⋃_{y \in A} (\{y\} \times 𝒫 y)$
3	2	fveq2d	$⊢ x = A \to card (⋃_{y \in x} (\{y\} \times 𝒫 y)) = card (⋃_{y \in A} (\{y\} \times 𝒫 y))$
4		fvex	$⊢ card (⋃_{y \in A} (\{y\} \times 𝒫 y)) \in V$
5	3 1 4	fvmpt	$⊢ A \in (𝒫 ω \cap Fin) \to F (A) = card (⋃_{y \in A} (\{y\} \times 𝒫 y))$

Metamath Proof Explorer