This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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