Theorem erdszelem3

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)$$
Assertion	erdszelem3	$$⊢A\in \left(1\dots N\right)\to K\left(A\right)=sup\left(\left|.\right|\left[\left\{y\in 𝒫\left(1\dots A\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\wedge A\in y\right)\right\}\right],ℝ,<\right)$$

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		oveq2	$$⊢x=A\to \left(1\dots x\right)=\left(1\dots A\right)$$
5	4	pweqd	$$⊢x=A\to 𝒫\left(1\dots x\right)=𝒫\left(1\dots A\right)$$
6		eleq1	$$⊢x=A\to \left(x\in y\leftrightarrow A\in y\right)$$
7	6	anbi2d	$$⊢x=A\to \left(\left(\left({F\upharpoonright }_y\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\wedge x\in y\right)\leftrightarrow \left(\left({F\upharpoonright }_y\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\wedge A\in y\right)\right)$$
8	5 7	rabeqbidv	$$⊢x=A\to \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\}=\left\{y\in 𝒫\left(1\dots A\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\wedge A\in y\right)\right\}$$
9	8	imaeq2d	$$⊢x=A\to \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]=\left|.\right|\left[\left\{y\in 𝒫\left(1\dots A\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\wedge A\in y\right)\right\}\right]$$
10	9	supeq1d	$$⊢x=A\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)=sup\left(\left|.\right|\left[\left\{y\in 𝒫\left(1\dots A\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\wedge A\in y\right)\right\}\right],ℝ,<\right)$$
11		ltso	$$⊢<\mathrm{Or}ℝ$$
12	11	supex	$$⊢sup\left(\left|.\right|\left[\left\{y\in 𝒫\left(1\dots A\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\wedge A\in y\right)\right\}\right],ℝ,<\right)\in \mathrm{V}$$
13	10 3 12	fvmpt	$$⊢A\in \left(1\dots N\right)\to K\left(A\right)=sup\left(\left|.\right|\left[\left\{y\in 𝒫\left(1\dots A\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\wedge A\in y\right)\right\}\right],ℝ,<\right)$$