fzisoeu

Description: A finite ordered set has a unique order isomorphism to a generic finite sequence of integers. This theorem generalizes fz1iso for the base index and also states the uniqueness condition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fzisoeu.h	$⊢ φ \to H \in Fin$
	fzisoeu.or	$⊢ φ \to < Or H$
	fzisoeu.m	$⊢ φ \to M \in ℤ$
	fzisoeu.4	$⊢ N = \|H\| + M - 1$
Assertion	fzisoeu	$⊢ φ \to \exists! f f {Isom}_{<, <} ((M \dots N), H)$

Proof

Step	Hyp	Ref	Expression
1		fzisoeu.h	$⊢ φ \to H \in Fin$
2		fzisoeu.or	$⊢ φ \to < Or H$
3		fzisoeu.m	$⊢ φ \to M \in ℤ$
4		fzisoeu.4	$⊢ N = \|H\| + M - 1$
5		fzssz	$⊢ (M \dots N) \subseteq ℤ$
6		zssre	$⊢ ℤ \subseteq ℝ$
7	5 6	sstri	$⊢ (M \dots N) \subseteq ℝ$
8		ltso	$⊢ < Or ℝ$
9		soss	$⊢ (M \dots N) \subseteq ℝ \to (< Or ℝ \to < Or (M \dots N))$
10	7 8 9	mp2	$⊢ < Or (M \dots N)$
11		fzfi	$⊢ (M \dots N) \in Fin$
12		fz1iso	$⊢ (< Or (M \dots N) \land (M \dots N) \in Fin) \to \exists h h {Isom}_{<, <} ((1 \dots \|(M \dots N)\|), (M \dots N))$
13	10 11 12	mp2an	$⊢ \exists h h {Isom}_{<, <} ((1 \dots \|(M \dots N)\|), (M \dots N))$
14		fveq2	$⊢ H = \emptyset \to \|H\| = \|\emptyset\|$
15		hash0	$⊢ \|\emptyset\| = 0$
16	14 15	eqtrdi	$⊢ H = \emptyset \to \|H\| = 0$
17	16	oveq1d	$⊢ H = \emptyset \to \|H\| + M - 1 = 0 + M - 1$
18	4 17	eqtrid	$⊢ H = \emptyset \to N = 0 + M - 1$
19	18	oveq2d	$⊢ H = \emptyset \to (M \dots N) = (M \dots 0 + M - 1)$
20	19	adantl	$⊢ (φ \land H = \emptyset) \to (M \dots N) = (M \dots 0 + M - 1)$
21	3	zcnd	$⊢ φ \to M \in ℂ$
22		1cnd	$⊢ φ \to 1 \in ℂ$
23	21 22	subcld	$⊢ φ \to M - 1 \in ℂ$
24	23	addlidd	$⊢ φ \to 0 + M - 1 = M - 1$
25	24	oveq2d	$⊢ φ \to (M \dots 0 + M - 1) = (M \dots M - 1)$
26	3	zred	$⊢ φ \to M \in ℝ$
27	26	ltm1d	$⊢ φ \to M - 1 < M$
28		peano2zm	$⊢ M \in ℤ \to M - 1 \in ℤ$
29	3 28	syl	$⊢ φ \to M - 1 \in ℤ$
30		fzn	$⊢ (M \in ℤ \land M - 1 \in ℤ) \to (M - 1 < M \leftrightarrow (M \dots M - 1) = \emptyset)$
31	3 29 30	syl2anc	$⊢ φ \to (M - 1 < M \leftrightarrow (M \dots M - 1) = \emptyset)$
32	27 31	mpbid	$⊢ φ \to (M \dots M - 1) = \emptyset$
33	25 32	eqtrd	$⊢ φ \to (M \dots 0 + M - 1) = \emptyset$
34	33	adantr	$⊢ (φ \land H = \emptyset) \to (M \dots 0 + M - 1) = \emptyset$
35		eqcom	$⊢ H = \emptyset \leftrightarrow \emptyset = H$
36	35	bilani	$⊢ (φ \land H = \emptyset) \to \emptyset = H$
37	20 34 36	3eqtrd	$⊢ (φ \land H = \emptyset) \to (M \dots N) = H$
38	37	fveq2d	$⊢ (φ \land H = \emptyset) \to \|(M \dots N)\| = \|H\|$
39	22 21	pncan3d	$⊢ φ \to 1 + M - 1 = M$
40	39	eqcomd	$⊢ φ \to M = 1 + M - 1$
41	40	adantr	$⊢ (φ \land \neg H = \emptyset) \to M = 1 + M - 1$
42		1red	$⊢ (φ \land \neg H = \emptyset) \to 1 \in ℝ$
43		neqne	$⊢ \neg H = \emptyset \to H \neq \emptyset$
44	43	adantl	$⊢ (φ \land \neg H = \emptyset) \to H \neq \emptyset$
45	1	adantr	$⊢ (φ \land \neg H = \emptyset) \to H \in Fin$
46		hashnncl	$⊢ H \in Fin \to (\|H\| \in ℕ \leftrightarrow H \neq \emptyset)$
47	45 46	syl	$⊢ (φ \land \neg H = \emptyset) \to (\|H\| \in ℕ \leftrightarrow H \neq \emptyset)$
48	44 47	mpbird	$⊢ (φ \land \neg H = \emptyset) \to \|H\| \in ℕ$
49	48	nnred	$⊢ (φ \land \neg H = \emptyset) \to \|H\| \in ℝ$
50	29	zred	$⊢ φ \to M - 1 \in ℝ$
51	50	adantr	$⊢ (φ \land \neg H = \emptyset) \to M - 1 \in ℝ$
52	48	nnge1d	$⊢ (φ \land \neg H = \emptyset) \to 1 \leq \|H\|$
53	42 49 51 52	leadd1dd	$⊢ (φ \land \neg H = \emptyset) \to 1 + M - 1 \leq \|H\| + M - 1$
54	53 4	breqtrrdi	$⊢ (φ \land \neg H = \emptyset) \to 1 + M - 1 \leq N$
55	41 54	eqbrtrd	$⊢ (φ \land \neg H = \emptyset) \to M \leq N$
56	3	adantr	$⊢ (φ \land \neg H = \emptyset) \to M \in ℤ$
57		hashcl	$⊢ H \in Fin \to \|H\| \in ℕ_{0}$
58		nn0z	$⊢ \|H\| \in ℕ_{0} \to \|H\| \in ℤ$
59	1 57 58	3syl	$⊢ φ \to \|H\| \in ℤ$
60	59 29	zaddcld	$⊢ φ \to \|H\| + M - 1 \in ℤ$
61	4 60	eqeltrid	$⊢ φ \to N \in ℤ$
62	61	adantr	$⊢ (φ \land \neg H = \emptyset) \to N \in ℤ$
63		eluz	$⊢ (M \in ℤ \land N \in ℤ) \to (N \in ℤ_{\geq M} \leftrightarrow M \leq N)$
64	56 62 63	syl2anc	$⊢ (φ \land \neg H = \emptyset) \to (N \in ℤ_{\geq M} \leftrightarrow M \leq N)$
65	55 64	mpbird	$⊢ (φ \land \neg H = \emptyset) \to N \in ℤ_{\geq M}$
66		hashfz	$⊢ N \in ℤ_{\geq M} \to \|(M \dots N)\| = N - M + 1$
67	65 66	syl	$⊢ (φ \land \neg H = \emptyset) \to \|(M \dots N)\| = N - M + 1$
68	4	oveq1i	$⊢ N - M = \|H\| + (M - 1) - M$
69	1 57	syl	$⊢ φ \to \|H\| \in ℕ_{0}$
70	69	nn0cnd	$⊢ φ \to \|H\| \in ℂ$
71	70 23 21	addsubassd	$⊢ φ \to \|H\| + (M - 1) - M = \|H\| + (M - 1) - M$
72	68 71	eqtrid	$⊢ φ \to N - M = \|H\| + (M - 1) - M$
73	22	negcld	$⊢ φ \to - 1 \in ℂ$
74	21 22	negsubd	$⊢ φ \to M + -1 = M - 1$
75	74	eqcomd	$⊢ φ \to M - 1 = M + -1$
76	21 73 75	mvrladdd	$⊢ φ \to M - 1 - M = - 1$
77	76	oveq2d	$⊢ φ \to \|H\| + (M - 1) - M = \|H\| + -1$
78	72 77	eqtrd	$⊢ φ \to N - M = \|H\| + -1$
79	78	oveq1d	$⊢ φ \to N - M + 1 = \|H\| + -1 + 1$
80	79	adantr	$⊢ (φ \land \neg H = \emptyset) \to N - M + 1 = \|H\| + -1 + 1$
81	70 22	negsubd	$⊢ φ \to \|H\| + -1 = \|H\| - 1$
82	81	oveq1d	$⊢ φ \to \|H\| + -1 + 1 = \|H\| - 1 + 1$
83	70 22	npcand	$⊢ φ \to \|H\| - 1 + 1 = \|H\|$
84	82 83	eqtrd	$⊢ φ \to \|H\| + -1 + 1 = \|H\|$
85	84	adantr	$⊢ (φ \land \neg H = \emptyset) \to \|H\| + -1 + 1 = \|H\|$
86	67 80 85	3eqtrd	$⊢ (φ \land \neg H = \emptyset) \to \|(M \dots N)\| = \|H\|$
87	38 86	pm2.61dan	$⊢ φ \to \|(M \dots N)\| = \|H\|$
88	87	oveq2d	$⊢ φ \to (1 \dots \|(M \dots N)\|) = (1 \dots \|H\|)$
89		isoeq4	$⊢ (1 \dots \|(M \dots N)\|) = (1 \dots \|H\|) \to (h {Isom}_{<, <} ((1 \dots \|(M \dots N)\|), (M \dots N)) \leftrightarrow h {Isom}_{<, <} ((1 \dots \|H\|), (M \dots N)))$
90	88 89	syl	$⊢ φ \to (h {Isom}_{<, <} ((1 \dots \|(M \dots N)\|), (M \dots N)) \leftrightarrow h {Isom}_{<, <} ((1 \dots \|H\|), (M \dots N)))$
91	90	biimpd	$⊢ φ \to (h {Isom}_{<, <} ((1 \dots \|(M \dots N)\|), (M \dots N)) \to h {Isom}_{<, <} ((1 \dots \|H\|), (M \dots N)))$
92	91	eximdv	$⊢ φ \to (\exists h h {Isom}_{<, <} ((1 \dots \|(M \dots N)\|), (M \dots N)) \to \exists h h {Isom}_{<, <} ((1 \dots \|H\|), (M \dots N)))$
93	13 92	mpi	$⊢ φ \to \exists h h {Isom}_{<, <} ((1 \dots \|H\|), (M \dots N))$
94		fz1iso	$⊢ (< Or H \land H \in Fin) \to \exists g g {Isom}_{<, <} ((1 \dots \|H\|), H)$
95	2 1 94	syl2anc	$⊢ φ \to \exists g g {Isom}_{<, <} ((1 \dots \|H\|), H)$
96		exdistrv	$⊢ \exists h \exists g (h {Isom}_{<, <} ((1 \dots \|H\|), (M \dots N)) \land g {Isom}_{<, <} ((1 \dots \|H\|), H)) \leftrightarrow (\exists h h {Isom}_{<, <} ((1 \dots \|H\|), (M \dots N)) \land \exists g g {Isom}_{<, <} ((1 \dots \|H\|), H))$
97	93 95 96	sylanbrc	$⊢ φ \to \exists h \exists g (h {Isom}_{<, <} ((1 \dots \|H\|), (M \dots N)) \land g {Isom}_{<, <} ((1 \dots \|H\|), H))$
98		isocnv	$⊢ h {Isom}_{<, <} ((1 \dots \|H\|), (M \dots N)) \to h^{-1} {Isom}_{<, <} ((M \dots N), (1 \dots \|H\|))$
99	98	ad2antrl	$⊢ (φ \land (h {Isom}_{<, <} ((1 \dots \|H\|), (M \dots N)) \land g {Isom}_{<, <} ((1 \dots \|H\|), H))) \to h^{-1} {Isom}_{<, <} ((M \dots N), (1 \dots \|H\|))$
100		simprr	$⊢ (φ \land (h {Isom}_{<, <} ((1 \dots \|H\|), (M \dots N)) \land g {Isom}_{<, <} ((1 \dots \|H\|), H))) \to g {Isom}_{<, <} ((1 \dots \|H\|), H)$
101		isotr	$⊢ (h^{-1} {Isom}_{<, <} ((M \dots N), (1 \dots \|H\|)) \land g {Isom}_{<, <} ((1 \dots \|H\|), H)) \to (g \circ h^{-1}) {Isom}_{<, <} ((M \dots N), H)$
102	99 100 101	syl2anc	$⊢ (φ \land (h {Isom}_{<, <} ((1 \dots \|H\|), (M \dots N)) \land g {Isom}_{<, <} ((1 \dots \|H\|), H))) \to (g \circ h^{-1}) {Isom}_{<, <} ((M \dots N), H)$
103	102	ex	$⊢ φ \to ((h {Isom}_{<, <} ((1 \dots \|H\|), (M \dots N)) \land g {Isom}_{<, <} ((1 \dots \|H\|), H)) \to (g \circ h^{-1}) {Isom}_{<, <} ((M \dots N), H))$
104	103	2eximdv	$⊢ φ \to (\exists h \exists g (h {Isom}_{<, <} ((1 \dots \|H\|), (M \dots N)) \land g {Isom}_{<, <} ((1 \dots \|H\|), H)) \to \exists h \exists g (g \circ h^{-1}) {Isom}_{<, <} ((M \dots N), H))$
105	97 104	mpd	$⊢ φ \to \exists h \exists g (g \circ h^{-1}) {Isom}_{<, <} ((M \dots N), H)$
106		vex	$⊢ g \in V$
107		vex	$⊢ h \in V$
108	107	cnvex	$⊢ h^{-1} \in V$
109	106 108	coex	$⊢ g \circ h^{-1} \in V$
110		isoeq1	$⊢ f = g \circ h^{-1} \to (f {Isom}_{<, <} ((M \dots N), H) \leftrightarrow (g \circ h^{-1}) {Isom}_{<, <} ((M \dots N), H))$
111	109 110	spcev	$⊢ (g \circ h^{-1}) {Isom}_{<, <} ((M \dots N), H) \to \exists f f {Isom}_{<, <} ((M \dots N), H)$
112	111	a1i	$⊢ φ \to ((g \circ h^{-1}) {Isom}_{<, <} ((M \dots N), H) \to \exists f f {Isom}_{<, <} ((M \dots N), H))$
113	112	exlimdvv	$⊢ φ \to (\exists h \exists g (g \circ h^{-1}) {Isom}_{<, <} ((M \dots N), H) \to \exists f f {Isom}_{<, <} ((M \dots N), H))$
114	105 113	mpd	$⊢ φ \to \exists f f {Isom}_{<, <} ((M \dots N), H)$
115		ltwefz	$⊢ < We (M \dots N)$
116		wemoiso	$⊢ < We (M \dots N) \to \exists^{*} f f {Isom}_{<, <} ((M \dots N), H)$
117	115 116	mp1i	$⊢ φ \to \exists^{*} f f {Isom}_{<, <} ((M \dots N), H)$
118		df-eu	$⊢ \exists! f f {Isom}_{<, <} ((M \dots N), H) \leftrightarrow (\exists f f {Isom}_{<, <} ((M \dots N), H) \land \exists^{*} f f {Isom}_{<, <} ((M \dots N), H))$
119	114 117 118	sylanbrc	$⊢ φ \to \exists! f f {Isom}_{<, <} ((M \dots N), H)$

Metamath Proof Explorer

Theorem fzisoeu

Proof