Theorem smores 5848

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.)

Assertion

Ref	Expression
smores	⊢ ((Smo A ∧ B ∈ dom A) → Smo (A ↾ B))

Proof of Theorem smores

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		funres 4884	. . . . . . . 8 ⊢ (Fun A → Fun (A ↾ B))
2		funfn 4874	. . . . . . . 8 ⊢ (Fun A ↔ A Fn dom A)
3		funfn 4874	. . . . . . . 8 ⊢ (Fun (A ↾ B) ↔ (A ↾ B) Fn dom (A ↾ B))
4	1, 2, 3	3imtr3i 189	. . . . . . 7 ⊢ (A Fn dom A → (A ↾ B) Fn dom (A ↾ B))
5		resss 4578	. . . . . . . . 9 ⊢ (A ↾ B) ⊆ A
6		rnss 4507	. . . . . . . . 9 ⊢ ((A ↾ B) ⊆ A → ran (A ↾ B) ⊆ ran A)
7	5, 6	ax-mp 7	. . . . . . . 8 ⊢ ran (A ↾ B) ⊆ ran A
8		sstr 2947	. . . . . . . 8 ⊢ ((ran (A ↾ B) ⊆ ran A ∧ ran A ⊆ On) → ran (A ↾ B) ⊆ On)
9	7, 8	mpan 400	. . . . . . 7 ⊢ (ran A ⊆ On → ran (A ↾ B) ⊆ On)
10	4, 9	anim12i 321	. . . . . 6 ⊢ ((A Fn dom A ∧ ran A ⊆ On) → ((A ↾ B) Fn dom (A ↾ B) ∧ ran (A ↾ B) ⊆ On))
11		df-f 4849	. . . . . 6 ⊢ (A:dom A⟶On ↔ (A Fn dom A ∧ ran A ⊆ On))
12		df-f 4849	. . . . . 6 ⊢ ((A ↾ B):dom (A ↾ B)⟶On ↔ ((A ↾ B) Fn dom (A ↾ B) ∧ ran (A ↾ B) ⊆ On))
13	10, 11, 12	3imtr4i 190	. . . . 5 ⊢ (A:dom A⟶On → (A ↾ B):dom (A ↾ B)⟶On)
14	13	a1i 9	. . . 4 ⊢ (B ∈ dom A → (A:dom A⟶On → (A ↾ B):dom (A ↾ B)⟶On))
15		ordelord 4084	. . . . . . 7 ⊢ ((Ord dom A ∧ B ∈ dom A) → Ord B)
16	15	expcom 109	. . . . . 6 ⊢ (B ∈ dom A → (Ord dom A → Ord B))
17		ordin 4088	. . . . . . 7 ⊢ ((Ord B ∧ Ord dom A) → Ord (B ∩ dom A))
18	17	ex 108	. . . . . 6 ⊢ (Ord B → (Ord dom A → Ord (B ∩ dom A)))
19	16, 18	syli 33	. . . . 5 ⊢ (B ∈ dom A → (Ord dom A → Ord (B ∩ dom A)))
20		dmres 4575	. . . . . 6 ⊢ dom (A ↾ B) = (B ∩ dom A)
21		ordeq 4075	. . . . . 6 ⊢ (dom (A ↾ B) = (B ∩ dom A) → (Ord dom (A ↾ B) ↔ Ord (B ∩ dom A)))
22	20, 21	ax-mp 7	. . . . 5 ⊢ (Ord dom (A ↾ B) ↔ Ord (B ∩ dom A))
23	19, 22	syl6ibr 151	. . . 4 ⊢ (B ∈ dom A → (Ord dom A → Ord dom (A ↾ B)))
24		dmss 4477	. . . . . . . . 9 ⊢ ((A ↾ B) ⊆ A → dom (A ↾ B) ⊆ dom A)
25	5, 24	ax-mp 7	. . . . . . . 8 ⊢ dom (A ↾ B) ⊆ dom A
26		ssralv 2998	. . . . . . . 8 ⊢ (dom (A ↾ B) ⊆ dom A → (∀x ∈ dom A∀y ∈ dom A(x ∈ y → (A‘x) ∈ (A‘y)) → ∀x ∈ dom (A ↾ B)∀y ∈ dom A(x ∈ y → (A‘x) ∈ (A‘y))))
27	25, 26	ax-mp 7	. . . . . . 7 ⊢ (∀x ∈ dom A∀y ∈ dom A(x ∈ y → (A‘x) ∈ (A‘y)) → ∀x ∈ dom (A ↾ B)∀y ∈ dom A(x ∈ y → (A‘x) ∈ (A‘y)))
28		ssralv 2998	. . . . . . . . 9 ⊢ (dom (A ↾ B) ⊆ dom A → (∀y ∈ dom A(x ∈ y → (A‘x) ∈ (A‘y)) → ∀y ∈ dom (A ↾ B)(x ∈ y → (A‘x) ∈ (A‘y))))
29	25, 28	ax-mp 7	. . . . . . . 8 ⊢ (∀y ∈ dom A(x ∈ y → (A‘x) ∈ (A‘y)) → ∀y ∈ dom (A ↾ B)(x ∈ y → (A‘x) ∈ (A‘y)))
30	29	ralimi 2378	. . . . . . 7 ⊢ (∀x ∈ dom (A ↾ B)∀y ∈ dom A(x ∈ y → (A‘x) ∈ (A‘y)) → ∀x ∈ dom (A ↾ B)∀y ∈ dom (A ↾ B)(x ∈ y → (A‘x) ∈ (A‘y)))
31	27, 30	syl 14	. . . . . 6 ⊢ (∀x ∈ dom A∀y ∈ dom A(x ∈ y → (A‘x) ∈ (A‘y)) → ∀x ∈ dom (A ↾ B)∀y ∈ dom (A ↾ B)(x ∈ y → (A‘x) ∈ (A‘y)))
32		inss1 3151	. . . . . . . . . . . . 13 ⊢ (B ∩ dom A) ⊆ B
33	20, 32	eqsstri 2969	. . . . . . . . . . . 12 ⊢ dom (A ↾ B) ⊆ B
34		simpl 102	. . . . . . . . . . . 12 ⊢ ((x ∈ dom (A ↾ B) ∧ y ∈ dom (A ↾ B)) → x ∈ dom (A ↾ B))
35	33, 34	sseldi 2937	. . . . . . . . . . 11 ⊢ ((x ∈ dom (A ↾ B) ∧ y ∈ dom (A ↾ B)) → x ∈ B)
36		fvres 5141	. . . . . . . . . . 11 ⊢ (x ∈ B → ((A ↾ B)‘x) = (A‘x))
37	35, 36	syl 14	. . . . . . . . . 10 ⊢ ((x ∈ dom (A ↾ B) ∧ y ∈ dom (A ↾ B)) → ((A ↾ B)‘x) = (A‘x))
38		simpr 103	. . . . . . . . . . . 12 ⊢ ((x ∈ dom (A ↾ B) ∧ y ∈ dom (A ↾ B)) → y ∈ dom (A ↾ B))
39	33, 38	sseldi 2937	. . . . . . . . . . 11 ⊢ ((x ∈ dom (A ↾ B) ∧ y ∈ dom (A ↾ B)) → y ∈ B)
40		fvres 5141	. . . . . . . . . . 11 ⊢ (y ∈ B → ((A ↾ B)‘y) = (A‘y))
41	39, 40	syl 14	. . . . . . . . . 10 ⊢ ((x ∈ dom (A ↾ B) ∧ y ∈ dom (A ↾ B)) → ((A ↾ B)‘y) = (A‘y))
42	37, 41	eleq12d 2105	. . . . . . . . 9 ⊢ ((x ∈ dom (A ↾ B) ∧ y ∈ dom (A ↾ B)) → (((A ↾ B)‘x) ∈ ((A ↾ B)‘y) ↔ (A‘x) ∈ (A‘y)))
43	42	imbi2d 219	. . . . . . . 8 ⊢ ((x ∈ dom (A ↾ B) ∧ y ∈ dom (A ↾ B)) → ((x ∈ y → ((A ↾ B)‘x) ∈ ((A ↾ B)‘y)) ↔ (x ∈ y → (A‘x) ∈ (A‘y))))
44	43	ralbidva 2316	. . . . . . 7 ⊢ (x ∈ dom (A ↾ B) → (∀y ∈ dom (A ↾ B)(x ∈ y → ((A ↾ B)‘x) ∈ ((A ↾ B)‘y)) ↔ ∀y ∈ dom (A ↾ B)(x ∈ y → (A‘x) ∈ (A‘y))))
45	44	ralbiia 2332	. . . . . 6 ⊢ (∀x ∈ dom (A ↾ B)∀y ∈ dom (A ↾ B)(x ∈ y → ((A ↾ B)‘x) ∈ ((A ↾ B)‘y)) ↔ ∀x ∈ dom (A ↾ B)∀y ∈ dom (A ↾ B)(x ∈ y → (A‘x) ∈ (A‘y)))
46	31, 45	sylibr 137	. . . . 5 ⊢ (∀x ∈ dom A∀y ∈ dom A(x ∈ y → (A‘x) ∈ (A‘y)) → ∀x ∈ dom (A ↾ B)∀y ∈ dom (A ↾ B)(x ∈ y → ((A ↾ B)‘x) ∈ ((A ↾ B)‘y)))
47	46	a1i 9	. . . 4 ⊢ (B ∈ dom A → (∀x ∈ dom A∀y ∈ dom A(x ∈ y → (A‘x) ∈ (A‘y)) → ∀x ∈ dom (A ↾ B)∀y ∈ dom (A ↾ B)(x ∈ y → ((A ↾ B)‘x) ∈ ((A ↾ B)‘y))))
48	14, 23, 47	3anim123d 1213	. . 3 ⊢ (B ∈ dom A → ((A:dom A⟶On ∧ Ord dom A ∧ ∀x ∈ dom A∀y ∈ dom A(x ∈ y → (A‘x) ∈ (A‘y))) → ((A ↾ B):dom (A ↾ B)⟶On ∧ Ord dom (A ↾ B) ∧ ∀x ∈ dom (A ↾ B)∀y ∈ dom (A ↾ B)(x ∈ y → ((A ↾ B)‘x) ∈ ((A ↾ B)‘y)))))
49		df-smo 5842	. . 3 ⊢ (Smo A ↔ (A:dom A⟶On ∧ Ord dom A ∧ ∀x ∈ dom A∀y ∈ dom A(x ∈ y → (A‘x) ∈ (A‘y))))
50		df-smo 5842	. . 3 ⊢ (Smo (A ↾ B) ↔ ((A ↾ B):dom (A ↾ B)⟶On ∧ Ord dom (A ↾ B) ∧ ∀x ∈ dom (A ↾ B)∀y ∈ dom (A ↾ B)(x ∈ y → ((A ↾ B)‘x) ∈ ((A ↾ B)‘y))))
51	48, 49, 50	3imtr4g 194	. 2 ⊢ (B ∈ dom A → (Smo A → Smo (A ↾ B)))
52	51	impcom 116	1 ⊢ ((Smo A ∧ B ∈ dom A) → Smo (A ↾ B))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∧ w3a 884   = wceq 1242   ∈ wcel 1390  ∀wral 2300   ∩ cin 2910   ⊆ wss 2911  Ord word 4065  Oncon0 4066  dom cdm 4288  ran crn 4289   ↾ cres 4290  Fun wfun 4839   Fn wfn 4840  ⟶wf 4841  ‘cfv 4845  Smo wsmo 5841

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-tr 3846  df-iord 4069  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-fv 4853  df-smo 5842

This theorem is referenced by:  smores3  5849