Theorem isfin3

Description: Definition of a III-finite set. (Contributed by Stefan O'Rear, 16-May-2015)

	Ref	Expression
Assertion	isfin3	|- ( A e. Fin3 <-> ~P A e. Fin4 )

Proof

Step	Hyp	Ref	Expression
1		df-fin3	|- Fin3 = { x | ~P x e. Fin4 }
2	1	eleq2i	|- ( A e. Fin3 <-> A e. { x | ~P x e. Fin4 } )
3		pwexr	|- ( ~P A e. Fin4 -> A e. _V )
4		pweq	|- ( x = A -> ~P x = ~P A )
5	4	eleq1d	|- ( x = A -> ( ~P x e. Fin4 <-> ~P A e. Fin4 ) )
6	3 5	elab3	|- ( A e. { x | ~P x e. Fin4 } <-> ~P A e. Fin4 )
7	2 6	bitri	|- ( A e. Fin3 <-> ~P A e. Fin4 )