Metamath Proof Explorer


Theorem fin2inf

Description: This (useless) theorem, which was proved without the Axiom of Infinity, demonstrates an artifact of our definition of binary relation, which is meaningful only when its arguments exist. In particular, the antecedent cannot be satisfied unless _om exists. (Contributed by NM, 13-Nov-2003)

Ref Expression
Assertion fin2inf
|- ( A ~< _om -> _om e. _V )

Proof

Step Hyp Ref Expression
1 relsdom
 |-  Rel ~<
2 1 brrelex2i
 |-  ( A ~< _om -> _om e. _V )