Theorem infinfnum

Description: Equivalence between two infiniteness criteria for numerable sets. (Contributed by BTernaryTau, 15-Jul-2026)

	Ref	Expression
Assertion	infinfnum	⊢ ( 𝐴 ∈ dom card → ( ¬ 𝐴 ∈ Fin ↔ ω ≼ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		isfin4-2	⊢ ( 𝐴 ∈ dom card → ( 𝐴 ∈ FinIV ↔ ¬ ω ≼ 𝐴 ) )
2	1	con2bid	⊢ ( 𝐴 ∈ dom card → ( ω ≼ 𝐴 ↔ ¬ 𝐴 ∈ FinIV ) )
3		fin45	⊢ ( 𝐴 ∈ FinIV → 𝐴 ∈ FinV )
4		fin56	⊢ ( 𝐴 ∈ FinV → 𝐴 ∈ FinVI )
5		fin67	⊢ ( 𝐴 ∈ FinVI → 𝐴 ∈ FinVII )
6	3 4 5	3syl	⊢ ( 𝐴 ∈ FinIV → 𝐴 ∈ FinVII )
7		fin71num	⊢ ( 𝐴 ∈ dom card → ( 𝐴 ∈ FinVII ↔ 𝐴 ∈ Fin ) )
8	6 7	imbitrid	⊢ ( 𝐴 ∈ dom card → ( 𝐴 ∈ FinIV → 𝐴 ∈ Fin ) )
9		fin12	⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ FinII )
10		fin23	⊢ ( 𝐴 ∈ FinII → 𝐴 ∈ FinIII )
11		fin34	⊢ ( 𝐴 ∈ FinIII → 𝐴 ∈ FinIV )
12	9 10 11	3syl	⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ FinIV )
13	8 12	impbid1	⊢ ( 𝐴 ∈ dom card → ( 𝐴 ∈ FinIV ↔ 𝐴 ∈ Fin ) )
14	13	notbid	⊢ ( 𝐴 ∈ dom card → ( ¬ 𝐴 ∈ FinIV ↔ ¬ 𝐴 ∈ Fin ) )
15	2 14	bitr2d	⊢ ( 𝐴 ∈ dom card → ( ¬ 𝐴 ∈ Fin ↔ ω ≼ 𝐴 ) )