isercolllem1

	Ref	Expression
Hypotheses	isercoll.z	$⊢ Z = ℤ_{\geq M}$
	isercoll.m	$⊢ φ \to M \in ℤ$
	isercoll.g	$⊢ φ \to G : ℕ ⟶ Z$
	isercoll.i	$⊢ (φ \land k \in ℕ) \to G (k) < G (k + 1)$
Assertion	isercolllem1	$⊢ (φ \land S \subseteq ℕ) \to ({G ↾}_{S}) {Isom}_{<, <} (S, G [S])$

Proof

Step	Hyp	Ref	Expression
1		isercoll.z	$⊢ Z = ℤ_{\geq M}$
2		isercoll.m	$⊢ φ \to M \in ℤ$
3		isercoll.g	$⊢ φ \to G : ℕ ⟶ Z$
4		isercoll.i	$⊢ (φ \land k \in ℕ) \to G (k) < G (k + 1)$
5		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
6	1 5	eqsstri	$⊢ Z \subseteq ℤ$
7		zssre	$⊢ ℤ \subseteq ℝ$
8	6 7	sstri	$⊢ Z \subseteq ℝ$
9	3	ad2antrr	$⊢ ((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \to G : ℕ ⟶ Z$
10		simplrl	$⊢ ((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \to x \in ℕ$
11	9 10	ffvelrnd	$⊢ ((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \to G (x) \in Z$
12	8 11	sseldi	$⊢ ((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \to G (x) \in ℝ$
13		simplrr	$⊢ ((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \to y \in ℕ$
14	13	nnred	$⊢ ((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \to y \in ℝ$
15	12 14	resubcld	$⊢ ((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \to G (x) - y \in ℝ$
16	10	nnred	$⊢ ((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \to x \in ℝ$
17	12 16	resubcld	$⊢ ((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \to G (x) - x \in ℝ$
18	9 13	ffvelrnd	$⊢ ((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \to G (y) \in Z$
19	8 18	sseldi	$⊢ ((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \to G (y) \in ℝ$
20	19 14	resubcld	$⊢ ((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \to G (y) - y \in ℝ$
21		simpr	$⊢ ((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \to x < y$
22	16 14 12 21	ltsub2dd	$⊢ ((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \to G (x) - y < G (x) - x$
23	10	nnzd	$⊢ ((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \to x \in ℤ$
24	13	nnzd	$⊢ ((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \to y \in ℤ$
25	16 14 21	ltled	$⊢ ((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \to x \leq y$
26		eluz2	$⊢ y \in ℤ_{\geq x} \leftrightarrow (x \in ℤ \land y \in ℤ \land x \leq y)$
27	23 24 25 26	syl3anbrc	$⊢ ((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \to y \in ℤ_{\geq x}$
28		elfzuz	$⊢ k \in (x \dots y) \to k \in ℤ_{\geq x}$
29		eluznn	$⊢ (x \in ℕ \land k \in ℤ_{\geq x}) \to k \in ℕ$
30	10 29	sylan	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in ℤ_{\geq x}) \to k \in ℕ$
31		fveq2	$⊢ n = k \to G (n) = G (k)$
32		id	$⊢ n = k \to n = k$
33	31 32	oveq12d	$⊢ n = k \to G (n) - n = G (k) - k$
34		eqid	$⊢ (n \in ℕ ⟼ G (n) - n) = (n \in ℕ ⟼ G (n) - n)$
35		ovex	$⊢ G (k) - k \in V$
36	33 34 35	fvmpt	$⊢ k \in ℕ \to (n \in ℕ ⟼ G (n) - n) (k) = G (k) - k$
37	36	adantl	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in ℕ) \to (n \in ℕ ⟼ G (n) - n) (k) = G (k) - k$
38	9	ffvelrnda	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in ℕ) \to G (k) \in Z$
39	8 38	sseldi	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in ℕ) \to G (k) \in ℝ$
40		nnre	$⊢ k \in ℕ \to k \in ℝ$
41	40	adantl	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in ℕ) \to k \in ℝ$
42	39 41	resubcld	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in ℕ) \to G (k) - k \in ℝ$
43	37 42	eqeltrd	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in ℕ) \to (n \in ℕ ⟼ G (n) - n) (k) \in ℝ$
44	30 43	syldan	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in ℤ_{\geq x}) \to (n \in ℕ ⟼ G (n) - n) (k) \in ℝ$
45	28 44	sylan2	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in (x \dots y)) \to (n \in ℕ ⟼ G (n) - n) (k) \in ℝ$
46		elfzuz	$⊢ k \in (x \dots y - 1) \to k \in ℤ_{\geq x}$
47		peano2nn	$⊢ k \in ℕ \to k + 1 \in ℕ$
48		ffvelrn	$⊢ (G : ℕ ⟶ Z \land k + 1 \in ℕ) \to G (k + 1) \in Z$
49	9 47 48	syl2an	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in ℕ) \to G (k + 1) \in Z$
50	8 49	sseldi	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in ℕ) \to G (k + 1) \in ℝ$
51		peano2rem	$⊢ G (k + 1) \in ℝ \to G (k + 1) - 1 \in ℝ$
52	50 51	syl	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in ℕ) \to G (k + 1) - 1 \in ℝ$
53	4	ad4ant14	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in ℕ) \to G (k) < G (k + 1)$
54	6 38	sseldi	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in ℕ) \to G (k) \in ℤ$
55	6 49	sseldi	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in ℕ) \to G (k + 1) \in ℤ$
56		zltlem1	$⊢ (G (k) \in ℤ \land G (k + 1) \in ℤ) \to (G (k) < G (k + 1) \leftrightarrow G (k) \leq G (k + 1) - 1)$
57	54 55 56	syl2anc	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in ℕ) \to (G (k) < G (k + 1) \leftrightarrow G (k) \leq G (k + 1) - 1)$
58	53 57	mpbid	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in ℕ) \to G (k) \leq G (k + 1) - 1$
59	39 52 41 58	lesub1dd	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in ℕ) \to G (k) - k \leq G (k + 1) - 1 - k$
60	50	recnd	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in ℕ) \to G (k + 1) \in ℂ$
61		1cnd	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in ℕ) \to 1 \in ℂ$
62	41	recnd	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in ℕ) \to k \in ℂ$
63	60 61 62	sub32d	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in ℕ) \to G (k + 1) - 1 - k = G (k + 1) - k - 1$
64	60 62 61	subsub4d	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in ℕ) \to G (k + 1) - k - 1 = G (k + 1) - (k + 1)$
65	63 64	eqtrd	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in ℕ) \to G (k + 1) - 1 - k = G (k + 1) - (k + 1)$
66	59 65	breqtrd	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in ℕ) \to G (k) - k \leq G (k + 1) - (k + 1)$
67	47	adantl	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in ℕ) \to k + 1 \in ℕ$
68		fveq2	$⊢ n = k + 1 \to G (n) = G (k + 1)$
69		id	$⊢ n = k + 1 \to n = k + 1$
70	68 69	oveq12d	$⊢ n = k + 1 \to G (n) - n = G (k + 1) - (k + 1)$
71		ovex	$⊢ G (k + 1) - (k + 1) \in V$
72	70 34 71	fvmpt	$⊢ k + 1 \in ℕ \to (n \in ℕ ⟼ G (n) - n) (k + 1) = G (k + 1) - (k + 1)$
73	67 72	syl	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in ℕ) \to (n \in ℕ ⟼ G (n) - n) (k + 1) = G (k + 1) - (k + 1)$
74	66 37 73	3brtr4d	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in ℕ) \to (n \in ℕ ⟼ G (n) - n) (k) \leq (n \in ℕ ⟼ G (n) - n) (k + 1)$
75	30 74	syldan	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in ℤ_{\geq x}) \to (n \in ℕ ⟼ G (n) - n) (k) \leq (n \in ℕ ⟼ G (n) - n) (k + 1)$
76	46 75	sylan2	$⊢ (((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \land k \in (x \dots y - 1)) \to (n \in ℕ ⟼ G (n) - n) (k) \leq (n \in ℕ ⟼ G (n) - n) (k + 1)$
77	27 45 76	monoord	$⊢ ((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \to (n \in ℕ ⟼ G (n) - n) (x) \leq (n \in ℕ ⟼ G (n) - n) (y)$
78		fveq2	$⊢ n = x \to G (n) = G (x)$
79		id	$⊢ n = x \to n = x$
80	78 79	oveq12d	$⊢ n = x \to G (n) - n = G (x) - x$
81		ovex	$⊢ G (x) - x \in V$
82	80 34 81	fvmpt	$⊢ x \in ℕ \to (n \in ℕ ⟼ G (n) - n) (x) = G (x) - x$
83	10 82	syl	$⊢ ((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \to (n \in ℕ ⟼ G (n) - n) (x) = G (x) - x$
84		fveq2	$⊢ n = y \to G (n) = G (y)$
85		id	$⊢ n = y \to n = y$
86	84 85	oveq12d	$⊢ n = y \to G (n) - n = G (y) - y$
87		ovex	$⊢ G (y) - y \in V$
88	86 34 87	fvmpt	$⊢ y \in ℕ \to (n \in ℕ ⟼ G (n) - n) (y) = G (y) - y$
89	13 88	syl	$⊢ ((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \to (n \in ℕ ⟼ G (n) - n) (y) = G (y) - y$
90	77 83 89	3brtr3d	$⊢ ((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \to G (x) - x \leq G (y) - y$
91	15 17 20 22 90	ltletrd	$⊢ ((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \to G (x) - y < G (y) - y$
92	12 19 14	ltsub1d	$⊢ ((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \to (G (x) < G (y) \leftrightarrow G (x) - y < G (y) - y)$
93	91 92	mpbird	$⊢ ((φ \land (x \in ℕ \land y \in ℕ)) \land x < y) \to G (x) < G (y)$
94	93	ex	$⊢ (φ \land (x \in ℕ \land y \in ℕ)) \to (x < y \to G (x) < G (y))$
95	94	ralrimivva	$⊢ φ \to \forall x \in ℕ \forall y \in ℕ (x < y \to G (x) < G (y))$
96		ss2ralv	$⊢ S \subseteq ℕ \to (\forall x \in ℕ \forall y \in ℕ (x < y \to G (x) < G (y)) \to \forall x \in S \forall y \in S (x < y \to G (x) < G (y)))$
97	95 96	mpan9	$⊢ (φ \land S \subseteq ℕ) \to \forall x \in S \forall y \in S (x < y \to G (x) < G (y))$
98		nnssre	$⊢ ℕ \subseteq ℝ$
99		ltso	$⊢ < Or ℝ$
100		soss	$⊢ ℕ \subseteq ℝ \to (< Or ℝ \to < Or ℕ)$
101	98 99 100	mp2	$⊢ < Or ℕ$
102	101	a1i	$⊢ (φ \land S \subseteq ℕ) \to < Or ℕ$
103		soss	$⊢ Z \subseteq ℝ \to (< Or ℝ \to < Or Z)$
104	8 99 103	mp2	$⊢ < Or Z$
105	104	a1i	$⊢ (φ \land S \subseteq ℕ) \to < Or Z$
106	3	adantr	$⊢ (φ \land S \subseteq ℕ) \to G : ℕ ⟶ Z$
107		simpr	$⊢ (φ \land S \subseteq ℕ) \to S \subseteq ℕ$
108		soisores	$⊢ ((< Or ℕ \land < Or Z) \land (G : ℕ ⟶ Z \land S \subseteq ℕ)) \to (({G ↾}_{S}) {Isom}_{<, <} (S, G [S]) \leftrightarrow \forall x \in S \forall y \in S (x < y \to G (x) < G (y)))$
109	102 105 106 107 108	syl22anc	$⊢ (φ \land S \subseteq ℕ) \to (({G ↾}_{S}) {Isom}_{<, <} (S, G [S]) \leftrightarrow \forall x \in S \forall y \in S (x < y \to G (x) < G (y)))$
110	97 109	mpbird	$⊢ (φ \land S \subseteq ℕ) \to ({G ↾}_{S}) {Isom}_{<, <} (S, G [S])$

Metamath Proof Explorer

Theorem isercolllem1

Proof