Metamath Proof Explorer

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 ⊢ C = a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i
Assertion hashbcval ⊢ A ∈ V ∧ N ∈ ℕ 0 → A C N = x ∈ 𝒫 A | x = N

Proof

Step Hyp Ref Expression
1 ramval.c ⊢ C = a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i
2 elex ⊢ A ∈ V → A ∈ V
3 pwexg ⊢ A ∈ V → 𝒫 A ∈ V
4 3 adantr ⊢ A ∈ V ∧ N ∈ ℕ 0 → 𝒫 A ∈ V
5 rabexg ⊢ 𝒫 A ∈ V → x ∈ 𝒫 A | x = N ∈ V
6 4 5 syl ⊢ A ∈ V ∧ N ∈ ℕ 0 → x ∈ 𝒫 A | x = N ∈ V
7 fveqeq2 ⊢ b = x → b = i ↔ x = i
8 7 cbvrabv ⊢ b ∈ 𝒫 a | b = i = x ∈ 𝒫 a | x = i
9 simpl ⊢ a = A ∧ i = N → a = A
10 9 pweqd ⊢ a = A ∧ i = N → 𝒫 a = 𝒫 A
11 simpr ⊢ a = A ∧ i = N → i = N
12 11 eqeq2d ⊢ a = A ∧ i = N → x = i ↔ x = N
13 10 12 rabeqbidv ⊢ a = A ∧ i = N → x ∈ 𝒫 a | x = i = x ∈ 𝒫 A | x = N
14 8 13 eqtrid ⊢ a = A ∧ i = N → b ∈ 𝒫 a | b = i = x ∈ 𝒫 A | x = N
15 14 1 ovmpoga ⊢ A ∈ V ∧ N ∈ ℕ 0 ∧ x ∈ 𝒫 A | x = N ∈ V → A C N = x ∈ 𝒫 A | x = N
16 6 15 mpd3an3 ⊢ A ∈ V ∧ N ∈ ℕ 0 → A C N = x ∈ 𝒫 A | x = N
17 2 16 sylan ⊢ A ∈ V ∧ N ∈ ℕ 0 → A C N = x ∈ 𝒫 A | x = N