Theorem ballotlemoex

Description: O is a set. (Contributed by Thierry Arnoux, 7-Dec-2016)

	Ref	Expression
Hypotheses	ballotth.m	⊢ 𝑀 ∈ ℕ
	ballotth.n	⊢ 𝑁 ∈ ℕ
	ballotth.o	⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
Assertion	ballotlemoex	⊢ 𝑂 ∈ V

Proof

Step	Hyp	Ref	Expression
1		ballotth.m	⊢ 𝑀 ∈ ℕ
2		ballotth.n	⊢ 𝑁 ∈ ℕ
3		ballotth.o	⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
4		ovex	⊢ ( 1 ... ( 𝑀 + 𝑁 ) ) ∈ V
5	4	pwex	⊢ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∈ V
6	3 5	rabex2	⊢ 𝑂 ∈ V