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

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 )