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∈By=Sb=y|∃b∈By=Sb
2 eqid ⊢x∈B⟼Sx=x∈B⟼Sx
3 1 2 fsetsnf1o ⊢S∈V→x∈B⟼Sx:B⟶1-1 ontoy|∃b∈By=Sb
4 f1ovv ⊢x∈B⟼Sx:B⟶1-1 ontoy|∃b∈By=Sb→B∈V↔y|∃b∈By=Sb∈V
5 3 4 syl ⊢S∈V→B∈V↔y|∃b∈By=Sb∈V
6 5 notbid ⊢S∈V→¬B∈V↔¬y|∃b∈By=Sb∈V
7 df-nel ⊢B∉V↔¬B∈V
8 df-nel ⊢y|∃b∈By=Sb∉V↔¬y|∃b∈By=Sb∈V
9 6 7 8 3bitr4g ⊢S∈V→B∉V↔y|∃b∈By=Sb∉V
10 9 biimpa ⊢S∈V∧B∉V→y|∃b∈By=Sb∉V
11 fsetabsnop ⊢S∈V→f|f:S⟶B=y|∃b∈By=Sb
12 11 adantr ⊢S∈V∧B∉V→f|f:S⟶B=y|∃b∈By=Sb
13 eqidd ⊢S∈V∧B∉V→V=V
14 12 13 neleq12d ⊢S∈V∧B∉V→f|f:S⟶B∉V↔y|∃b∈By=Sb∉V
15 10 14 mpbird ⊢S∈V∧B∉V→f|f:S⟶B∉V