Metamath Proof Explorer

Theorem fin17

Description: Every I-finite set is VII-finite. (Contributed by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion fin17 ⊢ A ∈ Fin → A ∈ FinVII

Proof

Step Hyp Ref Expression
1 eldif ⊢ b ∈ On ∖ ω ↔ b ∈ On ∧ ¬ b ∈ ω
2 enfi ⊢ A ≈ b → A ∈ Fin ↔ b ∈ Fin
3 onfin ⊢ b ∈ On → b ∈ Fin ↔ b ∈ ω
4 2 3 sylan9bbr ⊢ b ∈ On ∧ A ≈ b → A ∈ Fin ↔ b ∈ ω
5 4 biimpd ⊢ b ∈ On ∧ A ≈ b → A ∈ Fin → b ∈ ω
6 5 con3d ⊢ b ∈ On ∧ A ≈ b → ¬ b ∈ ω → ¬ A ∈ Fin
7 6 impancom ⊢ b ∈ On ∧ ¬ b ∈ ω → A ≈ b → ¬ A ∈ Fin
8 1 7 sylbi ⊢ b ∈ On ∖ ω → A ≈ b → ¬ A ∈ Fin
9 8 rexlimiv ⊢ ∃ b ∈ On ∖ ω A ≈ b → ¬ A ∈ Fin
10 9 con2i ⊢ A ∈ Fin → ¬ ∃ b ∈ On ∖ ω A ≈ b
11 isfin7 ⊢ A ∈ Fin → A ∈ FinVII ↔ ¬ ∃ b ∈ On ∖ ω A ≈ b
12 10 11 mpbird ⊢ A ∈ Fin → A ∈ FinVII