Theorem fsetdmprc0

Description: The set of functions with a proper class as domain is empty. (Contributed by AV, 22-Aug-2024)

	Ref	Expression
Assertion	fsetdmprc0	⊢ ( 𝐴 ∉ V → { 𝑓 ∣ 𝑓 Fn 𝐴 } = ∅ )

Proof

Step	Hyp	Ref	Expression
1		df-nel	⊢ ( 𝐴 ∉ V ↔ ¬ 𝐴 ∈ V )
2		vex	⊢ 𝑔 ∈ V
3	2	a1i	⊢ ( 𝑔 Fn 𝐴 → 𝑔 ∈ V )
4		id	⊢ ( 𝑔 Fn 𝐴 → 𝑔 Fn 𝐴 )
5	3 4	fndmexd	⊢ ( 𝑔 Fn 𝐴 → 𝐴 ∈ V )
6	5	con3i	⊢ ( ¬ 𝐴 ∈ V → ¬ 𝑔 Fn 𝐴 )
7	1 6	sylbi	⊢ ( 𝐴 ∉ V → ¬ 𝑔 Fn 𝐴 )
8	7	alrimiv	⊢ ( 𝐴 ∉ V → ∀ 𝑔 ¬ 𝑔 Fn 𝐴 )
9		fneq1	⊢ ( 𝑓 = 𝑔 → ( 𝑓 Fn 𝐴 ↔ 𝑔 Fn 𝐴 ) )
10	9	ab0w	⊢ ( { 𝑓 ∣ 𝑓 Fn 𝐴 } = ∅ ↔ ∀ 𝑔 ¬ 𝑔 Fn 𝐴 )
11	8 10	sylibr	⊢ ( 𝐴 ∉ V → { 𝑓 ∣ 𝑓 Fn 𝐴 } = ∅ )