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

Metamath Proof Explorer

Theorem tfsnfin2

Description: A transfinite sequence is infinite iff its domain is greater than or equal to omega. Theorem 5 in Grzegorz Bancerek, "Epsilon Numbers and Cantor Normal Form", Formalized Mathematics, Vol. 17, No. 4, Pages 249–256, 2009. DOI: 10.2478/v10037-009-0032-8 (Contributed by RP, 1-Mar-2025)

Ref Expression
Assertion tfsnfin2 ( ( 𝐴 Fn 𝐵 ∧ Ord 𝐵 ) → ( ¬ 𝐴 ∈ Fin ↔ ω ⊆ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fnfun ⊢ ( 𝐴 Fn 𝐵 → Fun 𝐴 )
2 fundmfibi ⊢ ( Fun 𝐴 → ( 𝐴 ∈ Fin ↔ dom 𝐴 ∈ Fin ) )
3 1 2 syl ⊢ ( 𝐴 Fn 𝐵 → ( 𝐴 ∈ Fin ↔ dom 𝐴 ∈ Fin ) )
4 fndm ⊢ ( 𝐴 Fn 𝐵 → dom 𝐴 = 𝐵 )
5 4 eleq1d ⊢ ( 𝐴 Fn 𝐵 → ( dom 𝐴 ∈ Fin ↔ 𝐵 ∈ Fin ) )
6 3 5 bitrd ⊢ ( 𝐴 Fn 𝐵 → ( 𝐴 ∈ Fin ↔ 𝐵 ∈ Fin ) )
7 ordfin ⊢ ( Ord 𝐵 → ( 𝐵 ∈ Fin ↔ 𝐵 ∈ ω ) )
8 6 7 sylan9bb ⊢ ( ( 𝐴 Fn 𝐵 ∧ Ord 𝐵 ) → ( 𝐴 ∈ Fin ↔ 𝐵 ∈ ω ) )
9 8 notbid ⊢ ( ( 𝐴 Fn 𝐵 ∧ Ord 𝐵 ) → ( ¬ 𝐴 ∈ Fin ↔ ¬ 𝐵 ∈ ω ) )
10 ordom ⊢ Ord ω
11 ordtri1 ⊢ ( ( Ord ω ∧ Ord 𝐵 ) → ( ω ⊆ 𝐵 ↔ ¬ 𝐵 ∈ ω ) )
12 10 11 mpan ⊢ ( Ord 𝐵 → ( ω ⊆ 𝐵 ↔ ¬ 𝐵 ∈ ω ) )
13 12 adantl ⊢ ( ( 𝐴 Fn 𝐵 ∧ Ord 𝐵 ) → ( ω ⊆ 𝐵 ↔ ¬ 𝐵 ∈ ω ) )
14 9 13 bitr4d ⊢ ( ( 𝐴 Fn 𝐵 ∧ Ord 𝐵 ) → ( ¬ 𝐴 ∈ Fin ↔ ω ⊆ 𝐵 ) )