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 ↾ 𝐴 )