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 ⊢x∈A|φ∈ℕ0

Proof

Step Hyp Ref Expression
1 eqid ⊢x∈A|φ=x∈A|φ
2 rabrsn ⊢x∈A|φ=x∈A|φ→x∈A|φ=∅∨x∈A|φ=A
3 fveq2 ⊢x∈A|φ=∅→x∈A|φ=∅
4 hash0 ⊢∅=0
5 0nn0 ⊢0∈ℕ0
6 4 5 eqeltri ⊢∅∈ℕ0
7 3 6 eqeltrdi ⊢x∈A|φ=∅→x∈A|φ∈ℕ0
8 fveq2 ⊢x∈A|φ=A→x∈A|φ=A
9 hashsng ⊢A∈V→A=1
10 1nn0 ⊢1∈ℕ0
11 9 10 eqeltrdi ⊢A∈V→A∈ℕ0
12 snprc ⊢¬A∈V↔A=∅
13 fveq2 ⊢A=∅→A=∅
14 13 6 eqeltrdi ⊢A=∅→A∈ℕ0
15 12 14 sylbi ⊢¬A∈V→A∈ℕ0
16 11 15 pm2.61i ⊢A∈ℕ0
17 8 16 eqeltrdi ⊢x∈A|φ=A→x∈A|φ∈ℕ0
18 7 17 jaoi ⊢x∈A|φ=∅∨x∈A|φ=A→x∈A|φ∈ℕ0
19 1 2 18 mp2b ⊢x∈A|φ∈ℕ0