erdszelem3

	Ref	Expression
Hypotheses	erdsze.n	$⊢ φ \to N \in ℕ$
	erdsze.f	$⊢ φ \to F : (1 \dots N) \underset{1-1}{⟶} ℝ$
	erdszelem.k	$⊢ K = (x \in (1 \dots N) ⟼ sup (\|.\| [\{y \in 𝒫 (1 \dots x) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land x \in y)\}] ℝ <))$
Assertion	erdszelem3	$⊢ A \in (1 \dots N) \to K (A) = sup (\|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}] ℝ <)$

Step	Hyp	Ref	Expression
1		erdsze.n	$⊢ φ \to N \in ℕ$
2		erdsze.f	$⊢ φ \to F : (1 \dots N) \underset{1-1}{⟶} ℝ$
3		erdszelem.k	$⊢ K = (x \in (1 \dots N) ⟼ sup (\|.\| [\{y \in 𝒫 (1 \dots x) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land x \in y)\}] ℝ <))$
4		oveq2	$⊢ x = A \to (1 \dots x) = (1 \dots A)$
5	4	pweqd	$⊢ x = A \to 𝒫 (1 \dots x) = 𝒫 (1 \dots A)$
6		eleq1	$⊢ x = A \to (x \in y \leftrightarrow A \in y)$
7	6	anbi2d	$⊢ x = A \to ((({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land x \in y) \leftrightarrow (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y))$
8	5 7	rabeqbidv	$⊢ x = A \to \{y \in 𝒫 (1 \dots x) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land x \in y)\} = \{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}$
9	8	imaeq2d	$⊢ x = A \to \|.\| [\{y \in 𝒫 (1 \dots x) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land x \in y)\}] = \|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}]$
10	9	supeq1d	$⊢ x = A \to sup (\|.\| [\{y \in 𝒫 (1 \dots x) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land x \in y)\}] ℝ <) = sup (\|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}] ℝ <)$
11		ltso	$⊢ < Or ℝ$
12	11	supex	$⊢ sup (\|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}] ℝ <) \in V$
13	10 3 12	fvmpt	$⊢ A \in (1 \dots N) \to K (A) = sup (\|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}] ℝ <)$

Metamath Proof Explorer