Metamath Proof Explorer


Theorem fin17

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

Ref Expression
Assertion fin17 ( 𝐴 ∈ Fin → 𝐴 ∈ FinVII )

Proof

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