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	syl5eq	$⊢ 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	addid2d	$⊢ φ \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	biimpi	$⊢ H = \emptyset \to \emptyset = H$
37	36	adantl	$⊢ (φ \land H = \emptyset) \to \emptyset = H$
38	20 34 37	3eqtrd	$⊢ (φ \land H = \emptyset) \to (M \dots N) = H$
39	38	fveq2d	$⊢ (φ \land H = \emptyset) \to \|(M \dots N)\| = \|H\|$
40	22 21	pncan3d	$⊢ φ \to 1 + M - 1 = M$
41	40	eqcomd	$⊢ φ \to M = 1 + M - 1$
42	41	adantr	$⊢ (φ \land \neg H = \emptyset) \to M = 1 + M - 1$
43		1red	$⊢ (φ \land \neg H = \emptyset) \to 1 \in ℝ$
44		neqne	$⊢ \neg H = \emptyset \to H \neq \emptyset$
45	44	adantl	$⊢ (φ \land \neg H = \emptyset) \to H \neq \emptyset$
46	1	adantr	$⊢ (φ \land \neg H = \emptyset) \to H \in Fin$
47		hashnncl	$⊢ H \in Fin \to (\|H\| \in ℕ \leftrightarrow H \neq \emptyset)$
48	46 47	syl	$⊢ (φ \land \neg H = \emptyset) \to (\|H\| \in ℕ \leftrightarrow H \neq \emptyset)$
49	45 48	mpbird	$⊢ (φ \land \neg H = \emptyset) \to \|H\| \in ℕ$
50	49	nnred	$⊢ (φ \land \neg H = \emptyset) \to \|H\| \in ℝ$
51	29	zred	$⊢ φ \to M - 1 \in ℝ$
52	51	adantr	$⊢ (φ \land \neg H = \emptyset) \to M - 1 \in ℝ$
53	49	nnge1d	$⊢ (φ \land \neg H = \emptyset) \to 1 \leq \|H\|$
54	43 50 52 53	leadd1dd	$⊢ (φ \land \neg H = \emptyset) \to 1 + M - 1 \leq \|H\| + M - 1$
55	54 4	breqtrrdi	$⊢ (φ \land \neg H = \emptyset) \to 1 + M - 1 \leq N$
56	42 55	eqbrtrd	$⊢ (φ \land \neg H = \emptyset) \to M \leq N$
57	3	adantr	$⊢ (φ \land \neg H = \emptyset) \to M \in ℤ$
58		hashcl	$⊢ H \in Fin \to \|H\| \in ℕ_{0}$
59		nn0z	$⊢ \|H\| \in ℕ_{0} \to \|H\| \in ℤ$
60	1 58 59	3syl	$⊢ φ \to \|H\| \in ℤ$
61	60 29	zaddcld	$⊢ φ \to \|H\| + M - 1 \in ℤ$
62	4 61	eqeltrid	$⊢ φ \to N \in ℤ$
63	62	adantr	$⊢ (φ \land \neg H = \emptyset) \to N \in ℤ$
64		eluz	$⊢ (M \in ℤ \land N \in ℤ) \to (N \in ℤ_{\geq M} \leftrightarrow M \leq N)$
65	57 63 64	syl2anc	$⊢ (φ \land \neg H = \emptyset) \to (N \in ℤ_{\geq M} \leftrightarrow M \leq N)$
66	56 65	mpbird	$⊢ (φ \land \neg H = \emptyset) \to N \in ℤ_{\geq M}$
67		hashfz	$⊢ N \in ℤ_{\geq M} \to \|(M \dots N)\| = N - M + 1$
68	66 67	syl	$⊢ (φ \land \neg H = \emptyset) \to \|(M \dots N)\| = N - M + 1$
69	4	oveq1i	$⊢ N - M = \|H\| + (M - 1) - M$
70	1 58	syl	$⊢ φ \to \|H\| \in ℕ_{0}$
71	70	nn0cnd	$⊢ φ \to \|H\| \in ℂ$
72	71 23 21	addsubassd	$⊢ φ \to \|H\| + (M - 1) - M = \|H\| + (M - 1) - M$
73	69 72	syl5eq	$⊢ φ \to N - M = \|H\| + (M - 1) - M$
74	22	negcld	$⊢ φ \to - 1 \in ℂ$
75	21 22	negsubd	$⊢ φ \to M + -1 = M - 1$
76	75	eqcomd	$⊢ φ \to M - 1 = M + -1$
77	21 74 76	mvrladdd	$⊢ φ \to M - 1 - M = - 1$
78	77	oveq2d	$⊢ φ \to \|H\| + (M - 1) - M = \|H\| + -1$
79	73 78	eqtrd	$⊢ φ \to N - M = \|H\| + -1$
80	79	oveq1d	$⊢ φ \to N - M + 1 = \|H\| + -1 + 1$
81	80	adantr	$⊢ (φ \land \neg H = \emptyset) \to N - M + 1 = \|H\| + -1 + 1$
82	71 22	negsubd	$⊢ φ \to \|H\| + -1 = \|H\| - 1$
83	82	oveq1d	$⊢ φ \to \|H\| + -1 + 1 = \|H\| - 1 + 1$
84	71 22	npcand	$⊢ φ \to \|H\| - 1 + 1 = \|H\|$
85	83 84	eqtrd	$⊢ φ \to \|H\| + -1 + 1 = \|H\|$
86	85	adantr	$⊢ (φ \land \neg H = \emptyset) \to \|H\| + -1 + 1 = \|H\|$
87	68 81 86	3eqtrd	$⊢ (φ \land \neg H = \emptyset) \to \|(M \dots N)\| = \|H\|$
88	39 87	pm2.61dan	$⊢ φ \to \|(M \dots N)\| = \|H\|$
89	88	oveq2d	$⊢ φ \to (1 \dots \|(M \dots N)\|) = (1 \dots \|H\|)$
90		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)))$
91	89 90	syl	$⊢ φ \to (h {Isom}_{<, <} ((1 \dots \|(M \dots N)\|), (M \dots N)) \leftrightarrow h {Isom}_{<, <} ((1 \dots \|H\|), (M \dots N)))$
92	91	biimpd	$⊢ φ \to (h {Isom}_{<, <} ((1 \dots \|(M \dots N)\|), (M \dots N)) \to h {Isom}_{<, <} ((1 \dots \|H\|), (M \dots N)))$
93	92	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)))$
94	13 93	mpi	$⊢ φ \to \exists h h {Isom}_{<, <} ((1 \dots \|H\|), (M \dots N))$
95		fz1iso	$⊢ (< Or H \land H \in Fin) \to \exists g g {Isom}_{<, <} ((1 \dots \|H\|), H)$
96	2 1 95	syl2anc	$⊢ φ \to \exists g g {Isom}_{<, <} ((1 \dots \|H\|), H)$
97		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))$
98	94 96 97	sylanbrc	$⊢ φ \to \exists h \exists g (h {Isom}_{<, <} ((1 \dots \|H\|), (M \dots N)) \land g {Isom}_{<, <} ((1 \dots \|H\|), H))$
99		isocnv	$⊢ h {Isom}_{<, <} ((1 \dots \|H\|), (M \dots N)) \to h^{-1} {Isom}_{<, <} ((M \dots N), (1 \dots \|H\|))$
100	99	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\|))$
101		simprr	$⊢ (φ \land (h {Isom}_{<, <} ((1 \dots \|H\|), (M \dots N)) \land g {Isom}_{<, <} ((1 \dots \|H\|), H))) \to g {Isom}_{<, <} ((1 \dots \|H\|), H)$
102		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)$
103	100 101 102	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)$
104	103	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))$
105	104	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))$
106	98 105	mpd	$⊢ φ \to \exists h \exists g (g \circ h^{-1}) {Isom}_{<, <} ((M \dots N), H)$
107		vex	$⊢ g \in V$
108		vex	$⊢ h \in V$
109	108	cnvex	$⊢ h^{-1} \in V$
110	107 109	coex	$⊢ g \circ h^{-1} \in V$
111		isoeq1	$⊢ f = g \circ h^{-1} \to (f {Isom}_{<, <} ((M \dots N), H) \leftrightarrow (g \circ h^{-1}) {Isom}_{<, <} ((M \dots N), H))$
112	110 111	spcev	$⊢ (g \circ h^{-1}) {Isom}_{<, <} ((M \dots N), H) \to \exists f f {Isom}_{<, <} ((M \dots N), H)$
113	112	a1i	$⊢ φ \to ((g \circ h^{-1}) {Isom}_{<, <} ((M \dots N), H) \to \exists f f {Isom}_{<, <} ((M \dots N), H))$
114	113	exlimdvv	$⊢ φ \to (\exists h \exists g (g \circ h^{-1}) {Isom}_{<, <} ((M \dots N), H) \to \exists f f {Isom}_{<, <} ((M \dots N), H))$
115	106 114	mpd	$⊢ φ \to \exists f f {Isom}_{<, <} ((M \dots N), H)$
116		ltwefz	$⊢ < We (M \dots N)$
117		wemoiso	$⊢ < We (M \dots N) \to \exists^{*} f f {Isom}_{<, <} ((M \dots N), H)$
118	116 117	mp1i	$⊢ φ \to \exists^{*} f f {Isom}_{<, <} ((M \dots N), H)$
119		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))$
120	115 118 119	sylanbrc	$⊢ φ \to \exists! f f {Isom}_{<, <} ((M \dots N), H)$

Metamath Proof Explorer

Theorem fzisoeu

Proof