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

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 ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 𝑁 → ( 𝑁 = 0 ∨ 𝑁 = 1 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝑥 ∈ { 𝐴 } ∣ 𝜑 }
2 rabrsn ⊢ ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } → ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = ∅ ∨ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } ) )
3 fveqeq2 ⊢ ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = ∅ → ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 𝑁 ↔ ( ♯ ‘ ∅ ) = 𝑁 ) )
4 eqcom ⊢ ( ( ♯ ‘ ∅ ) = 𝑁 ↔ 𝑁 = ( ♯ ‘ ∅ ) )
5 4 biimpi ⊢ ( ( ♯ ‘ ∅ ) = 𝑁 → 𝑁 = ( ♯ ‘ ∅ ) )
6 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
7 5 6 eqtrdi ⊢ ( ( ♯ ‘ ∅ ) = 𝑁 → 𝑁 = 0 )
8 7 orcd ⊢ ( ( ♯ ‘ ∅ ) = 𝑁 → ( 𝑁 = 0 ∨ 𝑁 = 1 ) )
9 3 8 biimtrdi ⊢ ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = ∅ → ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 𝑁 → ( 𝑁 = 0 ∨ 𝑁 = 1 ) ) )
10 fveqeq2 ⊢ ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } → ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 𝑁 ↔ ( ♯ ‘ { 𝐴 } ) = 𝑁 ) )
11 eqcom ⊢ ( ( ♯ ‘ { 𝐴 } ) = 𝑁 ↔ 𝑁 = ( ♯ ‘ { 𝐴 } ) )
12 11 biimpi ⊢ ( ( ♯ ‘ { 𝐴 } ) = 𝑁 → 𝑁 = ( ♯ ‘ { 𝐴 } ) )
13 hashsng ⊢ ( 𝐴 ∈ V → ( ♯ ‘ { 𝐴 } ) = 1 )
14 12 13 sylan9eqr ⊢ ( ( 𝐴 ∈ V ∧ ( ♯ ‘ { 𝐴 } ) = 𝑁 ) → 𝑁 = 1 )
15 14 olcd ⊢ ( ( 𝐴 ∈ V ∧ ( ♯ ‘ { 𝐴 } ) = 𝑁 ) → ( 𝑁 = 0 ∨ 𝑁 = 1 ) )
16 15 ex ⊢ ( 𝐴 ∈ V → ( ( ♯ ‘ { 𝐴 } ) = 𝑁 → ( 𝑁 = 0 ∨ 𝑁 = 1 ) ) )
17 snprc ⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
18 fveqeq2 ⊢ ( { 𝐴 } = ∅ → ( ( ♯ ‘ { 𝐴 } ) = 𝑁 ↔ ( ♯ ‘ ∅ ) = 𝑁 ) )
19 18 8 biimtrdi ⊢ ( { 𝐴 } = ∅ → ( ( ♯ ‘ { 𝐴 } ) = 𝑁 → ( 𝑁 = 0 ∨ 𝑁 = 1 ) ) )
20 17 19 sylbi ⊢ ( ¬ 𝐴 ∈ V → ( ( ♯ ‘ { 𝐴 } ) = 𝑁 → ( 𝑁 = 0 ∨ 𝑁 = 1 ) ) )
21 16 20 pm2.61i ⊢ ( ( ♯ ‘ { 𝐴 } ) = 𝑁 → ( 𝑁 = 0 ∨ 𝑁 = 1 ) )
22 10 21 biimtrdi ⊢ ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } → ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 𝑁 → ( 𝑁 = 0 ∨ 𝑁 = 1 ) ) )
23 9 22 jaoi ⊢ ( ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = ∅ ∨ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } ) → ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 𝑁 → ( 𝑁 = 0 ∨ 𝑁 = 1 ) ) )
24 1 2 23 mp2b ⊢ ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 𝑁 → ( 𝑁 = 0 ∨ 𝑁 = 1 ) )