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 ⁡ A
Assertion iordsmo ⊢ Smo ⁡ I ↾ A

Proof

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