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 ∈ Fin ∧ B ∈ Fin → ¬ A ∖ B ∈ Fin

Proof

Step Hyp Ref Expression
1 unfi ⊢ A ∖ B ∈ Fin ∧ B ∈ Fin → A ∖ B ∪ B ∈ Fin
2 undif1 ⊢ A ∖ B ∪ B = A ∪ B
3 2 eleq1i ⊢ A ∖ B ∪ B ∈ Fin ↔ A ∪ B ∈ Fin
4 unfir ⊢ A ∪ B ∈ Fin → A ∈ Fin ∧ B ∈ Fin
5 4 simpld ⊢ A ∪ B ∈ Fin → A ∈ Fin
6 3 5 sylbi ⊢ A ∖ B ∪ B ∈ Fin → A ∈ Fin
7 1 6 syl ⊢ A ∖ B ∈ Fin ∧ B ∈ Fin → A ∈ Fin
8 7 expcom ⊢ B ∈ Fin → A ∖ B ∈ Fin → A ∈ Fin
9 8 con3d ⊢ B ∈ Fin → ¬ A ∈ Fin → ¬ A ∖ B ∈ Fin
10 9 impcom ⊢ ¬ A ∈ Fin ∧ B ∈ Fin → ¬ A ∖ B ∈ Fin