This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )