Theorem isfin2

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

	Ref	Expression
Assertion	isfin2	|- ( A e. V -> ( A e. Fin2 <-> A. y e. ~P ~P A ( ( y =/= (/) /\ [C.] Or y ) -> U. y e. y ) ) )

Proof

Step	Hyp	Ref	Expression
1		pweq	|- ( x = A -> ~P x = ~P A )
2	1	pweqd	|- ( x = A -> ~P ~P x = ~P ~P A )
3	2	raleqdv	|- ( x = A -> ( A. y e. ~P ~P x ( ( y =/= (/) /\ [C.] Or y ) -> U. y e. y ) <-> A. y e. ~P ~P A ( ( y =/= (/) /\ [C.] Or y ) -> U. y e. y ) ) )
4		df-fin2	|- Fin2 = { x | A. y e. ~P ~P x ( ( y =/= (/) /\ [C.] Or y ) -> U. y e. y ) }
5	3 4	elab2g	|- ( A e. V -> ( A e. Fin2 <-> A. y e. ~P ~P A ( ( y =/= (/) /\ [C.] Or y ) -> U. y e. y ) ) )