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

Metamath Proof Explorer

Theorem iordsmo

Description: The identity relation restricted to the ordinals is a strictly monotone function. (Contributed by Andrew Salmon, 16-Nov-2011)

Ref Expression
Hypothesis iordsmo.1 ⊢ Ord 𝐴
Assertion iordsmo Smo ( I ↾ 𝐴 )

Proof

Step Hyp Ref Expression
1 iordsmo.1 ⊢ Ord 𝐴
2 fnresi ⊢ ( I ↾ 𝐴 ) Fn 𝐴
3 rnresi ⊢ ran ( I ↾ 𝐴 ) = 𝐴
4 ordsson ⊢ ( Ord 𝐴 → 𝐴 ⊆ On )
5 1 4 ax-mp ⊢ 𝐴 ⊆ On
6 3 5 eqsstri ⊢ ran ( I ↾ 𝐴 ) ⊆ On
7 df-f ⊢ ( ( I ↾ 𝐴 ) : 𝐴 ⟶ On ↔ ( ( I ↾ 𝐴 ) Fn 𝐴 ∧ ran ( I ↾ 𝐴 ) ⊆ On ) )
8 2 6 7 mpbir2an ⊢ ( I ↾ 𝐴 ) : 𝐴 ⟶ On
9 fvresi ⊢ ( 𝑥 ∈ 𝐴 → ( ( I ↾ 𝐴 ) ‘ 𝑥 ) = 𝑥 )
10 9 adantr ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( I ↾ 𝐴 ) ‘ 𝑥 ) = 𝑥 )
11 fvresi ⊢ ( 𝑦 ∈ 𝐴 → ( ( I ↾ 𝐴 ) ‘ 𝑦 ) = 𝑦 )
12 11 adantl ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( I ↾ 𝐴 ) ‘ 𝑦 ) = 𝑦 )
13 10 12 eleq12d ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( I ↾ 𝐴 ) ‘ 𝑥 ) ∈ ( ( I ↾ 𝐴 ) ‘ 𝑦 ) ↔ 𝑥 ∈ 𝑦 ) )
14 13 biimprd ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑦 → ( ( I ↾ 𝐴 ) ‘ 𝑥 ) ∈ ( ( I ↾ 𝐴 ) ‘ 𝑦 ) ) )
15 dmresi ⊢ dom ( I ↾ 𝐴 ) = 𝐴
16 8 1 14 15 issmo ⊢ Smo ( I ↾ 𝐴 )