Metamath Proof Explorer

Theorem fsetsnprcnex

Description: The class of all functions from a (proper) singleton into a proper class B is not a set. (Contributed by AV, 13-Sep-2024)

Ref Expression
Assertion fsetsnprcnex ⊢ S ∈ V ∧ B ∉ V → f | f : S ⟶ B ∉ V

Proof

Step Hyp Ref Expression
1 eqid ⊢ y | ∃ b ∈ B y = S b = y | ∃ b ∈ B y = S b
2 eqid ⊢ x ∈ B ⟼ S x = x ∈ B ⟼ S x
3 1 2 fsetsnf1o ⊢ S ∈ V → x ∈ B ⟼ S x : B ⟶ 1-1 onto y | ∃ b ∈ B y = S b
4 f1ovv ⊢ x ∈ B ⟼ S x : B ⟶ 1-1 onto y | ∃ b ∈ B y = S b → B ∈ V ↔ y | ∃ b ∈ B y = S b ∈ V
5 3 4 syl ⊢ S ∈ V → B ∈ V ↔ y | ∃ b ∈ B y = S b ∈ V
6 5 notbid ⊢ S ∈ V → ¬ B ∈ V ↔ ¬ y | ∃ b ∈ B y = S b ∈ V
7 df-nel ⊢ B ∉ V ↔ ¬ B ∈ V
8 df-nel ⊢ y | ∃ b ∈ B y = S b ∉ V ↔ ¬ y | ∃ b ∈ B y = S b ∈ V
9 6 7 8 3bitr4g ⊢ S ∈ V → B ∉ V ↔ y | ∃ b ∈ B y = S b ∉ V
10 9 biimpa ⊢ S ∈ V ∧ B ∉ V → y | ∃ b ∈ B y = S b ∉ V
11 fsetabsnop ⊢ S ∈ V → f | f : S ⟶ B = y | ∃ b ∈ B y = S b
12 11 adantr ⊢ S ∈ V ∧ B ∉ V → f | f : S ⟶ B = y | ∃ b ∈ B y = S b
13 eqidd ⊢ S ∈ V ∧ B ∉ V → V = V
14 12 13 neleq12d ⊢ S ∈ V ∧ B ∉ V → f | f : S ⟶ B ∉ V ↔ y | ∃ b ∈ B y = S b ∉ V
15 10 14 mpbird ⊢ S ∈ V ∧ B ∉ V → f | f : S ⟶ B ∉ V