Metamath Proof Explorer

Theorem fin71num

Description: A well-orderable set is VII-finite iff it is I-finite. Thus, even without choice, on the class of well-orderable sets all eight definitions of finite set coincide. (Contributed by Mario Carneiro, 18-May-2015)

Ref Expression
Assertion fin71num ⊢ A ∈ dom ⁡ card → A ∈ FinVII ↔ A ∈ Fin

Proof

Step Hyp Ref Expression
1 isfin7-2 ⊢ A ∈ dom ⁡ card → A ∈ FinVII ↔ A ∈ dom ⁡ card → A ∈ Fin
2 biimt ⊢ A ∈ dom ⁡ card → A ∈ Fin ↔ A ∈ dom ⁡ card → A ∈ Fin
3 1 2 bitr4d ⊢ A ∈ dom ⁡ card → A ∈ FinVII ↔ A ∈ Fin