Metamath Proof Explorer

Theorem omsmo

Description: A strictly monotonic ordinal function on the set of natural numbers is one-to-one. (Contributed by NM, 30-Nov-2003) (Revised by David Abernethy, 1-Jan-2014)

Ref Expression
Assertion omsmo ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) → 𝐹 : ω –1-1→ 𝐴 )

Proof

Step Hyp Ref Expression
1 simplr ⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) → 𝐹 : ω ⟶ 𝐴 )
2 omsmolem ⊢ ( 𝑧 ∈ ω → ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) → ( 𝑦 ∈ 𝑧 → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑧 ) ) ) )
3 2 adantl ⊢ ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) → ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) → ( 𝑦 ∈ 𝑧 → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑧 ) ) ) )
4 3 imp ⊢ ( ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) ∧ ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) ) → ( 𝑦 ∈ 𝑧 → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑧 ) ) )
5 omsmolem ⊢ ( 𝑦 ∈ ω → ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) → ( 𝑧 ∈ 𝑦 → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) )
6 5 adantr ⊢ ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) → ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) → ( 𝑧 ∈ 𝑦 → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) )
7 6 imp ⊢ ( ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) ∧ ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) ) → ( 𝑧 ∈ 𝑦 → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑦 ) ) )
8 4 7 orim12d ⊢ ( ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) ∧ ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) ) → ( ( 𝑦 ∈ 𝑧 ∨ 𝑧 ∈ 𝑦 ) → ( ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑧 ) ∨ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) )
9 8 ancoms ⊢ ( ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) ) → ( ( 𝑦 ∈ 𝑧 ∨ 𝑧 ∈ 𝑦 ) → ( ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑧 ) ∨ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) )
10 9 con3d ⊢ ( ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) ) → ( ¬ ( ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑧 ) ∨ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑦 ) ) → ¬ ( 𝑦 ∈ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) )
11 ffvelrn ⊢ ( ( 𝐹 : ω ⟶ 𝐴 ∧ 𝑦 ∈ ω ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 )
12 ssel ⊢ ( 𝐴 ⊆ On → ( ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 → ( 𝐹 ‘ 𝑦 ) ∈ On ) )
13 11 12 syl5 ⊢ ( 𝐴 ⊆ On → ( ( 𝐹 : ω ⟶ 𝐴 ∧ 𝑦 ∈ ω ) → ( 𝐹 ‘ 𝑦 ) ∈ On ) )
14 13 expdimp ⊢ ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) → ( 𝑦 ∈ ω → ( 𝐹 ‘ 𝑦 ) ∈ On ) )
15 eloni ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ On → Ord ( 𝐹 ‘ 𝑦 ) )
16 14 15 syl6 ⊢ ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) → ( 𝑦 ∈ ω → Ord ( 𝐹 ‘ 𝑦 ) ) )
17 ffvelrn ⊢ ( ( 𝐹 : ω ⟶ 𝐴 ∧ 𝑧 ∈ ω ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝐴 )
18 ssel ⊢ ( 𝐴 ⊆ On → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝐴 → ( 𝐹 ‘ 𝑧 ) ∈ On ) )
19 17 18 syl5 ⊢ ( 𝐴 ⊆ On → ( ( 𝐹 : ω ⟶ 𝐴 ∧ 𝑧 ∈ ω ) → ( 𝐹 ‘ 𝑧 ) ∈ On ) )
20 19 expdimp ⊢ ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) → ( 𝑧 ∈ ω → ( 𝐹 ‘ 𝑧 ) ∈ On ) )
21 eloni ⊢ ( ( 𝐹 ‘ 𝑧 ) ∈ On → Ord ( 𝐹 ‘ 𝑧 ) )
22 20 21 syl6 ⊢ ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) → ( 𝑧 ∈ ω → Ord ( 𝐹 ‘ 𝑧 ) ) )
23 16 22 anim12d ⊢ ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) → ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) → ( Ord ( 𝐹 ‘ 𝑦 ) ∧ Ord ( 𝐹 ‘ 𝑧 ) ) ) )
24 23 imp ⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) ) → ( Ord ( 𝐹 ‘ 𝑦 ) ∧ Ord ( 𝐹 ‘ 𝑧 ) ) )
25 ordtri3 ⊢ ( ( Ord ( 𝐹 ‘ 𝑦 ) ∧ Ord ( 𝐹 ‘ 𝑧 ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ↔ ¬ ( ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑧 ) ∨ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) )
26 24 25 syl ⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ↔ ¬ ( ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑧 ) ∨ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) )
27 26 adantlr ⊢ ( ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ↔ ¬ ( ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑧 ) ∨ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) )
28 nnord ⊢ ( 𝑦 ∈ ω → Ord 𝑦 )
29 nnord ⊢ ( 𝑧 ∈ ω → Ord 𝑧 )
30 ordtri3 ⊢ ( ( Ord 𝑦 ∧ Ord 𝑧 ) → ( 𝑦 = 𝑧 ↔ ¬ ( 𝑦 ∈ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) )
31 28 29 30 syl2an ⊢ ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) → ( 𝑦 = 𝑧 ↔ ¬ ( 𝑦 ∈ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) )
32 31 adantl ⊢ ( ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) ) → ( 𝑦 = 𝑧 ↔ ¬ ( 𝑦 ∈ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) )
33 10 27 32 3imtr4d ⊢ ( ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) → 𝑦 = 𝑧 ) )
34 33 ralrimivva ⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) → ∀ 𝑦 ∈ ω ∀ 𝑧 ∈ ω ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) → 𝑦 = 𝑧 ) )
35 dff13 ⊢ ( 𝐹 : ω –1-1→ 𝐴 ↔ ( 𝐹 : ω ⟶ 𝐴 ∧ ∀ 𝑦 ∈ ω ∀ 𝑧 ∈ ω ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) → 𝑦 = 𝑧 ) ) )
36 1 34 35 sylanbrc ⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) → 𝐹 : ω –1-1→ 𝐴 )