Theorem 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	⊢ 𝐶 = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
Assertion	hashbcval	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 𝐶 𝑁 ) = { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑁 } )

Proof

Step	Hyp	Ref	Expression
1		ramval.c	⊢ 𝐶 = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
2		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
3		pwexg	⊢ ( 𝐴 ∈ V → 𝒫 𝐴 ∈ V )
4	3	adantr	⊢ ( ( 𝐴 ∈ V ∧ 𝑁 ∈ ℕ0 ) → 𝒫 𝐴 ∈ V )
5		rabexg	⊢ ( 𝒫 𝐴 ∈ V → { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑁 } ∈ V )
6	4 5	syl	⊢ ( ( 𝐴 ∈ V ∧ 𝑁 ∈ ℕ0 ) → { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑁 } ∈ V )
7		fveqeq2	⊢ ( 𝑏 = 𝑥 → ( ( ♯ ‘ 𝑏 ) = 𝑖 ↔ ( ♯ ‘ 𝑥 ) = 𝑖 ) )
8	7	cbvrabv	⊢ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } = { 𝑥 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑥 ) = 𝑖 }
9		simpl	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑖 = 𝑁 ) → 𝑎 = 𝐴 )
10	9	pweqd	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑖 = 𝑁 ) → 𝒫 𝑎 = 𝒫 𝐴 )
11		simpr	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑖 = 𝑁 ) → 𝑖 = 𝑁 )
12	11	eqeq2d	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑖 = 𝑁 ) → ( ( ♯ ‘ 𝑥 ) = 𝑖 ↔ ( ♯ ‘ 𝑥 ) = 𝑁 ) )
13	10 12	rabeqbidv	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑖 = 𝑁 ) → { 𝑥 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑥 ) = 𝑖 } = { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑁 } )
14	8 13	syl5eq	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑖 = 𝑁 ) → { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } = { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑁 } )
15	14 1	ovmpoga	⊢ ( ( 𝐴 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑁 } ∈ V ) → ( 𝐴 𝐶 𝑁 ) = { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑁 } )
16	6 15	mpd3an3	⊢ ( ( 𝐴 ∈ V ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 𝐶 𝑁 ) = { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑁 } )
17	2 16	sylan	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 𝐶 𝑁 ) = { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑁 } )