smores

Description: A strictly monotone function restricted to an ordinal remains strictly monotone. (Contributed by Andrew Salmon, 16-Nov-2011) (Proof shortened by Mario Carneiro, 5-Dec-2016)

		Ref	Expression
	Assertion	smores	$⊢ (Smo A \land B \in dom A) \to Smo ({A ↾}_{B})$

Proof

Step	Hyp	Ref	Expression
1		funres	$⊢ Fun A \to Fun ({A ↾}_{B})$
2		funfn	$⊢ Fun A \leftrightarrow A Fn dom A$
3		funfn	$⊢ Fun ({A ↾}_{B}) \leftrightarrow ({A ↾}_{B}) Fn dom ({A ↾}_{B})$
4	1 2 3	3imtr3i	$⊢ A Fn dom A \to ({A ↾}_{B}) Fn dom ({A ↾}_{B})$
5		resss	$⊢ {A ↾}_{B} \subseteq A$
6	5	rnssi	$⊢ ran ({A ↾}_{B}) \subseteq ran A$
7		sstr	$⊢ (ran ({A ↾}_{B}) \subseteq ran A \land ran A \subseteq On) \to ran ({A ↾}_{B}) \subseteq On$
8	6 7	mpan	$⊢ ran A \subseteq On \to ran ({A ↾}_{B}) \subseteq On$
9	4 8	anim12i	$⊢ (A Fn dom A \land ran A \subseteq On) \to (({A ↾}_{B}) Fn dom ({A ↾}_{B}) \land ran ({A ↾}_{B}) \subseteq On)$
10		df-f	$⊢ A : dom A ⟶ On \leftrightarrow (A Fn dom A \land ran A \subseteq On)$
11		df-f	$⊢ ({A ↾}_{B}) : dom ({A ↾}_{B}) ⟶ On \leftrightarrow (({A ↾}_{B}) Fn dom ({A ↾}_{B}) \land ran ({A ↾}_{B}) \subseteq On)$
12	9 10 11	3imtr4i	$⊢ A : dom A ⟶ On \to ({A ↾}_{B}) : dom ({A ↾}_{B}) ⟶ On$
13	12	a1i	$⊢ B \in dom A \to (A : dom A ⟶ On \to ({A ↾}_{B}) : dom ({A ↾}_{B}) ⟶ On)$
14		ordelord	$⊢ (Ord dom A \land B \in dom A) \to Ord B$
15	14	expcom	$⊢ B \in dom A \to (Ord dom A \to Ord B)$
16		ordin	$⊢ (Ord B \land Ord dom A) \to Ord (B \cap dom A)$
17	16	ex	$⊢ Ord B \to (Ord dom A \to Ord (B \cap dom A))$
18	15 17	syli	$⊢ B \in dom A \to (Ord dom A \to Ord (B \cap dom A))$
19		dmres	$⊢ dom ({A ↾}_{B}) = B \cap dom A$
20		ordeq	$⊢ dom ({A ↾}_{B}) = B \cap dom A \to (Ord dom ({A ↾}_{B}) \leftrightarrow Ord (B \cap dom A))$
21	19 20	ax-mp	$⊢ Ord dom ({A ↾}_{B}) \leftrightarrow Ord (B \cap dom A)$
22	18 21	syl6ibr	$⊢ B \in dom A \to (Ord dom A \to Ord dom ({A ↾}_{B}))$
23		dmss	$⊢ {A ↾}_{B} \subseteq A \to dom ({A ↾}_{B}) \subseteq dom A$
24	5 23	ax-mp	$⊢ dom ({A ↾}_{B}) \subseteq dom A$
25		ssralv	$⊢ dom ({A ↾}_{B}) \subseteq dom A \to (\forall x \in dom A \forall y \in dom A (x \in y \to A (x) \in A (y)) \to \forall x \in dom ({A ↾}_{B}) \forall y \in dom A (x \in y \to A (x) \in A (y)))$
26	24 25	ax-mp	$⊢ \forall x \in dom A \forall y \in dom A (x \in y \to A (x) \in A (y)) \to \forall x \in dom ({A ↾}_{B}) \forall y \in dom A (x \in y \to A (x) \in A (y))$
27		ssralv	$⊢ dom ({A ↾}_{B}) \subseteq dom A \to (\forall y \in dom A (x \in y \to A (x) \in A (y)) \to \forall y \in dom ({A ↾}_{B}) (x \in y \to A (x) \in A (y)))$
28	24 27	ax-mp	$⊢ \forall y \in dom A (x \in y \to A (x) \in A (y)) \to \forall y \in dom ({A ↾}_{B}) (x \in y \to A (x) \in A (y))$
29	28	ralimi	$⊢ \forall x \in dom ({A ↾}_{B}) \forall y \in dom A (x \in y \to A (x) \in A (y)) \to \forall x \in dom ({A ↾}_{B}) \forall y \in dom ({A ↾}_{B}) (x \in y \to A (x) \in A (y))$
30	26 29	syl	$⊢ \forall x \in dom A \forall y \in dom A (x \in y \to A (x) \in A (y)) \to \forall x \in dom ({A ↾}_{B}) \forall y \in dom ({A ↾}_{B}) (x \in y \to A (x) \in A (y))$
31		inss1	$⊢ B \cap dom A \subseteq B$
32	19 31	eqsstri	$⊢ dom ({A ↾}_{B}) \subseteq B$
33		simpl	$⊢ (x \in dom ({A ↾}_{B}) \land y \in dom ({A ↾}_{B})) \to x \in dom ({A ↾}_{B})$
34	32 33	sselid	$⊢ (x \in dom ({A ↾}_{B}) \land y \in dom ({A ↾}_{B})) \to x \in B$
35	34	fvresd	$⊢ (x \in dom ({A ↾}_{B}) \land y \in dom ({A ↾}_{B})) \to ({A ↾}_{B}) (x) = A (x)$
36		simpr	$⊢ (x \in dom ({A ↾}_{B}) \land y \in dom ({A ↾}_{B})) \to y \in dom ({A ↾}_{B})$
37	32 36	sselid	$⊢ (x \in dom ({A ↾}_{B}) \land y \in dom ({A ↾}_{B})) \to y \in B$
38	37	fvresd	$⊢ (x \in dom ({A ↾}_{B}) \land y \in dom ({A ↾}_{B})) \to ({A ↾}_{B}) (y) = A (y)$
39	35 38	eleq12d	$⊢ (x \in dom ({A ↾}_{B}) \land y \in dom ({A ↾}_{B})) \to (({A ↾}_{B}) (x) \in ({A ↾}_{B}) (y) \leftrightarrow A (x) \in A (y))$
40	39	imbi2d	$⊢ (x \in dom ({A ↾}_{B}) \land y \in dom ({A ↾}_{B})) \to ((x \in y \to ({A ↾}_{B}) (x) \in ({A ↾}_{B}) (y)) \leftrightarrow (x \in y \to A (x) \in A (y)))$
41	40	ralbidva	$⊢ x \in dom ({A ↾}_{B}) \to (\forall y \in dom ({A ↾}_{B}) (x \in y \to ({A ↾}_{B}) (x) \in ({A ↾}_{B}) (y)) \leftrightarrow \forall y \in dom ({A ↾}_{B}) (x \in y \to A (x) \in A (y)))$
42	41	ralbiia	$⊢ \forall x \in dom ({A ↾}_{B}) \forall y \in dom ({A ↾}_{B}) (x \in y \to ({A ↾}_{B}) (x) \in ({A ↾}_{B}) (y)) \leftrightarrow \forall x \in dom ({A ↾}_{B}) \forall y \in dom ({A ↾}_{B}) (x \in y \to A (x) \in A (y))$
43	30 42	sylibr	$⊢ \forall x \in dom A \forall y \in dom A (x \in y \to A (x) \in A (y)) \to \forall x \in dom ({A ↾}_{B}) \forall y \in dom ({A ↾}_{B}) (x \in y \to ({A ↾}_{B}) (x) \in ({A ↾}_{B}) (y))$
44	43	a1i	$⊢ B \in dom A \to (\forall x \in dom A \forall y \in dom A (x \in y \to A (x) \in A (y)) \to \forall x \in dom ({A ↾}_{B}) \forall y \in dom ({A ↾}_{B}) (x \in y \to ({A ↾}_{B}) (x) \in ({A ↾}_{B}) (y)))$
45	13 22 44	3anim123d	$⊢ B \in dom A \to ((A : dom A ⟶ On \land Ord dom A \land \forall x \in dom A \forall y \in dom A (x \in y \to A (x) \in A (y))) \to (({A ↾}_{B}) : dom ({A ↾}_{B}) ⟶ On \land Ord dom ({A ↾}_{B}) \land \forall x \in dom ({A ↾}_{B}) \forall y \in dom ({A ↾}_{B}) (x \in y \to ({A ↾}_{B}) (x) \in ({A ↾}_{B}) (y))))$
46		df-smo	$⊢ Smo A \leftrightarrow (A : dom A ⟶ On \land Ord dom A \land \forall x \in dom A \forall y \in dom A (x \in y \to A (x) \in A (y)))$
47		df-smo	$⊢ Smo ({A ↾}_{B}) \leftrightarrow (({A ↾}_{B}) : dom ({A ↾}_{B}) ⟶ On \land Ord dom ({A ↾}_{B}) \land \forall x \in dom ({A ↾}_{B}) \forall y \in dom ({A ↾}_{B}) (x \in y \to ({A ↾}_{B}) (x) \in ({A ↾}_{B}) (y)))$
48	45 46 47	3imtr4g	$⊢ B \in dom A \to (Smo A \to Smo ({A ↾}_{B}))$
49	48	impcom	$⊢ (Smo A \land B \in dom A) \to Smo ({A ↾}_{B})$

Metamath Proof Explorer

Theorem smores

Proof