Metamath Proof Explorer


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