Theorem fsetprcnex

Description: The class of all functions from a nonempty set A into a proper class B is not a set. If one of the preconditions is not fufilled, then { f | f : A --> B } is a set, see fsetdmprc0 for A e/V , fset0 for A = (/) , and fsetex for B e. V , see also fsetexb . (Contributed by AV, 14-Sep-2024) (Proof shortened by BJ, 15-Sep-2024)

	Ref	Expression
Assertion	fsetprcnex	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) ∧ 𝐵 ∉ V ) → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∉ V )

Proof

Step	Hyp	Ref	Expression
1		n0	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑎 𝑎 ∈ 𝐴 )
2		feq1	⊢ ( 𝑓 = 𝑚 → ( 𝑓 : 𝐴 ⟶ 𝐵 ↔ 𝑚 : 𝐴 ⟶ 𝐵 ) )
3	2	cbvabv	⊢ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } = { 𝑚 ∣ 𝑚 : 𝐴 ⟶ 𝐵 }
4		fveq1	⊢ ( 𝑔 = 𝑛 → ( 𝑔 ‘ 𝑎 ) = ( 𝑛 ‘ 𝑎 ) )
5	4	cbvmptv	⊢ ( 𝑔 ∈ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ↦ ( 𝑔 ‘ 𝑎 ) ) = ( 𝑛 ∈ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ↦ ( 𝑛 ‘ 𝑎 ) )
6	3 5	fsetfocdm	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑔 ∈ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ↦ ( 𝑔 ‘ 𝑎 ) ) : { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } –onto→ 𝐵 )
7		fornex	⊢ ( { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V → ( ( 𝑔 ∈ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ↦ ( 𝑔 ‘ 𝑎 ) ) : { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } –onto→ 𝐵 → 𝐵 ∈ V ) )
8	6 7	syl5com	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑎 ∈ 𝐴 ) → ( { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V → 𝐵 ∈ V ) )
9	8	nelcon3d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑎 ∈ 𝐴 ) → ( 𝐵 ∉ V → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∉ V ) )
10	9	expcom	⊢ ( 𝑎 ∈ 𝐴 → ( 𝐴 ∈ 𝑉 → ( 𝐵 ∉ V → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∉ V ) ) )
11	10	exlimiv	⊢ ( ∃ 𝑎 𝑎 ∈ 𝐴 → ( 𝐴 ∈ 𝑉 → ( 𝐵 ∉ V → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∉ V ) ) )
12	1 11	sylbi	⊢ ( 𝐴 ≠ ∅ → ( 𝐴 ∈ 𝑉 → ( 𝐵 ∉ V → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∉ V ) ) )
13	12	impcom	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) → ( 𝐵 ∉ V → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∉ V ) )
14	13	imp	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) ∧ 𝐵 ∉ V ) → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∉ V )