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 ) )