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 )