Metamath Proof Explorer

Theorem hashrabsn01

Description: The size of a restricted class abstraction restricted to a singleton is either 0 or 1. (Contributed by Alexander van der Vekens, 3-Sep-2018)

Ref Expression
Assertion hashrabsn01 ⊢ x ∈ A | φ = N → N = 0 ∨ N = 1

Proof

Step Hyp Ref Expression
1 eqid ⊢ x ∈ A | φ = x ∈ A | φ
2 rabrsn ⊢ x ∈ A | φ = x ∈ A | φ → x ∈ A | φ = ∅ ∨ x ∈ A | φ = A
3 fveqeq2 ⊢ x ∈ A | φ = ∅ → x ∈ A | φ = N ↔ ∅ = N
4 eqcom ⊢ ∅ = N ↔ N = ∅
5 4 biimpi ⊢ ∅ = N → N = ∅
6 hash0 ⊢ ∅ = 0
7 5 6 eqtrdi ⊢ ∅ = N → N = 0
8 7 orcd ⊢ ∅ = N → N = 0 ∨ N = 1
9 3 8 biimtrdi ⊢ x ∈ A | φ = ∅ → x ∈ A | φ = N → N = 0 ∨ N = 1
10 fveqeq2 ⊢ x ∈ A | φ = A → x ∈ A | φ = N ↔ A = N
11 eqcom ⊢ A = N ↔ N = A
12 11 biimpi ⊢ A = N → N = A
13 hashsng ⊢ A ∈ V → A = 1
14 12 13 sylan9eqr ⊢ A ∈ V ∧ A = N → N = 1
15 14 olcd ⊢ A ∈ V ∧ A = N → N = 0 ∨ N = 1
16 15 ex ⊢ A ∈ V → A = N → N = 0 ∨ N = 1
17 snprc ⊢ ¬ A ∈ V ↔ A = ∅
18 fveqeq2 ⊢ A = ∅ → A = N ↔ ∅ = N
19 18 8 biimtrdi ⊢ A = ∅ → A = N → N = 0 ∨ N = 1
20 17 19 sylbi ⊢ ¬ A ∈ V → A = N → N = 0 ∨ N = 1
21 16 20 pm2.61i ⊢ A = N → N = 0 ∨ N = 1
22 10 21 biimtrdi ⊢ x ∈ A | φ = A → x ∈ A | φ = N → N = 0 ∨ N = 1
23 9 22 jaoi ⊢ x ∈ A | φ = ∅ ∨ x ∈ A | φ = A → x ∈ A | φ = N → N = 0 ∨ N = 1
24 1 2 23 mp2b ⊢ x ∈ A | φ = N → N = 0 ∨ N = 1