erdszelem5

	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	erdszelem5	$⊢ (φ \land A \in (1 \dots N)) \to K (A) \in \|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}]$

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	1 2 3	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)\}] ℝ <)$
6	5	adantl	$⊢ (φ \land 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)\}] ℝ <)$
7		snex	$⊢ \{A\} \in V$
8		hashf	$⊢ \|.\| : V ⟶ ℕ_{0} \cup \{+∞\}$
9	8	fdmi	$⊢ dom \|.\| = V$
10	7 9	eleqtrri	$⊢ \{A\} \in dom \|.\|$
11	1 2 3 4	erdszelem4	$⊢ (φ \land A \in (1 \dots N)) \to \{A\} \in \{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}$
12		inelcm	$⊢ (\{A\} \in dom \|.\| \land \{A\} \in \{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}) \to dom \|.\| \cap \{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\} \neq \emptyset$
13	10 11 12	sylancr	$⊢ (φ \land A \in (1 \dots N)) \to dom \|.\| \cap \{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\} \neq \emptyset$
14		imadisj	$⊢ \|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}] = \emptyset \leftrightarrow dom \|.\| \cap \{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\} = \emptyset$
15	14	necon3bii	$⊢ \|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}] \neq \emptyset \leftrightarrow dom \|.\| \cap \{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\} \neq \emptyset$
16	13 15	sylibr	$⊢ (φ \land A \in (1 \dots N)) \to \|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}] \neq \emptyset$
17		eqid	$⊢ \{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\} = \{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}$
18	17	erdszelem2	$⊢ (\|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}] \in Fin \land \|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}] \subseteq ℕ)$
19	18	simpli	$⊢ \|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}] \in Fin$
20	18	simpri	$⊢ \|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}] \subseteq ℕ$
21		nnssre	$⊢ ℕ \subseteq ℝ$
22	20 21	sstri	$⊢ \|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}] \subseteq ℝ$
23		ltso	$⊢ < Or ℝ$
24		fisupcl	$⊢ (< Or ℝ \land (\|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}] \in Fin \land \|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}] \neq \emptyset \land \|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}] \subseteq ℝ)) \to sup (\|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}] ℝ <) \in \|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}]$
25	23 24	mpan	$⊢ (\|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}] \in Fin \land \|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}] \neq \emptyset \land \|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}] \subseteq ℝ) \to sup (\|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}] ℝ <) \in \|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}]$
26	19 22 25	mp3an13	$⊢ \|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}] \neq \emptyset \to sup (\|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}] ℝ <) \in \|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}]$
27	16 26	syl	$⊢ (φ \land A \in (1 \dots N)) \to sup (\|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}] ℝ <) \in \|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}]$
28	6 27	eqeltrd	$⊢ (φ \land A \in (1 \dots N)) \to K (A) \in \|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}]$

Metamath Proof Explorer

Theorem erdszelem5

Proof