Theorem ballotlemelo

Description: Elementhood in O . (Contributed by Thierry Arnoux, 17-Apr-2017)

	Ref	Expression
Hypotheses	ballotth.m	⊢ 𝑀 ∈ ℕ
	ballotth.n	⊢ 𝑁 ∈ ℕ
	ballotth.o	⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
Assertion	ballotlemelo	⊢ ( 𝐶 ∈ 𝑂 ↔ ( 𝐶 ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ♯ ‘ 𝐶 ) = 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		ballotth.m	⊢ 𝑀 ∈ ℕ
2		ballotth.n	⊢ 𝑁 ∈ ℕ
3		ballotth.o	⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
4		fveqeq2	⊢ ( 𝑑 = 𝐶 → ( ( ♯ ‘ 𝑑 ) = 𝑀 ↔ ( ♯ ‘ 𝐶 ) = 𝑀 ) )
5		fveqeq2	⊢ ( 𝑐 = 𝑑 → ( ( ♯ ‘ 𝑐 ) = 𝑀 ↔ ( ♯ ‘ 𝑑 ) = 𝑀 ) )
6	5	cbvrabv	⊢ { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 } = { 𝑑 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑑 ) = 𝑀 }
7	3 6	eqtri	⊢ 𝑂 = { 𝑑 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑑 ) = 𝑀 }
8	4 7	elrab2	⊢ ( 𝐶 ∈ 𝑂 ↔ ( 𝐶 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ♯ ‘ 𝐶 ) = 𝑀 ) )
9		ovex	⊢ ( 1 ... ( 𝑀 + 𝑁 ) ) ∈ V
10	9	elpw2	⊢ ( 𝐶 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ↔ 𝐶 ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
11	10	anbi1i	⊢ ( ( 𝐶 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ♯ ‘ 𝐶 ) = 𝑀 ) ↔ ( 𝐶 ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ♯ ‘ 𝐶 ) = 𝑀 ) )
12	8 11	bitri	⊢ ( 𝐶 ∈ 𝑂 ↔ ( 𝐶 ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ♯ ‘ 𝐶 ) = 𝑀 ) )