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		rnresss	$⊢ ran ({A ↾}_{B}) \subseteq ran A$
6		sstr	$⊢ (ran ({A ↾}_{B}) \subseteq ran A \land ran A \subseteq On) \to ran ({A ↾}_{B}) \subseteq On$
7	5 6	mpan	$⊢ ran A \subseteq On \to ran ({A ↾}_{B}) \subseteq On$
8	4 7	anim12i	$⊢ (A Fn dom A \land ran A \subseteq On) \to (({A ↾}_{B}) Fn dom ({A ↾}_{B}) \land ran ({A ↾}_{B}) \subseteq On)$
9		df-f	$⊢ A : dom A ⟶ On \leftrightarrow (A Fn dom A \land ran A \subseteq On)$
10		df-f	$⊢ ({A ↾}_{B}) : dom ({A ↾}_{B}) ⟶ On \leftrightarrow (({A ↾}_{B}) Fn dom ({A ↾}_{B}) \land ran ({A ↾}_{B}) \subseteq On)$
11	8 9 10	3imtr4i	$⊢ A : dom A ⟶ On \to ({A ↾}_{B}) : dom ({A ↾}_{B}) ⟶ On$
12	11	a1i	$⊢ B \in dom A \to (A : dom A ⟶ On \to ({A ↾}_{B}) : dom ({A ↾}_{B}) ⟶ On)$
13		ordelord	$⊢ (Ord dom A \land B \in dom A) \to Ord B$
14	13	expcom	$⊢ B \in dom A \to (Ord dom A \to Ord B)$
15		ordin	$⊢ (Ord B \land Ord dom A) \to Ord (B \cap dom A)$
16	15	ex	$⊢ Ord B \to (Ord dom A \to Ord (B \cap dom A))$
17	14 16	syli	$⊢ B \in dom A \to (Ord dom A \to Ord (B \cap dom A))$
18		dmres	$⊢ dom ({A ↾}_{B}) = B \cap dom A$
19		ordeq	$⊢ dom ({A ↾}_{B}) = B \cap dom A \to (Ord dom ({A ↾}_{B}) \leftrightarrow Ord (B \cap dom A))$
20	18 19	ax-mp	$⊢ Ord dom ({A ↾}_{B}) \leftrightarrow Ord (B \cap dom A)$
21	17 20	imbitrrdi	$⊢ B \in dom A \to (Ord dom A \to Ord dom ({A ↾}_{B}))$
22		dmresss	$⊢ dom ({A ↾}_{B}) \subseteq dom A$
23		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)))$
24	22 23	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))$
25		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)))$
26	22 25	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))$
27	26	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))$
28	24 27	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))$
29		resdmss	$⊢ dom ({A ↾}_{B}) \subseteq B$
30		simpl	$⊢ (x \in dom ({A ↾}_{B}) \land y \in dom ({A ↾}_{B})) \to x \in dom ({A ↾}_{B})$
31	29 30	sselid	$⊢ (x \in dom ({A ↾}_{B}) \land y \in dom ({A ↾}_{B})) \to x \in B$
32	31	fvresd	$⊢ (x \in dom ({A ↾}_{B}) \land y \in dom ({A ↾}_{B})) \to ({A ↾}_{B}) (x) = A (x)$
33		simpr	$⊢ (x \in dom ({A ↾}_{B}) \land y \in dom ({A ↾}_{B})) \to y \in dom ({A ↾}_{B})$
34	29 33	sselid	$⊢ (x \in dom ({A ↾}_{B}) \land y \in dom ({A ↾}_{B})) \to y \in B$
35	34	fvresd	$⊢ (x \in dom ({A ↾}_{B}) \land y \in dom ({A ↾}_{B})) \to ({A ↾}_{B}) (y) = A (y)$
36	32 35	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))$
37	36	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)))$
38	37	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)))$
39	38	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))$
40	28 39	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))$
41	40	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)))$
42	12 21 41	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))))$
43		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)))$
44		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)))$
45	42 43 44	3imtr4g	$⊢ B \in dom A \to (Smo A \to Smo ({A ↾}_{B}))$
46	45	impcom	$⊢ (Smo A \land B \in dom A) \to Smo ({A ↾}_{B})$

Metamath Proof Explorer

Theorem smores

Proof