Theorem fourierdlem36

Description: F is an isomorphism. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem36.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	fourierdlem36.assr	$$⊢\phi \to A\subseteq ℝ$$
	fourierdlem36.f	$$⊢F=\left(\iota f|f{Isom}_{<,<}\left(\left(0\dots N\right),A\right)\right)$$
	fourierdlem36.n	$$⊢N=\left|A\right|-1$$
Assertion	fourierdlem36	$$⊢\phi \to F{Isom}_{<,<}\left(\left(0\dots N\right),A\right)$$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem36.a	$$⊢\phi \to A\in \mathrm{Fin}$$
2		fourierdlem36.assr	$$⊢\phi \to A\subseteq ℝ$$
3		fourierdlem36.f	$$⊢F=\left(\iota f|f{Isom}_{<,<}\left(\left(0\dots N\right),A\right)\right)$$
4		fourierdlem36.n	$$⊢N=\left|A\right|-1$$
5		ltso	$$⊢<\mathrm{Or}ℝ$$
6		soss	$$⊢A\subseteq ℝ\to \left(<\mathrm{Or}ℝ\to <\mathrm{Or}A\right)$$
7	2 5 6	mpisyl	$$⊢\phi \to <\mathrm{Or}A$$
8		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
9		eqid	$$⊢\left|A\right|+0-1=\left|A\right|+0-1$$
10	1 7 8 9	fzisoeu	$$⊢\phi \to \exists !ff{Isom}_{<,<}\left(\left(0\dots \left|A\right|+0-1\right),A\right)$$
11		hashcl	$$⊢A\in \mathrm{Fin}\to \left|A\right|\in {\mathbb{N}}_0$$
12	1 11	syl	$$⊢\phi \to \left|A\right|\in {\mathbb{N}}_0$$
13	12	nn0cnd	$$⊢\phi \to \left|A\right|\in ℂ$$
14		1cnd	$$⊢\phi \to 1\in ℂ$$
15	13 14	negsubd	$$⊢\phi \to \left|A\right|+-1=\left|A\right|-1$$
16		df-neg	$$⊢-1=0-1$$
17	16	eqcomi	$$⊢0-1=-1$$
18	17	oveq2i	$$⊢\left|A\right|+0-1=\left|A\right|+-1$$
19	15 18 4	3eqtr4g	$$⊢\phi \to \left|A\right|+0-1=N$$
20	19	oveq2d	$$⊢\phi \to \left(0\dots \left|A\right|+0-1\right)=\left(0\dots N\right)$$
21		isoeq4	$$⊢\left(0\dots \left|A\right|+0-1\right)=\left(0\dots N\right)\to \left(f{Isom}_{<,<}\left(\left(0\dots \left|A\right|+0-1\right),A\right)\leftrightarrow f{Isom}_{<,<}\left(\left(0\dots N\right),A\right)\right)$$
22	20 21	syl	$$⊢\phi \to \left(f{Isom}_{<,<}\left(\left(0\dots \left|A\right|+0-1\right),A\right)\leftrightarrow f{Isom}_{<,<}\left(\left(0\dots N\right),A\right)\right)$$
23	22	eubidv	$$⊢\phi \to \left(\exists !ff{Isom}_{<,<}\left(\left(0\dots \left|A\right|+0-1\right),A\right)\leftrightarrow \exists !ff{Isom}_{<,<}\left(\left(0\dots N\right),A\right)\right)$$
24	10 23	mpbid	$$⊢\phi \to \exists !ff{Isom}_{<,<}\left(\left(0\dots N\right),A\right)$$
25		iotacl	$$⊢\exists !ff{Isom}_{<,<}\left(\left(0\dots N\right),A\right)\to \left(\iota f|f{Isom}_{<,<}\left(\left(0\dots N\right),A\right)\right)\in \left\{f|f{Isom}_{<,<}\left(\left(0\dots N\right),A\right)\right\}$$
26	24 25	syl	$$⊢\phi \to \left(\iota f|f{Isom}_{<,<}\left(\left(0\dots N\right),A\right)\right)\in \left\{f|f{Isom}_{<,<}\left(\left(0\dots N\right),A\right)\right\}$$
27	3 26	eqeltrid	$$⊢\phi \to F\in \left\{f|f{Isom}_{<,<}\left(\left(0\dots N\right),A\right)\right\}$$
28		iotaex	$$⊢\left(\iota f|f{Isom}_{<,<}\left(\left(0\dots N\right),A\right)\right)\in \mathrm{V}$$
29	3 28	eqeltri	$$⊢F\in \mathrm{V}$$
30		isoeq1	$$⊢f=F\to \left(f{Isom}_{<,<}\left(\left(0\dots N\right),A\right)\leftrightarrow F{Isom}_{<,<}\left(\left(0\dots N\right),A\right)\right)$$
31	29 30	elab	$$⊢F\in \left\{f|f{Isom}_{<,<}\left(\left(0\dots N\right),A\right)\right\}\leftrightarrow F{Isom}_{<,<}\left(\left(0\dots N\right),A\right)$$
32	27 31	sylib	$$⊢\phi \to F{Isom}_{<,<}\left(\left(0\dots N\right),A\right)$$