isercolllem2

	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	isercolllem2	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to (1 \dots \|G [G^{-1} [(M \dots N)]]\|) = G^{-1} [(M \dots N)]$

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		elfznn	$⊢ x \in (1 \dots sup (G^{-1} [(M \dots N)] ℝ <)) \to x \in ℕ$
6	5	a1i	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to (x \in (1 \dots sup (G^{-1} [(M \dots N)] ℝ <)) \to x \in ℕ)$
7		cnvimass	$⊢ G^{-1} [(M \dots N)] \subseteq dom G$
8	3	adantr	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to G : ℕ ⟶ Z$
9	7 8	fssdm	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to G^{-1} [(M \dots N)] \subseteq ℕ$
10	9	sseld	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to (x \in G^{-1} [(M \dots N)] \to x \in ℕ)$
11		id	$⊢ x \in ℕ \to x \in ℕ$
12		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
13	11 12	eleqtrdi	$⊢ x \in ℕ \to x \in ℤ_{\geq 1}$
14		ltso	$⊢ < Or ℝ$
15	14	a1i	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to < Or ℝ$
16		fzfid	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to (M \dots N) \in Fin$
17		ffun	$⊢ G : ℕ ⟶ Z \to Fun G$
18		funimacnv	$⊢ Fun G \to G [G^{-1} [(M \dots N)]] = (M \dots N) \cap ran G$
19	8 17 18	3syl	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to G [G^{-1} [(M \dots N)]] = (M \dots N) \cap ran G$
20		inss1	$⊢ (M \dots N) \cap ran G \subseteq (M \dots N)$
21	19 20	eqsstrdi	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to G [G^{-1} [(M \dots N)]] \subseteq (M \dots N)$
22	16 21	ssfid	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to G [G^{-1} [(M \dots N)]] \in Fin$
23		ssid	$⊢ ℕ \subseteq ℕ$
24	1 2 3 4	isercolllem1	$⊢ (φ \land ℕ \subseteq ℕ) \to ({G ↾}_{ℕ}) {Isom}_{<, <} (ℕ, G [ℕ])$
25	23 24	mpan2	$⊢ φ \to ({G ↾}_{ℕ}) {Isom}_{<, <} (ℕ, G [ℕ])$
26		ffn	$⊢ G : ℕ ⟶ Z \to G Fn ℕ$
27		fnresdm	$⊢ G Fn ℕ \to {G ↾}_{ℕ} = G$
28		isoeq1	$⊢ {G ↾}_{ℕ} = G \to (({G ↾}_{ℕ}) {Isom}_{<, <} (ℕ, G [ℕ]) \leftrightarrow G {Isom}_{<, <} (ℕ, G [ℕ]))$
29	3 26 27 28	4syl	$⊢ φ \to (({G ↾}_{ℕ}) {Isom}_{<, <} (ℕ, G [ℕ]) \leftrightarrow G {Isom}_{<, <} (ℕ, G [ℕ]))$
30	25 29	mpbid	$⊢ φ \to G {Isom}_{<, <} (ℕ, G [ℕ])$
31		isof1o	$⊢ G {Isom}_{<, <} (ℕ, G [ℕ]) \to G : ℕ \underset{1-1 onto}{⟶} G [ℕ]$
32		f1ocnv	$⊢ G : ℕ \underset{1-1 onto}{⟶} G [ℕ] \to G^{-1} : G [ℕ] \underset{1-1 onto}{⟶} ℕ$
33		f1ofun	$⊢ G^{-1} : G [ℕ] \underset{1-1 onto}{⟶} ℕ \to Fun G^{-1}$
34	30 31 32 33	4syl	$⊢ φ \to Fun G^{-1}$
35		df-f1	$⊢ G : ℕ \underset{1-1}{⟶} Z \leftrightarrow (G : ℕ ⟶ Z \land Fun G^{-1})$
36	3 34 35	sylanbrc	$⊢ φ \to G : ℕ \underset{1-1}{⟶} Z$
37	36	adantr	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to G : ℕ \underset{1-1}{⟶} Z$
38		nnex	$⊢ ℕ \in V$
39		ssexg	$⊢ (G^{-1} [(M \dots N)] \subseteq ℕ \land ℕ \in V) \to G^{-1} [(M \dots N)] \in V$
40	9 38 39	sylancl	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to G^{-1} [(M \dots N)] \in V$
41		f1imaeng	$⊢ (G : ℕ \underset{1-1}{⟶} Z \land G^{-1} [(M \dots N)] \subseteq ℕ \land G^{-1} [(M \dots N)] \in V) \to G [G^{-1} [(M \dots N)]] \approx G^{-1} [(M \dots N)]$
42	37 9 40 41	syl3anc	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to G [G^{-1} [(M \dots N)]] \approx G^{-1} [(M \dots N)]$
43	42	ensymd	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to G^{-1} [(M \dots N)] \approx G [G^{-1} [(M \dots N)]]$
44		enfii	$⊢ (G [G^{-1} [(M \dots N)]] \in Fin \land G^{-1} [(M \dots N)] \approx G [G^{-1} [(M \dots N)]]) \to G^{-1} [(M \dots N)] \in Fin$
45	22 43 44	syl2anc	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to G^{-1} [(M \dots N)] \in Fin$
46		1nn	$⊢ 1 \in ℕ$
47	46	a1i	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to 1 \in ℕ$
48		ffvelcdm	$⊢ (G : ℕ ⟶ Z \land 1 \in ℕ) \to G (1) \in Z$
49	3 46 48	sylancl	$⊢ φ \to G (1) \in Z$
50	49 1	eleqtrdi	$⊢ φ \to G (1) \in ℤ_{\geq M}$
51	50	adantr	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to G (1) \in ℤ_{\geq M}$
52		simpr	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to N \in ℤ_{\geq G (1)}$
53		elfzuzb	$⊢ G (1) \in (M \dots N) \leftrightarrow (G (1) \in ℤ_{\geq M} \land N \in ℤ_{\geq G (1)})$
54	51 52 53	sylanbrc	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to G (1) \in (M \dots N)$
55	8	ffnd	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to G Fn ℕ$
56		elpreima	$⊢ G Fn ℕ \to (1 \in G^{-1} [(M \dots N)] \leftrightarrow (1 \in ℕ \land G (1) \in (M \dots N)))$
57	55 56	syl	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to (1 \in G^{-1} [(M \dots N)] \leftrightarrow (1 \in ℕ \land G (1) \in (M \dots N)))$
58	47 54 57	mpbir2and	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to 1 \in G^{-1} [(M \dots N)]$
59	58	ne0d	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to G^{-1} [(M \dots N)] \neq \emptyset$
60		nnssre	$⊢ ℕ \subseteq ℝ$
61	9 60	sstrdi	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to G^{-1} [(M \dots N)] \subseteq ℝ$
62		fisupcl	$⊢ (< Or ℝ \land (G^{-1} [(M \dots N)] \in Fin \land G^{-1} [(M \dots N)] \neq \emptyset \land G^{-1} [(M \dots N)] \subseteq ℝ)) \to sup (G^{-1} [(M \dots N)] ℝ <) \in G^{-1} [(M \dots N)]$
63	15 45 59 61 62	syl13anc	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to sup (G^{-1} [(M \dots N)] ℝ <) \in G^{-1} [(M \dots N)]$
64	9 63	sseldd	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to sup (G^{-1} [(M \dots N)] ℝ <) \in ℕ$
65	64	nnzd	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to sup (G^{-1} [(M \dots N)] ℝ <) \in ℤ$
66		elfz5	$⊢ (x \in ℤ_{\geq 1} \land sup (G^{-1} [(M \dots N)] ℝ <) \in ℤ) \to (x \in (1 \dots sup (G^{-1} [(M \dots N)] ℝ <)) \leftrightarrow x \leq sup (G^{-1} [(M \dots N)] ℝ <))$
67	13 65 66	syl2anr	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to (x \in (1 \dots sup (G^{-1} [(M \dots N)] ℝ <)) \leftrightarrow x \leq sup (G^{-1} [(M \dots N)] ℝ <))$
68		elpreima	$⊢ G Fn ℕ \to (sup (G^{-1} [(M \dots N)] ℝ <) \in G^{-1} [(M \dots N)] \leftrightarrow (sup (G^{-1} [(M \dots N)] ℝ <) \in ℕ \land G (sup (G^{-1} [(M \dots N)] ℝ <)) \in (M \dots N)))$
69	55 68	syl	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to (sup (G^{-1} [(M \dots N)] ℝ <) \in G^{-1} [(M \dots N)] \leftrightarrow (sup (G^{-1} [(M \dots N)] ℝ <) \in ℕ \land G (sup (G^{-1} [(M \dots N)] ℝ <)) \in (M \dots N)))$
70	63 69	mpbid	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to (sup (G^{-1} [(M \dots N)] ℝ <) \in ℕ \land G (sup (G^{-1} [(M \dots N)] ℝ <)) \in (M \dots N))$
71		elfzle2	$⊢ G (sup (G^{-1} [(M \dots N)] ℝ <)) \in (M \dots N) \to G (sup (G^{-1} [(M \dots N)] ℝ <)) \leq N$
72	70 71	simpl2im	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to G (sup (G^{-1} [(M \dots N)] ℝ <)) \leq N$
73	72	adantr	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to G (sup (G^{-1} [(M \dots N)] ℝ <)) \leq N$
74		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
75	1 74	eqsstri	$⊢ Z \subseteq ℤ$
76		zssre	$⊢ ℤ \subseteq ℝ$
77	75 76	sstri	$⊢ Z \subseteq ℝ$
78	8	ffvelcdmda	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to G (x) \in Z$
79	77 78	sselid	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to G (x) \in ℝ$
80	8 64	ffvelcdmd	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to G (sup (G^{-1} [(M \dots N)] ℝ <)) \in Z$
81	80	adantr	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to G (sup (G^{-1} [(M \dots N)] ℝ <)) \in Z$
82	77 81	sselid	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to G (sup (G^{-1} [(M \dots N)] ℝ <)) \in ℝ$
83		eluzelz	$⊢ N \in ℤ_{\geq G (1)} \to N \in ℤ$
84	83	ad2antlr	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to N \in ℤ$
85	76 84	sselid	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to N \in ℝ$
86		letr	$⊢ (G (x) \in ℝ \land G (sup (G^{-1} [(M \dots N)] ℝ <)) \in ℝ \land N \in ℝ) \to ((G (x) \leq G (sup (G^{-1} [(M \dots N)] ℝ <)) \land G (sup (G^{-1} [(M \dots N)] ℝ <)) \leq N) \to G (x) \leq N)$
87	79 82 85 86	syl3anc	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to ((G (x) \leq G (sup (G^{-1} [(M \dots N)] ℝ <)) \land G (sup (G^{-1} [(M \dots N)] ℝ <)) \leq N) \to G (x) \leq N)$
88	73 87	mpan2d	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to (G (x) \leq G (sup (G^{-1} [(M \dots N)] ℝ <)) \to G (x) \leq N)$
89	30	ad2antrr	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to G {Isom}_{<, <} (ℕ, G [ℕ])$
90	60	a1i	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to ℕ \subseteq ℝ$
91		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
92	90 91	sstrdi	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to ℕ \subseteq ℝ^{*}$
93		imassrn	$⊢ G [ℕ] \subseteq ran G$
94	3	ad2antrr	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to G : ℕ ⟶ Z$
95	94	frnd	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to ran G \subseteq Z$
96	93 95	sstrid	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to G [ℕ] \subseteq Z$
97	96 77	sstrdi	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to G [ℕ] \subseteq ℝ$
98	97 91	sstrdi	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to G [ℕ] \subseteq ℝ^{*}$
99		simpr	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to x \in ℕ$
100	64	adantr	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to sup (G^{-1} [(M \dots N)] ℝ <) \in ℕ$
101		leisorel	$⊢ (G {Isom}_{<, <} (ℕ, G [ℕ]) \land (ℕ \subseteq ℝ^{} \land G [ℕ] \subseteq ℝ^{}) \land (x \in ℕ \land sup (G^{-1} [(M \dots N)] ℝ <) \in ℕ)) \to (x \leq sup (G^{-1} [(M \dots N)] ℝ <) \leftrightarrow G (x) \leq G (sup (G^{-1} [(M \dots N)] ℝ <)))$
102	89 92 98 99 100 101	syl122anc	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to (x \leq sup (G^{-1} [(M \dots N)] ℝ <) \leftrightarrow G (x) \leq G (sup (G^{-1} [(M \dots N)] ℝ <)))$
103	78 1	eleqtrdi	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to G (x) \in ℤ_{\geq M}$
104		elfz5	$⊢ (G (x) \in ℤ_{\geq M} \land N \in ℤ) \to (G (x) \in (M \dots N) \leftrightarrow G (x) \leq N)$
105	103 84 104	syl2anc	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to (G (x) \in (M \dots N) \leftrightarrow G (x) \leq N)$
106	88 102 105	3imtr4d	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to (x \leq sup (G^{-1} [(M \dots N)] ℝ <) \to G (x) \in (M \dots N))$
107		elpreima	$⊢ G Fn ℕ \to (x \in G^{-1} [(M \dots N)] \leftrightarrow (x \in ℕ \land G (x) \in (M \dots N)))$
108	107	baibd	$⊢ (G Fn ℕ \land x \in ℕ) \to (x \in G^{-1} [(M \dots N)] \leftrightarrow G (x) \in (M \dots N))$
109	55 108	sylan	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to (x \in G^{-1} [(M \dots N)] \leftrightarrow G (x) \in (M \dots N))$
110	106 109	sylibrd	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to (x \leq sup (G^{-1} [(M \dots N)] ℝ <) \to x \in G^{-1} [(M \dots N)])$
111		fimaxre2	$⊢ (G^{-1} [(M \dots N)] \subseteq ℝ \land G^{-1} [(M \dots N)] \in Fin) \to \exists x \in ℝ \forall y \in G^{-1} [(M \dots N)] y \leq x$
112	61 45 111	syl2anc	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to \exists x \in ℝ \forall y \in G^{-1} [(M \dots N)] y \leq x$
113		suprub	$⊢ ((G^{-1} [(M \dots N)] \subseteq ℝ \land G^{-1} [(M \dots N)] \neq \emptyset \land \exists x \in ℝ \forall y \in G^{-1} [(M \dots N)] y \leq x) \land x \in G^{-1} [(M \dots N)]) \to x \leq sup (G^{-1} [(M \dots N)] ℝ <)$
114	113	ex	$⊢ (G^{-1} [(M \dots N)] \subseteq ℝ \land G^{-1} [(M \dots N)] \neq \emptyset \land \exists x \in ℝ \forall y \in G^{-1} [(M \dots N)] y \leq x) \to (x \in G^{-1} [(M \dots N)] \to x \leq sup (G^{-1} [(M \dots N)] ℝ <))$
115	61 59 112 114	syl3anc	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to (x \in G^{-1} [(M \dots N)] \to x \leq sup (G^{-1} [(M \dots N)] ℝ <))$
116	115	adantr	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to (x \in G^{-1} [(M \dots N)] \to x \leq sup (G^{-1} [(M \dots N)] ℝ <))$
117	110 116	impbid	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to (x \leq sup (G^{-1} [(M \dots N)] ℝ <) \leftrightarrow x \in G^{-1} [(M \dots N)])$
118	67 117	bitrd	$⊢ ((φ \land N \in ℤ_{\geq G (1)}) \land x \in ℕ) \to (x \in (1 \dots sup (G^{-1} [(M \dots N)] ℝ <)) \leftrightarrow x \in G^{-1} [(M \dots N)])$
119	118	ex	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to (x \in ℕ \to (x \in (1 \dots sup (G^{-1} [(M \dots N)] ℝ <)) \leftrightarrow x \in G^{-1} [(M \dots N)]))$
120	6 10 119	pm5.21ndd	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to (x \in (1 \dots sup (G^{-1} [(M \dots N)] ℝ <)) \leftrightarrow x \in G^{-1} [(M \dots N)])$
121	120	eqrdv	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to (1 \dots sup (G^{-1} [(M \dots N)] ℝ <)) = G^{-1} [(M \dots N)]$
122	121	fveq2d	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to \|(1 \dots sup (G^{-1} [(M \dots N)] ℝ <))\| = \|G^{-1} [(M \dots N)]\|$
123	64	nnnn0d	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to sup (G^{-1} [(M \dots N)] ℝ <) \in ℕ_{0}$
124		hashfz1	$⊢ sup (G^{-1} [(M \dots N)] ℝ <) \in ℕ_{0} \to \|(1 \dots sup (G^{-1} [(M \dots N)] ℝ <))\| = sup (G^{-1} [(M \dots N)] ℝ <)$
125	123 124	syl	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to \|(1 \dots sup (G^{-1} [(M \dots N)] ℝ <))\| = sup (G^{-1} [(M \dots N)] ℝ <)$
126		hashen	$⊢ (G^{-1} [(M \dots N)] \in Fin \land G [G^{-1} [(M \dots N)]] \in Fin) \to (\|G^{-1} [(M \dots N)]\| = \|G [G^{-1} [(M \dots N)]]\| \leftrightarrow G^{-1} [(M \dots N)] \approx G [G^{-1} [(M \dots N)]])$
127	45 22 126	syl2anc	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to (\|G^{-1} [(M \dots N)]\| = \|G [G^{-1} [(M \dots N)]]\| \leftrightarrow G^{-1} [(M \dots N)] \approx G [G^{-1} [(M \dots N)]])$
128	43 127	mpbird	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to \|G^{-1} [(M \dots N)]\| = \|G [G^{-1} [(M \dots N)]]\|$
129	122 125 128	3eqtr3d	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to sup (G^{-1} [(M \dots N)] ℝ <) = \|G [G^{-1} [(M \dots N)]]\|$
130	129	oveq2d	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to (1 \dots sup (G^{-1} [(M \dots N)] ℝ <)) = (1 \dots \|G [G^{-1} [(M \dots N)]]\|)$
131	130 121	eqtr3d	$⊢ (φ \land N \in ℤ_{\geq G (1)}) \to (1 \dots \|G [G^{-1} [(M \dots N)]]\|) = G^{-1} [(M \dots N)]$

Metamath Proof Explorer

Theorem isercolllem2

Proof