Theorem erdszelem6

Description: Lemma for erdsze . (Contributed by Mario Carneiro, 22-Jan-2015)

	Ref	Expression
Hypotheses	erdsze.n	$$⊢\phi \to N\in \mathbb{N}$$
	erdsze.f	$$⊢\phi \to F:\left(1\dots N\right)\underset{1-1}{⟶}ℝ$$
	erdszelem.k	$$⊢K=\left(x\in \left(1\dots N\right)⟼sup\left(\left|.\right|\left[\left\{y\in 𝒫\left(1\dots x\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\wedge x\in y\right)\right\}\right],ℝ,<\right)\right)$$
	erdszelem.o	$$⊢O\mathrm{Or}ℝ$$
Assertion	erdszelem6	$$⊢\phi \to K:\left(1\dots N\right)⟶\mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		erdsze.n	$$⊢\phi \to N\in \mathbb{N}$$
2		erdsze.f	$$⊢\phi \to F:\left(1\dots N\right)\underset{1-1}{⟶}ℝ$$
3		erdszelem.k	$$⊢K=\left(x\in \left(1\dots N\right)⟼sup\left(\left|.\right|\left[\left\{y\in 𝒫\left(1\dots x\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\wedge x\in y\right)\right\}\right],ℝ,<\right)\right)$$
4		erdszelem.o	$$⊢O\mathrm{Or}ℝ$$
5		ltso	$$⊢<\mathrm{Or}ℝ$$
6	5	supex	$$⊢sup\left(\left|.\right|\left[\left\{y\in 𝒫\left(1\dots x\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\wedge x\in y\right)\right\}\right],ℝ,<\right)\in \mathrm{V}$$
7	6	a1i	$$⊢\left(\phi \wedge x\in \left(1\dots N\right)\right)\to sup\left(\left|.\right|\left[\left\{y\in 𝒫\left(1\dots x\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\wedge x\in y\right)\right\}\right],ℝ,<\right)\in \mathrm{V}$$
8	3	a1i	$$⊢\phi \to K=\left(x\in \left(1\dots N\right)⟼sup\left(\left|.\right|\left[\left\{y\in 𝒫\left(1\dots x\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\wedge x\in y\right)\right\}\right],ℝ,<\right)\right)$$
9		eqid	$$⊢\left\{y\in 𝒫\left(1\dots z\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\wedge z\in y\right)\right\}=\left\{y\in 𝒫\left(1\dots z\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\wedge z\in y\right)\right\}$$
10	9	erdszelem2	$$⊢\left(\left|.\right|\left[\left\{y\in 𝒫\left(1\dots z\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\wedge z\in y\right)\right\}\right]\in \mathrm{Fin}\wedge \left|.\right|\left[\left\{y\in 𝒫\left(1\dots z\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\wedge z\in y\right)\right\}\right]\subseteq \mathbb{N}\right)$$
11	10	simpri	$$⊢\left|.\right|\left[\left\{y\in 𝒫\left(1\dots z\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\wedge z\in y\right)\right\}\right]\subseteq \mathbb{N}$$
12	1 2 3 4	erdszelem5	$$⊢\left(\phi \wedge z\in \left(1\dots N\right)\right)\to K\left(z\right)\in \left|.\right|\left[\left\{y\in 𝒫\left(1\dots z\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\wedge z\in y\right)\right\}\right]$$
13	11 12	sseldi	$$⊢\left(\phi \wedge z\in \left(1\dots N\right)\right)\to K\left(z\right)\in \mathbb{N}$$
14	7 8 13	fmpt2d	$$⊢\phi \to K:\left(1\dots N\right)⟶\mathbb{N}$$