Theorem fsetexb

Description: The class of all functions from a class A into a class B is a set iff B is a set or A is not a set or A is empty. (Contributed by AV, 15-Sep-2024)

	Ref	Expression
Assertion	fsetexb	|- ( { f | f : A --> B } e. _V <-> ( A e/ _V \/ A = (/) \/ B e. _V ) )

Proof

Step	Hyp	Ref	Expression
1		ioran	|- ( -. ( ( A e/ _V \/ A = (/) ) \/ B e. _V ) <-> ( -. ( A e/ _V \/ A = (/) ) /\ -. B e. _V ) )
2		df-nel	|- ( B e/ _V <-> -. B e. _V )
3		ioran	|- ( -. ( A e/ _V \/ A = (/) ) <-> ( -. A e/ _V /\ -. A = (/) ) )
4		nnel	|- ( -. A e/ _V <-> A e. _V )
5		df-ne	|- ( A =/= (/) <-> -. A = (/) )
6	5	bicomi	|- ( -. A = (/) <-> A =/= (/) )
7	4 6	anbi12i	|- ( ( -. A e/ _V /\ -. A = (/) ) <-> ( A e. _V /\ A =/= (/) ) )
8	3 7	bitri	|- ( -. ( A e/ _V \/ A = (/) ) <-> ( A e. _V /\ A =/= (/) ) )
9		fsetprcnex	|- ( ( ( A e. _V /\ A =/= (/) ) /\ B e/ _V ) -> { f | f : A --> B } e/ _V )
10	9	ex	|- ( ( A e. _V /\ A =/= (/) ) -> ( B e/ _V -> { f | f : A --> B } e/ _V ) )
11	8 10	sylbi	|- ( -. ( A e/ _V \/ A = (/) ) -> ( B e/ _V -> { f | f : A --> B } e/ _V ) )
12	2 11	biimtrrid	|- ( -. ( A e/ _V \/ A = (/) ) -> ( -. B e. _V -> { f | f : A --> B } e/ _V ) )
13	12	imp	|- ( ( -. ( A e/ _V \/ A = (/) ) /\ -. B e. _V ) -> { f | f : A --> B } e/ _V )
14	1 13	sylbi	|- ( -. ( ( A e/ _V \/ A = (/) ) \/ B e. _V ) -> { f | f : A --> B } e/ _V )
15		df-nel	|- ( { f | f : A --> B } e/ _V <-> -. { f | f : A --> B } e. _V )
16	14 15	sylib	|- ( -. ( ( A e/ _V \/ A = (/) ) \/ B e. _V ) -> -. { f | f : A --> B } e. _V )
17	16	con4i	|- ( { f | f : A --> B } e. _V -> ( ( A e/ _V \/ A = (/) ) \/ B e. _V ) )
18		df-3or	|- ( ( A e/ _V \/ A = (/) \/ B e. _V ) <-> ( ( A e/ _V \/ A = (/) ) \/ B e. _V ) )
19	17 18	sylibr	|- ( { f | f : A --> B } e. _V -> ( A e/ _V \/ A = (/) \/ B e. _V ) )
20		fsetdmprc0	|- ( A e/ _V -> { f | f Fn A } = (/) )
21		ffn	|- ( f : A --> B -> f Fn A )
22	21	ss2abi	|- { f | f : A --> B } C_ { f | f Fn A }
23		sseq0	|- ( ( { f | f : A --> B } C_ { f | f Fn A } /\ { f | f Fn A } = (/) ) -> { f | f : A --> B } = (/) )
24	22 23	mpan	|- ( { f | f Fn A } = (/) -> { f | f : A --> B } = (/) )
25		0ex	|- (/) e. _V
26	24 25	eqeltrdi	|- ( { f | f Fn A } = (/) -> { f | f : A --> B } e. _V )
27	20 26	syl	|- ( A e/ _V -> { f | f : A --> B } e. _V )
28		feq2	|- ( A = (/) -> ( f : A --> B <-> f : (/) --> B ) )
29	28	abbidv	|- ( A = (/) -> { f | f : A --> B } = { f | f : (/) --> B } )
30		fset0	|- { f | f : (/) --> B } = { (/) }
31	29 30	eqtrdi	|- ( A = (/) -> { f | f : A --> B } = { (/) } )
32		p0ex	|- { (/) } e. _V
33	31 32	eqeltrdi	|- ( A = (/) -> { f | f : A --> B } e. _V )
34		fsetex	|- ( B e. _V -> { f | f : A --> B } e. _V )
35	27 33 34	3jaoi	|- ( ( A e/ _V \/ A = (/) \/ B e. _V ) -> { f | f : A --> B } e. _V )
36	19 35	impbii	|- ( { f | f : A --> B } e. _V <-> ( A e/ _V \/ A = (/) \/ B e. _V ) )