Metamath Proof Explorer

Theorem erdszelem6

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

		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)\}] ℝ <))$
		erdszelem.o	$⊢ O Or ℝ$
	Assertion	erdszelem6	$⊢ φ \to K : (1 \dots N) ⟶ ℕ$

Proof

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		erdszelem.o	$⊢ O Or ℝ$
5		ltso	$⊢ < Or ℝ$
6	5	supex	$⊢ sup (\|.\| [\{y \in 𝒫 (1 \dots x) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land x \in y)\}] ℝ <) \in V$
7	6	a1i	$⊢ (φ \land x \in (1 \dots N)) \to sup (\|.\| [\{y \in 𝒫 (1 \dots x) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land x \in y)\}] ℝ <) \in V$
8	3	a1i	$⊢ φ \to K = (x \in (1 \dots N) ⟼ sup (\|.\| [\{y \in 𝒫 (1 \dots x) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land x \in y)\}] ℝ <))$
9		eqid	$⊢ \{y \in 𝒫 (1 \dots z) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land z \in y)\} = \{y \in 𝒫 (1 \dots z) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land z \in y)\}$
10	9	erdszelem2	$⊢ (\|.\| [\{y \in 𝒫 (1 \dots z) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land z \in y)\}] \in Fin \land \|.\| [\{y \in 𝒫 (1 \dots z) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land z \in y)\}] \subseteq ℕ)$
11	10	simpri	$⊢ \|.\| [\{y \in 𝒫 (1 \dots z) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land z \in y)\}] \subseteq ℕ$
12	1 2 3 4	erdszelem5	$⊢ (φ \land z \in (1 \dots N)) \to K (z) \in \|.\| [\{y \in 𝒫 (1 \dots z) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land z \in y)\}]$
13	11 12	sselid	$⊢ (φ \land z \in (1 \dots N)) \to K (z) \in ℕ$
14	7 8 13	fmpt2d	$⊢ φ \to K : (1 \dots N) ⟶ ℕ$