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	⊢ ( 𝐴 ∈ dom card → ( 𝐴 ∈ FinVII ↔ 𝐴 ∈ Fin ) )

Proof

Step	Hyp	Ref	Expression
1		isfin7-2	⊢ ( 𝐴 ∈ dom card → ( 𝐴 ∈ FinVII ↔ ( 𝐴 ∈ dom card → 𝐴 ∈ Fin ) ) )
2		biimt	⊢ ( 𝐴 ∈ dom card → ( 𝐴 ∈ Fin ↔ ( 𝐴 ∈ dom card → 𝐴 ∈ Fin ) ) )
3	1 2	bitr4d	⊢ ( 𝐴 ∈ dom card → ( 𝐴 ∈ FinVII ↔ 𝐴 ∈ Fin ) )