erdszelem4

	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	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)\}$

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		elfznn	$⊢ A \in (1 \dots N) \to A \in ℕ$
6	5	adantl	$⊢ (φ \land A \in (1 \dots N)) \to A \in ℕ$
7		elfz1end	$⊢ A \in ℕ \leftrightarrow A \in (1 \dots A)$
8	6 7	sylib	$⊢ (φ \land A \in (1 \dots N)) \to A \in (1 \dots A)$
9	8	snssd	$⊢ (φ \land A \in (1 \dots N)) \to \{A\} \subseteq (1 \dots A)$
10		elsni	$⊢ x \in \{A\} \to x = A$
11		elsni	$⊢ y \in \{A\} \to y = A$
12	10 11	breqan12d	$⊢ (x \in \{A\} \land y \in \{A\}) \to (x < y \leftrightarrow A < A)$
13	12	adantl	$⊢ ((φ \land A \in (1 \dots N)) \land (x \in \{A\} \land y \in \{A\})) \to (x < y \leftrightarrow A < A)$
14		fzssuz	$⊢ (1 \dots N) \subseteq ℤ_{\geq 1}$
15		uzssz	$⊢ ℤ_{\geq 1} \subseteq ℤ$
16		zssre	$⊢ ℤ \subseteq ℝ$
17	15 16	sstri	$⊢ ℤ_{\geq 1} \subseteq ℝ$
18	14 17	sstri	$⊢ (1 \dots N) \subseteq ℝ$
19		simpr	$⊢ (φ \land A \in (1 \dots N)) \to A \in (1 \dots N)$
20	19	adantr	$⊢ ((φ \land A \in (1 \dots N)) \land (x \in \{A\} \land y \in \{A\})) \to A \in (1 \dots N)$
21	18 20	sseldi	$⊢ ((φ \land A \in (1 \dots N)) \land (x \in \{A\} \land y \in \{A\})) \to A \in ℝ$
22	21	ltnrd	$⊢ ((φ \land A \in (1 \dots N)) \land (x \in \{A\} \land y \in \{A\})) \to \neg A < A$
23	22	pm2.21d	$⊢ ((φ \land A \in (1 \dots N)) \land (x \in \{A\} \land y \in \{A\})) \to (A < A \to F (x) O F (y))$
24	13 23	sylbid	$⊢ ((φ \land A \in (1 \dots N)) \land (x \in \{A\} \land y \in \{A\})) \to (x < y \to F (x) O F (y))$
25	24	ralrimivva	$⊢ (φ \land A \in (1 \dots N)) \to \forall x \in \{A\} \forall y \in \{A\} (x < y \to F (x) O F (y))$
26		f1f	$⊢ F : (1 \dots N) \underset{1-1}{⟶} ℝ \to F : (1 \dots N) ⟶ ℝ$
27	2 26	syl	$⊢ φ \to F : (1 \dots N) ⟶ ℝ$
28	27	adantr	$⊢ (φ \land A \in (1 \dots N)) \to F : (1 \dots N) ⟶ ℝ$
29	19	snssd	$⊢ (φ \land A \in (1 \dots N)) \to \{A\} \subseteq (1 \dots N)$
30		ltso	$⊢ < Or ℝ$
31		soss	$⊢ (1 \dots N) \subseteq ℝ \to (< Or ℝ \to < Or (1 \dots N))$
32	18 30 31	mp2	$⊢ < Or (1 \dots N)$
33		soisores	$⊢ ((< Or (1 \dots N) \land O Or ℝ) \land (F : (1 \dots N) ⟶ ℝ \land \{A\} \subseteq (1 \dots N))) \to (({F ↾}_{\{A\}}) {Isom}_{<, O} (\{A\}, F [\{A\}]) \leftrightarrow \forall x \in \{A\} \forall y \in \{A\} (x < y \to F (x) O F (y)))$
34	32 4 33	mpanl12	$⊢ (F : (1 \dots N) ⟶ ℝ \land \{A\} \subseteq (1 \dots N)) \to (({F ↾}_{\{A\}}) {Isom}_{<, O} (\{A\}, F [\{A\}]) \leftrightarrow \forall x \in \{A\} \forall y \in \{A\} (x < y \to F (x) O F (y)))$
35	28 29 34	syl2anc	$⊢ (φ \land A \in (1 \dots N)) \to (({F ↾}_{\{A\}}) {Isom}_{<, O} (\{A\}, F [\{A\}]) \leftrightarrow \forall x \in \{A\} \forall y \in \{A\} (x < y \to F (x) O F (y)))$
36	25 35	mpbird	$⊢ (φ \land A \in (1 \dots N)) \to ({F ↾}_{\{A\}}) {Isom}_{<, O} (\{A\}, F [\{A\}])$
37		snidg	$⊢ A \in (1 \dots N) \to A \in \{A\}$
38	37	adantl	$⊢ (φ \land A \in (1 \dots N)) \to A \in \{A\}$
39		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)\}$
40	39	erdszelem1	$⊢ \{A\} \in \{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\} \leftrightarrow (\{A\} \subseteq (1 \dots A) \land ({F ↾}_{\{A\}}) {Isom}_{<, O} (\{A\}, F [\{A\}]) \land A \in \{A\})$
41	9 36 38 40	syl3anbrc	$⊢ (φ \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)\}$

Metamath Proof Explorer

Theorem erdszelem4

Proof