smores2

Description: A strictly monotone ordinal function restricted to an ordinal is still monotone. (Contributed by Mario Carneiro, 15-Mar-2013)

		Ref	Expression
	Assertion	smores2	$⊢ (Smo F \land Ord A) \to Smo ({F ↾}_{A})$

Proof

Step	Hyp	Ref	Expression
1		dfsmo2	$⊢ Smo F \leftrightarrow (F : dom F ⟶ On \land Ord dom F \land \forall x \in dom F \forall y \in x F (y) \in F (x))$
2	1	simp1bi	$⊢ Smo F \to F : dom F ⟶ On$
3	2	ffund	$⊢ Smo F \to Fun F$
4		funres	$⊢ Fun F \to Fun ({F ↾}_{A})$
5	4	funfnd	$⊢ Fun F \to ({F ↾}_{A}) Fn dom ({F ↾}_{A})$
6	3 5	syl	$⊢ Smo F \to ({F ↾}_{A}) Fn dom ({F ↾}_{A})$
7		df-ima	$⊢ F [A] = ran ({F ↾}_{A})$
8		imassrn	$⊢ F [A] \subseteq ran F$
9	7 8	eqsstrri	$⊢ ran ({F ↾}_{A}) \subseteq ran F$
10	2	frnd	$⊢ Smo F \to ran F \subseteq On$
11	9 10	sstrid	$⊢ Smo F \to ran ({F ↾}_{A}) \subseteq On$
12		df-f	$⊢ ({F ↾}_{A}) : dom ({F ↾}_{A}) ⟶ On \leftrightarrow (({F ↾}_{A}) Fn dom ({F ↾}_{A}) \land ran ({F ↾}_{A}) \subseteq On)$
13	6 11 12	sylanbrc	$⊢ Smo F \to ({F ↾}_{A}) : dom ({F ↾}_{A}) ⟶ On$
14	13	adantr	$⊢ (Smo F \land Ord A) \to ({F ↾}_{A}) : dom ({F ↾}_{A}) ⟶ On$
15		smodm	$⊢ Smo F \to Ord dom F$
16		ordin	$⊢ (Ord A \land Ord dom F) \to Ord (A \cap dom F)$
17		dmres	$⊢ dom ({F ↾}_{A}) = A \cap dom F$
18		ordeq	$⊢ dom ({F ↾}_{A}) = A \cap dom F \to (Ord dom ({F ↾}_{A}) \leftrightarrow Ord (A \cap dom F))$
19	17 18	ax-mp	$⊢ Ord dom ({F ↾}_{A}) \leftrightarrow Ord (A \cap dom F)$
20	16 19	sylibr	$⊢ (Ord A \land Ord dom F) \to Ord dom ({F ↾}_{A})$
21	20	ancoms	$⊢ (Ord dom F \land Ord A) \to Ord dom ({F ↾}_{A})$
22	15 21	sylan	$⊢ (Smo F \land Ord A) \to Ord dom ({F ↾}_{A})$
23		resss	$⊢ {F ↾}_{A} \subseteq F$
24		dmss	$⊢ {F ↾}_{A} \subseteq F \to dom ({F ↾}_{A}) \subseteq dom F$
25	23 24	ax-mp	$⊢ dom ({F ↾}_{A}) \subseteq dom F$
26	1	simp3bi	$⊢ Smo F \to \forall x \in dom F \forall y \in x F (y) \in F (x)$
27		ssralv	$⊢ dom ({F ↾}_{A}) \subseteq dom F \to (\forall x \in dom F \forall y \in x F (y) \in F (x) \to \forall x \in dom ({F ↾}_{A}) \forall y \in x F (y) \in F (x))$
28	25 26 27	mpsyl	$⊢ Smo F \to \forall x \in dom ({F ↾}_{A}) \forall y \in x F (y) \in F (x)$
29	28	adantr	$⊢ (Smo F \land Ord A) \to \forall x \in dom ({F ↾}_{A}) \forall y \in x F (y) \in F (x)$
30		ordtr1	$⊢ Ord dom ({F ↾}_{A}) \to ((y \in x \land x \in dom ({F ↾}_{A})) \to y \in dom ({F ↾}_{A}))$
31	22 30	syl	$⊢ (Smo F \land Ord A) \to ((y \in x \land x \in dom ({F ↾}_{A})) \to y \in dom ({F ↾}_{A}))$
32		inss1	$⊢ A \cap dom F \subseteq A$
33	17 32	eqsstri	$⊢ dom ({F ↾}_{A}) \subseteq A$
34	33	sseli	$⊢ y \in dom ({F ↾}_{A}) \to y \in A$
35	31 34	syl6	$⊢ (Smo F \land Ord A) \to ((y \in x \land x \in dom ({F ↾}_{A})) \to y \in A)$
36	35	expcomd	$⊢ (Smo F \land Ord A) \to (x \in dom ({F ↾}_{A}) \to (y \in x \to y \in A))$
37	36	imp31	$⊢ (((Smo F \land Ord A) \land x \in dom ({F ↾}_{A})) \land y \in x) \to y \in A$
38	37	fvresd	$⊢ (((Smo F \land Ord A) \land x \in dom ({F ↾}_{A})) \land y \in x) \to ({F ↾}_{A}) (y) = F (y)$
39	33	sseli	$⊢ x \in dom ({F ↾}_{A}) \to x \in A$
40	39	fvresd	$⊢ x \in dom ({F ↾}_{A}) \to ({F ↾}_{A}) (x) = F (x)$
41	40	ad2antlr	$⊢ (((Smo F \land Ord A) \land x \in dom ({F ↾}_{A})) \land y \in x) \to ({F ↾}_{A}) (x) = F (x)$
42	38 41	eleq12d	$⊢ (((Smo F \land Ord A) \land x \in dom ({F ↾}_{A})) \land y \in x) \to (({F ↾}_{A}) (y) \in ({F ↾}_{A}) (x) \leftrightarrow F (y) \in F (x))$
43	42	ralbidva	$⊢ ((Smo F \land Ord A) \land x \in dom ({F ↾}_{A})) \to (\forall y \in x ({F ↾}_{A}) (y) \in ({F ↾}_{A}) (x) \leftrightarrow \forall y \in x F (y) \in F (x))$
44	43	ralbidva	$⊢ (Smo F \land Ord A) \to (\forall x \in dom ({F ↾}_{A}) \forall y \in x ({F ↾}_{A}) (y) \in ({F ↾}_{A}) (x) \leftrightarrow \forall x \in dom ({F ↾}_{A}) \forall y \in x F (y) \in F (x))$
45	29 44	mpbird	$⊢ (Smo F \land Ord A) \to \forall x \in dom ({F ↾}_{A}) \forall y \in x ({F ↾}_{A}) (y) \in ({F ↾}_{A}) (x)$
46		dfsmo2	$⊢ Smo ({F ↾}_{A}) \leftrightarrow (({F ↾}_{A}) : dom ({F ↾}_{A}) ⟶ On \land Ord dom ({F ↾}_{A}) \land \forall x \in dom ({F ↾}_{A}) \forall y \in x ({F ↾}_{A}) (y) \in ({F ↾}_{A}) (x))$
47	14 22 45 46	syl3anbrc	$⊢ (Smo F \land Ord A) \to Smo ({F ↾}_{A})$

Metamath Proof Explorer

Theorem smores2

Proof