Theorem relprcnfsupp

Description: A proper class is never finitely supported. (Contributed by AV, 7-Jun-2019)

	Ref	Expression
Assertion	relprcnfsupp	⊢ ( ¬ 𝐴 ∈ V → ¬ 𝐴 finSupp 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		relfsupp	⊢ Rel finSupp
2	1	brrelex1i	⊢ ( 𝐴 finSupp 𝑍 → 𝐴 ∈ V )
3	2	con3i	⊢ ( ¬ 𝐴 ∈ V → ¬ 𝐴 finSupp 𝑍 )