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})$

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 \to A \subseteq On$
5	1 4	ax-mp	$⊢ A \subseteq On$
6	3 5	eqsstri	$⊢ ran ({I ↾}_{A}) \subseteq On$
7		df-f	$⊢ ({I ↾}_{A}) : A ⟶ On \leftrightarrow (({I ↾}_{A}) Fn A \land ran ({I ↾}_{A}) \subseteq On)$
8	2 6 7	mpbir2an	$⊢ ({I ↾}_{A}) : A ⟶ On$
9		fvresi	$⊢ x \in A \to ({I ↾}_{A}) (x) = x$
10	9	adantr	$⊢ (x \in A \land y \in A) \to ({I ↾}_{A}) (x) = x$
11		fvresi	$⊢ y \in A \to ({I ↾}_{A}) (y) = y$
12	11	adantl	$⊢ (x \in A \land y \in A) \to ({I ↾}_{A}) (y) = y$
13	10 12	eleq12d	$⊢ (x \in A \land y \in A) \to (({I ↾}_{A}) (x) \in ({I ↾}_{A}) (y) \leftrightarrow x \in y)$
14	13	biimprd	$⊢ (x \in A \land y \in A) \to (x \in y \to ({I ↾}_{A}) (x) \in ({I ↾}_{A}) (y))$
15		dmresi	$⊢ dom ({I ↾}_{A}) = A$
16	8 1 14 15	issmo	$⊢ Smo ({I ↾}_{A})$

Metamath Proof Explorer