Theorem isfi

Description: Express " A is finite." Definition 10.29 of TakeutiZaring p. 91 (whose " Fin " is a predicate instead of a class). (Contributed by NM, 22-Aug-2008)

	Ref	Expression
Assertion	isfi	|- ( A e. Fin <-> E. x e. _om A ~~ x )

Proof

Step	Hyp	Ref	Expression
1		df-fin	|- Fin = { y | E. x e. _om y ~~ x }
2	1	eleq2i	|- ( A e. Fin <-> A e. { y | E. x e. _om y ~~ x } )
3		relen	|- Rel ~~
4	3	brrelex1i	|- ( A ~~ x -> A e. _V )
5	4	rexlimivw	|- ( E. x e. _om A ~~ x -> A e. _V )
6		breq1	|- ( y = A -> ( y ~~ x <-> A ~~ x ) )
7	6	rexbidv	|- ( y = A -> ( E. x e. _om y ~~ x <-> E. x e. _om A ~~ x ) )
8	5 7	elab3	|- ( A e. { y | E. x e. _om y ~~ x } <-> E. x e. _om A ~~ x )
9	2 8	bitri	|- ( A e. Fin <-> E. x e. _om A ~~ x )