This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem relprcnfsupp

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

		Ref	Expression
	Assertion	relprcnfsupp	$⊢ \neg A \in V \to \neg {finSupp}_{Z} (A)$

Step	Hyp	Ref	Expression
1		relfsupp	$⊢ Rel finSupp$
2	1	brrelex1i	$⊢ {finSupp}_{Z} (A) \to A \in V$
3	2	con3i	$⊢ \neg A \in V \to \neg {finSupp}_{Z} (A)$