erdszelem7

	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 ℝ$
	erdszelem.a	$⊢ φ \to A \in (1 \dots N)$
	erdszelem7.r	$⊢ φ \to R \in ℕ$
	erdszelem7.m	$⊢ φ \to \neg K (A) \in (1 \dots R - 1)$
Assertion	erdszelem7	$⊢ φ \to \exists s \in 𝒫 (1 \dots N) (R \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, O} (s, F [s]))$

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		erdszelem.a	$⊢ φ \to A \in (1 \dots N)$
6		erdszelem7.r	$⊢ φ \to R \in ℕ$
7		erdszelem7.m	$⊢ φ \to \neg K (A) \in (1 \dots R - 1)$
8		hashf	$⊢ \|.\| : V ⟶ ℕ_{0} \cup \{+∞\}$
9		ffun	$⊢ \|.\| : V ⟶ ℕ_{0} \cup \{+∞\} \to Fun \|.\|$
10	8 9	ax-mp	$⊢ Fun \|.\|$
11	1 2 3 4	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)\}]$
12	5 11	mpdan	$⊢ φ \to K (A) \in \|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}]$
13		fvelima	$⊢ (Fun \|.\| \land K (A) \in \|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}]) \to \exists s \in \{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\} \|s\| = K (A)$
14	10 12 13	sylancr	$⊢ φ \to \exists s \in \{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\} \|s\| = K (A)$
15		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)\}$
16	15	erdszelem1	$⊢ s \in \{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\} \leftrightarrow (s \subseteq (1 \dots A) \land ({F ↾}_{s}) {Isom}_{<, O} (s, F [s]) \land A \in s)$
17		simprl1	$⊢ (φ \land ((s \subseteq (1 \dots A) \land ({F ↾}_{s}) {Isom}_{<, O} (s, F [s]) \land A \in s) \land \|s\| = K (A))) \to s \subseteq (1 \dots A)$
18		elfzuz3	$⊢ A \in (1 \dots N) \to N \in ℤ_{\geq A}$
19		fzss2	$⊢ N \in ℤ_{\geq A} \to (1 \dots A) \subseteq (1 \dots N)$
20	5 18 19	3syl	$⊢ φ \to (1 \dots A) \subseteq (1 \dots N)$
21	20	adantr	$⊢ (φ \land ((s \subseteq (1 \dots A) \land ({F ↾}_{s}) {Isom}_{<, O} (s, F [s]) \land A \in s) \land \|s\| = K (A))) \to (1 \dots A) \subseteq (1 \dots N)$
22	17 21	sstrd	$⊢ (φ \land ((s \subseteq (1 \dots A) \land ({F ↾}_{s}) {Isom}_{<, O} (s, F [s]) \land A \in s) \land \|s\| = K (A))) \to s \subseteq (1 \dots N)$
23		velpw	$⊢ s \in 𝒫 (1 \dots N) \leftrightarrow s \subseteq (1 \dots N)$
24	22 23	sylibr	$⊢ (φ \land ((s \subseteq (1 \dots A) \land ({F ↾}_{s}) {Isom}_{<, O} (s, F [s]) \land A \in s) \land \|s\| = K (A))) \to s \in 𝒫 (1 \dots N)$
25	1 2 3 4	erdszelem6	$⊢ φ \to K : (1 \dots N) ⟶ ℕ$
26	25 5	ffvelcdmd	$⊢ φ \to K (A) \in ℕ$
27		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
28	26 27	eleqtrdi	$⊢ φ \to K (A) \in ℤ_{\geq 1}$
29		nnz	$⊢ R \in ℕ \to R \in ℤ$
30		peano2zm	$⊢ R \in ℤ \to R - 1 \in ℤ$
31	6 29 30	3syl	$⊢ φ \to R - 1 \in ℤ$
32		elfz5	$⊢ (K (A) \in ℤ_{\geq 1} \land R - 1 \in ℤ) \to (K (A) \in (1 \dots R - 1) \leftrightarrow K (A) \leq R - 1)$
33	28 31 32	syl2anc	$⊢ φ \to (K (A) \in (1 \dots R - 1) \leftrightarrow K (A) \leq R - 1)$
34		nnltlem1	$⊢ (K (A) \in ℕ \land R \in ℕ) \to (K (A) < R \leftrightarrow K (A) \leq R - 1)$
35	26 6 34	syl2anc	$⊢ φ \to (K (A) < R \leftrightarrow K (A) \leq R - 1)$
36	33 35	bitr4d	$⊢ φ \to (K (A) \in (1 \dots R - 1) \leftrightarrow K (A) < R)$
37	7 36	mtbid	$⊢ φ \to \neg K (A) < R$
38	6	nnred	$⊢ φ \to R \in ℝ$
39	15	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 ℕ)$
40	39	simpri	$⊢ \|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}] \subseteq ℕ$
41		nnssre	$⊢ ℕ \subseteq ℝ$
42	40 41	sstri	$⊢ \|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}] \subseteq ℝ$
43	42 12	sselid	$⊢ φ \to K (A) \in ℝ$
44	38 43	lenltd	$⊢ φ \to (R \leq K (A) \leftrightarrow \neg K (A) < R)$
45	37 44	mpbird	$⊢ φ \to R \leq K (A)$
46	45	adantr	$⊢ (φ \land ((s \subseteq (1 \dots A) \land ({F ↾}_{s}) {Isom}_{<, O} (s, F [s]) \land A \in s) \land \|s\| = K (A))) \to R \leq K (A)$
47		simprr	$⊢ (φ \land ((s \subseteq (1 \dots A) \land ({F ↾}_{s}) {Isom}_{<, O} (s, F [s]) \land A \in s) \land \|s\| = K (A))) \to \|s\| = K (A)$
48	46 47	breqtrrd	$⊢ (φ \land ((s \subseteq (1 \dots A) \land ({F ↾}_{s}) {Isom}_{<, O} (s, F [s]) \land A \in s) \land \|s\| = K (A))) \to R \leq \|s\|$
49		simprl2	$⊢ (φ \land ((s \subseteq (1 \dots A) \land ({F ↾}_{s}) {Isom}_{<, O} (s, F [s]) \land A \in s) \land \|s\| = K (A))) \to ({F ↾}_{s}) {Isom}_{<, O} (s, F [s])$
50	24 48 49	jca32	$⊢ (φ \land ((s \subseteq (1 \dots A) \land ({F ↾}_{s}) {Isom}_{<, O} (s, F [s]) \land A \in s) \land \|s\| = K (A))) \to (s \in 𝒫 (1 \dots N) \land (R \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, O} (s, F [s])))$
51	50	expr	$⊢ (φ \land (s \subseteq (1 \dots A) \land ({F ↾}_{s}) {Isom}_{<, O} (s, F [s]) \land A \in s)) \to (\|s\| = K (A) \to (s \in 𝒫 (1 \dots N) \land (R \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, O} (s, F [s]))))$
52	16 51	sylan2b	$⊢ (φ \land s \in \{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}) \to (\|s\| = K (A) \to (s \in 𝒫 (1 \dots N) \land (R \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, O} (s, F [s]))))$
53	52	expimpd	$⊢ φ \to ((s \in \{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\} \land \|s\| = K (A)) \to (s \in 𝒫 (1 \dots N) \land (R \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, O} (s, F [s]))))$
54	53	reximdv2	$⊢ φ \to (\exists s \in \{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\} \|s\| = K (A) \to \exists s \in 𝒫 (1 \dots N) (R \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, O} (s, F [s])))$
55	14 54	mpd	$⊢ φ \to \exists s \in 𝒫 (1 \dots N) (R \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, O} (s, F [s]))$

Metamath Proof Explorer

Theorem erdszelem7

Proof