Theorem hashbc0

Description: The set of subsets of size zero is the singleton of the empty set. (Contributed by Mario Carneiro, 22-Apr-2015)

	Ref	Expression
Hypothesis	ramval.c	⊢ 𝐶 = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
Assertion	hashbc0	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 𝐶 0 ) = { ∅ } )

Proof

Step	Hyp	Ref	Expression
1		ramval.c	⊢ 𝐶 = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
2		0nn0	⊢ 0 ∈ ℕ0
3	1	hashbcval	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 0 ∈ ℕ0 ) → ( 𝐴 𝐶 0 ) = { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } )
4	2 3	mpan2	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 𝐶 0 ) = { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } )
5		hasheq0	⊢ ( 𝑥 ∈ V → ( ( ♯ ‘ 𝑥 ) = 0 ↔ 𝑥 = ∅ ) )
6	5	elv	⊢ ( ( ♯ ‘ 𝑥 ) = 0 ↔ 𝑥 = ∅ )
7	6	anbi2i	⊢ ( ( 𝑥 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑥 ) = 0 ) ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 = ∅ ) )
8		id	⊢ ( 𝑥 = ∅ → 𝑥 = ∅ )
9		0elpw	⊢ ∅ ∈ 𝒫 𝐴
10	8 9	eqeltrdi	⊢ ( 𝑥 = ∅ → 𝑥 ∈ 𝒫 𝐴 )
11	10	pm4.71ri	⊢ ( 𝑥 = ∅ ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 = ∅ ) )
12	7 11	bitr4i	⊢ ( ( 𝑥 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑥 ) = 0 ) ↔ 𝑥 = ∅ )
13	12	abbii	⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑥 ) = 0 ) } = { 𝑥 ∣ 𝑥 = ∅ }
14		df-rab	⊢ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } = { 𝑥 ∣ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑥 ) = 0 ) }
15		df-sn	⊢ { ∅ } = { 𝑥 ∣ 𝑥 = ∅ }
16	13 14 15	3eqtr4i	⊢ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } = { ∅ }
17	4 16	eqtrdi	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 𝐶 0 ) = { ∅ } )