# Metamath Proof Explorer

## 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
` |-  ( z = x -> ~P z = ~P x )`
2 1 pweqd
` |-  ( z = x -> ~P ~P z = ~P ~P x )`
3 2 raleqdv
` |-  ( z = x -> ( A. y e. ~P ~P z ( ( y =/= (/) /\ [C.] Or y ) -> U. y e. y ) <-> A. y e. ~P ~P x ( ( y =/= (/) /\ [C.] Or y ) -> U. y e. y ) ) )`
4 pweq
` |-  ( x = A -> ~P x = ~P A )`
5 4 pweqd
` |-  ( x = A -> ~P ~P x = ~P ~P A )`
6 5 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 ) ) )`
7 df-fin2
` |-  Fin2 = { z | A. y e. ~P ~P z ( ( y =/= (/) /\ [C.] Or y ) -> U. y e. y ) }`
8 3 6 7 elab2gw
` |-  ( A e. V -> ( A e. Fin2 <-> A. y e. ~P ~P A ( ( y =/= (/) /\ [C.] Or y ) -> U. y e. y ) ) )`