hashbcval

Description: Value of the "binomial set", the set of all N -element subsets of A . (Contributed by Mario Carneiro, 20-Apr-2015)

		Ref	Expression
	Hypothesis	ramval.c	$⊢ C = (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\})$
	Assertion	hashbcval	$⊢ (A \in V \land N \in ℕ_{0}) \to A C N = \{x \in 𝒫 A \| \|x\| = N\}$

Step	Hyp	Ref	Expression
1		ramval.c	$⊢ C = (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\})$
2		elex	$⊢ A \in V \to A \in V$
3		pwexg	$⊢ A \in V \to 𝒫 A \in V$
4	3	adantr	$⊢ (A \in V \land N \in ℕ_{0}) \to 𝒫 A \in V$
5		rabexg	$⊢ 𝒫 A \in V \to \{x \in 𝒫 A \| \|x\| = N\} \in V$
6	4 5	syl	$⊢ (A \in V \land N \in ℕ_{0}) \to \{x \in 𝒫 A \| \|x\| = N\} \in V$
7		fveqeq2	$⊢ b = x \to (\|b\| = i \leftrightarrow \|x\| = i)$
8	7	cbvrabv	$⊢ \{b \in 𝒫 a \| \|b\| = i\} = \{x \in 𝒫 a \| \|x\| = i\}$
9		simpl	$⊢ (a = A \land i = N) \to a = A$
10	9	pweqd	$⊢ (a = A \land i = N) \to 𝒫 a = 𝒫 A$
11		simpr	$⊢ (a = A \land i = N) \to i = N$
12	11	eqeq2d	$⊢ (a = A \land i = N) \to (\|x\| = i \leftrightarrow \|x\| = N)$
13	10 12	rabeqbidv	$⊢ (a = A \land i = N) \to \{x \in 𝒫 a \| \|x\| = i\} = \{x \in 𝒫 A \| \|x\| = N\}$
14	8 13	eqtrid	$⊢ (a = A \land i = N) \to \{b \in 𝒫 a \| \|b\| = i\} = \{x \in 𝒫 A \| \|x\| = N\}$
15	14 1	ovmpoga	$⊢ (A \in V \land N \in ℕ_{0} \land \{x \in 𝒫 A \| \|x\| = N\} \in V) \to A C N = \{x \in 𝒫 A \| \|x\| = N\}$
16	6 15	mpd3an3	$⊢ (A \in V \land N \in ℕ_{0}) \to A C N = \{x \in 𝒫 A \| \|x\| = N\}$
17	2 16	sylan	$⊢ (A \in V \land N \in ℕ_{0}) \to A C N = \{x \in 𝒫 A \| \|x\| = N\}$

Metamath Proof Explorer