Metamath Proof Explorer

Theorem fin1ai

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

Ref Expression
Assertion fin1ai 
|- ( ( A e. Fin1a /\ X C_ A ) -> ( X e. Fin \/ ( A \ X ) e. Fin ) )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( x = X -> ( x e. Fin <-> X e. Fin ) )
2 difeq2 
 |-  ( x = X -> ( A \ x ) = ( A \ X ) )
3 2 eleq1d 
 |-  ( x = X -> ( ( A \ x ) e. Fin <-> ( A \ X ) e. Fin ) )
4 1 3 orbi12d 
 |-  ( x = X -> ( ( x e. Fin \/ ( A \ x ) e. Fin ) <-> ( X e. Fin \/ ( A \ X ) e. Fin ) ) )
5 isfin1a 
 |-  ( A e. Fin1a -> ( A e. Fin1a <-> A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin ) ) )
6 5 ibi 
 |-  ( A e. Fin1a -> A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin ) )
7 6 adantr 
 |-  ( ( A e. Fin1a /\ X C_ A ) -> A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin ) )
8 elpw2g 
 |-  ( A e. Fin1a -> ( X e. ~P A <-> X C_ A ) )
9 8 biimpar 
 |-  ( ( A e. Fin1a /\ X C_ A ) -> X e. ~P A )
10 4 7 9 rspcdva 
 |-  ( ( A e. Fin1a /\ X C_ A ) -> ( X e. Fin \/ ( A \ X ) e. Fin ) )