Metamath Proof Explorer

Theorem relprcnfsupp

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

Ref Expression
Assertion relprcnfsupp 
|- ( -. A e. _V -> -. A finSupp Z )

Proof

Step Hyp Ref Expression
1 relfsupp 
 |-  Rel finSupp
2 1 brrelex1i 
 |-  ( A finSupp Z -> A e. _V )
3 2 con3i 
 |-  ( -. A e. _V -> -. A finSupp Z )