Theorem isfin1a

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

	Ref	Expression
Assertion	isfin1a	|- ( A e. V -> ( A e. Fin1a <-> A. y e. ~P A ( y e. Fin \/ ( A \ y ) e. Fin ) ) )

Proof

Step	Hyp	Ref	Expression
1		pweq	|- ( x = A -> ~P x = ~P A )
2		difeq1	|- ( x = A -> ( x \ y ) = ( A \ y ) )
3	2	eleq1d	|- ( x = A -> ( ( x \ y ) e. Fin <-> ( A \ y ) e. Fin ) )
4	3	orbi2d	|- ( x = A -> ( ( y e. Fin \/ ( x \ y ) e. Fin ) <-> ( y e. Fin \/ ( A \ y ) e. Fin ) ) )
5	1 4	raleqbidv	|- ( x = A -> ( A. y e. ~P x ( y e. Fin \/ ( x \ y ) e. Fin ) <-> A. y e. ~P A ( y e. Fin \/ ( A \ y ) e. Fin ) ) )
6		df-fin1a	|- Fin1a = { x | A. y e. ~P x ( y e. Fin \/ ( x \ y ) e. Fin ) }
7	5 6	elab2g	|- ( A e. V -> ( A e. Fin1a <-> A. y e. ~P A ( y e. Fin \/ ( A \ y ) e. Fin ) ) )