Theorem hashrabrsn

Description: The size of a restricted class abstraction restricted to a singleton is a nonnegative integer. (Contributed by Alexander van der Vekens, 22-Dec-2017)

	Ref	Expression
Assertion	hashrabrsn	⊢ ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) ∈ ℕ0

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝑥 ∈ { 𝐴 } ∣ 𝜑 }
2		rabrsn	⊢ ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } → ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = ∅ ∨ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } ) )
3		fveq2	⊢ ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = ∅ → ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = ( ♯ ‘ ∅ ) )
4		hash0	⊢ ( ♯ ‘ ∅ ) = 0
5		0nn0	⊢ 0 ∈ ℕ0
6	4 5	eqeltri	⊢ ( ♯ ‘ ∅ ) ∈ ℕ0
7	3 6	eqeltrdi	⊢ ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = ∅ → ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) ∈ ℕ0 )
8		fveq2	⊢ ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } → ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = ( ♯ ‘ { 𝐴 } ) )
9		hashsng	⊢ ( 𝐴 ∈ V → ( ♯ ‘ { 𝐴 } ) = 1 )
10		1nn0	⊢ 1 ∈ ℕ0
11	9 10	eqeltrdi	⊢ ( 𝐴 ∈ V → ( ♯ ‘ { 𝐴 } ) ∈ ℕ0 )
12		snprc	⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
13		fveq2	⊢ ( { 𝐴 } = ∅ → ( ♯ ‘ { 𝐴 } ) = ( ♯ ‘ ∅ ) )
14	13 6	eqeltrdi	⊢ ( { 𝐴 } = ∅ → ( ♯ ‘ { 𝐴 } ) ∈ ℕ0 )
15	12 14	sylbi	⊢ ( ¬ 𝐴 ∈ V → ( ♯ ‘ { 𝐴 } ) ∈ ℕ0 )
16	11 15	pm2.61i	⊢ ( ♯ ‘ { 𝐴 } ) ∈ ℕ0
17	8 16	eqeltrdi	⊢ ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } → ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) ∈ ℕ0 )
18	7 17	jaoi	⊢ ( ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = ∅ ∨ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } ) → ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) ∈ ℕ0 )
19	1 2 18	mp2b	⊢ ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) ∈ ℕ0