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

Metamath Proof Explorer

Theorem difinf

Description: An infinite set A minus a finite set is infinite. (Contributed by FL, 3-Aug-2009)

Ref Expression
Assertion difinf 
|- ( ( -. A e. Fin /\ B e. Fin ) -> -. ( A \ B ) e. Fin )

Proof

Step Hyp Ref Expression
1 unfi 
 |-  ( ( ( A \ B ) e. Fin /\ B e. Fin ) -> ( ( A \ B ) u. B ) e. Fin )
2 undif1 
 |-  ( ( A \ B ) u. B ) = ( A u. B )
3 2 eleq1i 
 |-  ( ( ( A \ B ) u. B ) e. Fin <-> ( A u. B ) e. Fin )
4 unfir 
 |-  ( ( A u. B ) e. Fin -> ( A e. Fin /\ B e. Fin ) )
5 4 simpld 
 |-  ( ( A u. B ) e. Fin -> A e. Fin )
6 3 5 sylbi 
 |-  ( ( ( A \ B ) u. B ) e. Fin -> A e. Fin )
7 1 6 syl 
 |-  ( ( ( A \ B ) e. Fin /\ B e. Fin ) -> A e. Fin )
8 7 expcom 
 |-  ( B e. Fin -> ( ( A \ B ) e. Fin -> A e. Fin ) )
9 8 con3d 
 |-  ( B e. Fin -> ( -. A e. Fin -> -. ( A \ B ) e. Fin ) )
10 9 impcom 
 |-  ( ( -. A e. Fin /\ B e. Fin ) -> -. ( A \ B ) e. Fin )