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 )