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 e. V /\ B e/ _V ) -> { f | f : { S } --> B } e/ _V )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- { y | E. b e. B y = { <. S , b >. } } = { y | E. b e. B y = { <. S , b >. } }
2		eqid	|- ( x e. B |-> { <. S , x >. } ) = ( x e. B |-> { <. S , x >. } )
3	1 2	fsetsnf1o	|- ( S e. V -> ( x e. B |-> { <. S , x >. } ) : B -1-1-onto-> { y | E. b e. B y = { <. S , b >. } } )
4		f1ovv	|- ( ( x e. B |-> { <. S , x >. } ) : B -1-1-onto-> { y | E. b e. B y = { <. S , b >. } } -> ( B e. _V <-> { y | E. b e. B y = { <. S , b >. } } e. _V ) )
5	3 4	syl	|- ( S e. V -> ( B e. _V <-> { y | E. b e. B y = { <. S , b >. } } e. _V ) )
6	5	notbid	|- ( S e. V -> ( -. B e. _V <-> -. { y | E. b e. B y = { <. S , b >. } } e. _V ) )
7		df-nel	|- ( B e/ _V <-> -. B e. _V )
8		df-nel	|- ( { y | E. b e. B y = { <. S , b >. } } e/ _V <-> -. { y | E. b e. B y = { <. S , b >. } } e. _V )
9	6 7 8	3bitr4g	|- ( S e. V -> ( B e/ _V <-> { y | E. b e. B y = { <. S , b >. } } e/ _V ) )
10	9	biimpa	|- ( ( S e. V /\ B e/ _V ) -> { y | E. b e. B y = { <. S , b >. } } e/ _V )
11		fsetabsnop	|- ( S e. V -> { f | f : { S } --> B } = { y | E. b e. B y = { <. S , b >. } } )
12	11	adantr	|- ( ( S e. V /\ B e/ _V ) -> { f | f : { S } --> B } = { y | E. b e. B y = { <. S , b >. } } )
13		eqidd	|- ( ( S e. V /\ B e/ _V ) -> _V = _V )
14	12 13	neleq12d	|- ( ( S e. V /\ B e/ _V ) -> ( { f | f : { S } --> B } e/ _V <-> { y | E. b e. B y = { <. S , b >. } } e/ _V ) )
15	10 14	mpbird	|- ( ( S e. V /\ B e/ _V ) -> { f | f : { S } --> B } e/ _V )