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