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	⊢ ( { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V ↔ ( 𝐴 ∉ V ∨ 𝐴 = ∅ ∨ 𝐵 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		ioran	⊢ ( ¬ ( ( 𝐴 ∉ V ∨ 𝐴 = ∅ ) ∨ 𝐵 ∈ V ) ↔ ( ¬ ( 𝐴 ∉ V ∨ 𝐴 = ∅ ) ∧ ¬ 𝐵 ∈ V ) )
2		df-nel	⊢ ( 𝐵 ∉ V ↔ ¬ 𝐵 ∈ V )
3		ioran	⊢ ( ¬ ( 𝐴 ∉ V ∨ 𝐴 = ∅ ) ↔ ( ¬ 𝐴 ∉ V ∧ ¬ 𝐴 = ∅ ) )
4		nnel	⊢ ( ¬ 𝐴 ∉ V ↔ 𝐴 ∈ V )
5		df-ne	⊢ ( 𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅ )
6	5	bicomi	⊢ ( ¬ 𝐴 = ∅ ↔ 𝐴 ≠ ∅ )
7	4 6	anbi12i	⊢ ( ( ¬ 𝐴 ∉ V ∧ ¬ 𝐴 = ∅ ) ↔ ( 𝐴 ∈ V ∧ 𝐴 ≠ ∅ ) )
8	3 7	bitri	⊢ ( ¬ ( 𝐴 ∉ V ∨ 𝐴 = ∅ ) ↔ ( 𝐴 ∈ V ∧ 𝐴 ≠ ∅ ) )
9		fsetprcnex	⊢ ( ( ( 𝐴 ∈ V ∧ 𝐴 ≠ ∅ ) ∧ 𝐵 ∉ V ) → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∉ V )
10	9	ex	⊢ ( ( 𝐴 ∈ V ∧ 𝐴 ≠ ∅ ) → ( 𝐵 ∉ V → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∉ V ) )
11	8 10	sylbi	⊢ ( ¬ ( 𝐴 ∉ V ∨ 𝐴 = ∅ ) → ( 𝐵 ∉ V → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∉ V ) )
12	2 11	biimtrrid	⊢ ( ¬ ( 𝐴 ∉ V ∨ 𝐴 = ∅ ) → ( ¬ 𝐵 ∈ V → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∉ V ) )
13	12	imp	⊢ ( ( ¬ ( 𝐴 ∉ V ∨ 𝐴 = ∅ ) ∧ ¬ 𝐵 ∈ V ) → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∉ V )
14	1 13	sylbi	⊢ ( ¬ ( ( 𝐴 ∉ V ∨ 𝐴 = ∅ ) ∨ 𝐵 ∈ V ) → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∉ V )
15		df-nel	⊢ ( { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∉ V ↔ ¬ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V )
16	14 15	sylib	⊢ ( ¬ ( ( 𝐴 ∉ V ∨ 𝐴 = ∅ ) ∨ 𝐵 ∈ V ) → ¬ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V )
17	16	con4i	⊢ ( { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V → ( ( 𝐴 ∉ V ∨ 𝐴 = ∅ ) ∨ 𝐵 ∈ V ) )
18		df-3or	⊢ ( ( 𝐴 ∉ V ∨ 𝐴 = ∅ ∨ 𝐵 ∈ V ) ↔ ( ( 𝐴 ∉ V ∨ 𝐴 = ∅ ) ∨ 𝐵 ∈ V ) )
19	17 18	sylibr	⊢ ( { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V → ( 𝐴 ∉ V ∨ 𝐴 = ∅ ∨ 𝐵 ∈ V ) )
20		fsetdmprc0	⊢ ( 𝐴 ∉ V → { 𝑓 ∣ 𝑓 Fn 𝐴 } = ∅ )
21		ffn	⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → 𝑓 Fn 𝐴 )
22	21	ss2abi	⊢ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ⊆ { 𝑓 ∣ 𝑓 Fn 𝐴 }
23		sseq0	⊢ ( ( { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ⊆ { 𝑓 ∣ 𝑓 Fn 𝐴 } ∧ { 𝑓 ∣ 𝑓 Fn 𝐴 } = ∅ ) → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } = ∅ )
24	22 23	mpan	⊢ ( { 𝑓 ∣ 𝑓 Fn 𝐴 } = ∅ → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } = ∅ )
25		0ex	⊢ ∅ ∈ V
26	24 25	eqeltrdi	⊢ ( { 𝑓 ∣ 𝑓 Fn 𝐴 } = ∅ → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V )
27	20 26	syl	⊢ ( 𝐴 ∉ V → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V )
28		feq2	⊢ ( 𝐴 = ∅ → ( 𝑓 : 𝐴 ⟶ 𝐵 ↔ 𝑓 : ∅ ⟶ 𝐵 ) )
29	28	abbidv	⊢ ( 𝐴 = ∅ → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } = { 𝑓 ∣ 𝑓 : ∅ ⟶ 𝐵 } )
30		fset0	⊢ { 𝑓 ∣ 𝑓 : ∅ ⟶ 𝐵 } = { ∅ }
31	29 30	eqtrdi	⊢ ( 𝐴 = ∅ → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } = { ∅ } )
32		p0ex	⊢ { ∅ } ∈ V
33	31 32	eqeltrdi	⊢ ( 𝐴 = ∅ → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V )
34		fsetex	⊢ ( 𝐵 ∈ V → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V )
35	27 33 34	3jaoi	⊢ ( ( 𝐴 ∉ V ∨ 𝐴 = ∅ ∨ 𝐵 ∈ V ) → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V )
36	19 35	impbii	⊢ ( { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V ↔ ( 𝐴 ∉ V ∨ 𝐴 = ∅ ∨ 𝐵 ∈ V ) )