erdszelem10

	Ref	Expression
Hypotheses	erdsze.n	$⊢ φ \to N \in ℕ$
	erdsze.f	$⊢ φ \to F : (1 \dots N) \underset{1-1}{⟶} ℝ$
	erdszelem.i	$⊢ I = (x \in (1 \dots N) ⟼ sup (\|.\| [\{y \in 𝒫 (1 \dots x) \| (({F ↾}_{y}) {Isom}_{<, <} (y, F [y]) \land x \in y)\}] ℝ <))$
	erdszelem.j	$⊢ J = (x \in (1 \dots N) ⟼ sup (\|.\| [\{y \in 𝒫 (1 \dots x) \| (({F ↾}_{y}) {Isom}_{<, <^{-1}} (y, F [y]) \land x \in y)\}] ℝ <))$
	erdszelem.t	$⊢ T = (n \in (1 \dots N) ⟼ ⟨I (n), J (n)⟩)$
	erdszelem.r	$⊢ φ \to R \in ℕ$
	erdszelem.s	$⊢ φ \to S \in ℕ$
	erdszelem.m	$⊢ φ \to (R - 1) (S - 1) < N$
Assertion	erdszelem10	$⊢ φ \to \exists m \in (1 \dots N) (\neg I (m) \in (1 \dots R - 1) \lor \neg J (m) \in (1 \dots S - 1))$

Proof

Step	Hyp	Ref	Expression
1		erdsze.n	$⊢ φ \to N \in ℕ$
2		erdsze.f	$⊢ φ \to F : (1 \dots N) \underset{1-1}{⟶} ℝ$
3		erdszelem.i	$⊢ I = (x \in (1 \dots N) ⟼ sup (\|.\| [\{y \in 𝒫 (1 \dots x) \| (({F ↾}_{y}) {Isom}_{<, <} (y, F [y]) \land x \in y)\}] ℝ <))$
4		erdszelem.j	$⊢ J = (x \in (1 \dots N) ⟼ sup (\|.\| [\{y \in 𝒫 (1 \dots x) \| (({F ↾}_{y}) {Isom}_{<, <^{-1}} (y, F [y]) \land x \in y)\}] ℝ <))$
5		erdszelem.t	$⊢ T = (n \in (1 \dots N) ⟼ ⟨I (n), J (n)⟩)$
6		erdszelem.r	$⊢ φ \to R \in ℕ$
7		erdszelem.s	$⊢ φ \to S \in ℕ$
8		erdszelem.m	$⊢ φ \to (R - 1) (S - 1) < N$
9		fzfi	$⊢ (1 \dots R - 1) \in Fin$
10		fzfi	$⊢ (1 \dots S - 1) \in Fin$
11		xpfi	$⊢ ((1 \dots R - 1) \in Fin \land (1 \dots S - 1) \in Fin) \to (1 \dots R - 1) \times (1 \dots S - 1) \in Fin$
12	9 10 11	mp2an	$⊢ (1 \dots R - 1) \times (1 \dots S - 1) \in Fin$
13		ssdomg	$⊢ (1 \dots R - 1) \times (1 \dots S - 1) \in Fin \to (ran T \subseteq (1 \dots R - 1) \times (1 \dots S - 1) \to ran T ≼ ((1 \dots R - 1) \times (1 \dots S - 1)))$
14	12 13	ax-mp	$⊢ ran T \subseteq (1 \dots R - 1) \times (1 \dots S - 1) \to ran T ≼ ((1 \dots R - 1) \times (1 \dots S - 1))$
15		domnsym	$⊢ ran T ≼ ((1 \dots R - 1) \times (1 \dots S - 1)) \to \neg ((1 \dots R - 1) \times (1 \dots S - 1)) ≺ ran T$
16	14 15	syl	$⊢ ran T \subseteq (1 \dots R - 1) \times (1 \dots S - 1) \to \neg ((1 \dots R - 1) \times (1 \dots S - 1)) ≺ ran T$
17		hashxp	$⊢ ((1 \dots R - 1) \in Fin \land (1 \dots S - 1) \in Fin) \to \|(1 \dots R - 1) \times (1 \dots S - 1)\| = \|(1 \dots R - 1)\| \|(1 \dots S - 1)\|$
18	9 10 17	mp2an	$⊢ \|(1 \dots R - 1) \times (1 \dots S - 1)\| = \|(1 \dots R - 1)\| \|(1 \dots S - 1)\|$
19		nnm1nn0	$⊢ R \in ℕ \to R - 1 \in ℕ_{0}$
20		hashfz1	$⊢ R - 1 \in ℕ_{0} \to \|(1 \dots R - 1)\| = R - 1$
21	6 19 20	3syl	$⊢ φ \to \|(1 \dots R - 1)\| = R - 1$
22		nnm1nn0	$⊢ S \in ℕ \to S - 1 \in ℕ_{0}$
23		hashfz1	$⊢ S - 1 \in ℕ_{0} \to \|(1 \dots S - 1)\| = S - 1$
24	7 22 23	3syl	$⊢ φ \to \|(1 \dots S - 1)\| = S - 1$
25	21 24	oveq12d	$⊢ φ \to \|(1 \dots R - 1)\| \|(1 \dots S - 1)\| = (R - 1) (S - 1)$
26	18 25	syl5eq	$⊢ φ \to \|(1 \dots R - 1) \times (1 \dots S - 1)\| = (R - 1) (S - 1)$
27	1	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
28		hashfz1	$⊢ N \in ℕ_{0} \to \|(1 \dots N)\| = N$
29	27 28	syl	$⊢ φ \to \|(1 \dots N)\| = N$
30	8 26 29	3brtr4d	$⊢ φ \to \|(1 \dots R - 1) \times (1 \dots S - 1)\| < \|(1 \dots N)\|$
31		fzfid	$⊢ φ \to (1 \dots N) \in Fin$
32		hashsdom	$⊢ ((1 \dots R - 1) \times (1 \dots S - 1) \in Fin \land (1 \dots N) \in Fin) \to (\|(1 \dots R - 1) \times (1 \dots S - 1)\| < \|(1 \dots N)\| \leftrightarrow ((1 \dots R - 1) \times (1 \dots S - 1)) ≺ (1 \dots N))$
33	12 31 32	sylancr	$⊢ φ \to (\|(1 \dots R - 1) \times (1 \dots S - 1)\| < \|(1 \dots N)\| \leftrightarrow ((1 \dots R - 1) \times (1 \dots S - 1)) ≺ (1 \dots N))$
34	30 33	mpbid	$⊢ φ \to ((1 \dots R - 1) \times (1 \dots S - 1)) ≺ (1 \dots N)$
35	1 2 3 4 5	erdszelem9	$⊢ φ \to T : (1 \dots N) \underset{1-1}{⟶} ℕ \times ℕ$
36		f1f1orn	$⊢ T : (1 \dots N) \underset{1-1}{⟶} ℕ \times ℕ \to T : (1 \dots N) \underset{1-1 onto}{⟶} ran T$
37		ovex	$⊢ (1 \dots N) \in V$
38	37	f1oen	$⊢ T : (1 \dots N) \underset{1-1 onto}{⟶} ran T \to (1 \dots N) \approx ran T$
39	35 36 38	3syl	$⊢ φ \to (1 \dots N) \approx ran T$
40		sdomentr	$⊢ (((1 \dots R - 1) \times (1 \dots S - 1)) ≺ (1 \dots N) \land (1 \dots N) \approx ran T) \to ((1 \dots R - 1) \times (1 \dots S - 1)) ≺ ran T$
41	34 39 40	syl2anc	$⊢ φ \to ((1 \dots R - 1) \times (1 \dots S - 1)) ≺ ran T$
42	16 41	nsyl3	$⊢ φ \to \neg ran T \subseteq (1 \dots R - 1) \times (1 \dots S - 1)$
43		nss	$⊢ \neg ran T \subseteq (1 \dots R - 1) \times (1 \dots S - 1) \leftrightarrow \exists s (s \in ran T \land \neg s \in ((1 \dots R - 1) \times (1 \dots S - 1)))$
44		df-rex	$⊢ \exists s \in ran T \neg s \in ((1 \dots R - 1) \times (1 \dots S - 1)) \leftrightarrow \exists s (s \in ran T \land \neg s \in ((1 \dots R - 1) \times (1 \dots S - 1)))$
45	43 44	bitr4i	$⊢ \neg ran T \subseteq (1 \dots R - 1) \times (1 \dots S - 1) \leftrightarrow \exists s \in ran T \neg s \in ((1 \dots R - 1) \times (1 \dots S - 1))$
46	42 45	sylib	$⊢ φ \to \exists s \in ran T \neg s \in ((1 \dots R - 1) \times (1 \dots S - 1))$
47		f1fn	$⊢ T : (1 \dots N) \underset{1-1}{⟶} ℕ \times ℕ \to T Fn (1 \dots N)$
48		eleq1	$⊢ s = T (m) \to (s \in ((1 \dots R - 1) \times (1 \dots S - 1)) \leftrightarrow T (m) \in ((1 \dots R - 1) \times (1 \dots S - 1)))$
49	48	notbid	$⊢ s = T (m) \to (\neg s \in ((1 \dots R - 1) \times (1 \dots S - 1)) \leftrightarrow \neg T (m) \in ((1 \dots R - 1) \times (1 \dots S - 1)))$
50	49	rexrn	$⊢ T Fn (1 \dots N) \to (\exists s \in ran T \neg s \in ((1 \dots R - 1) \times (1 \dots S - 1)) \leftrightarrow \exists m \in (1 \dots N) \neg T (m) \in ((1 \dots R - 1) \times (1 \dots S - 1)))$
51	35 47 50	3syl	$⊢ φ \to (\exists s \in ran T \neg s \in ((1 \dots R - 1) \times (1 \dots S - 1)) \leftrightarrow \exists m \in (1 \dots N) \neg T (m) \in ((1 \dots R - 1) \times (1 \dots S - 1)))$
52	46 51	mpbid	$⊢ φ \to \exists m \in (1 \dots N) \neg T (m) \in ((1 \dots R - 1) \times (1 \dots S - 1))$
53		fveq2	$⊢ n = m \to I (n) = I (m)$
54		fveq2	$⊢ n = m \to J (n) = J (m)$
55	53 54	opeq12d	$⊢ n = m \to ⟨I (n), J (n)⟩ = ⟨I (m), J (m)⟩$
56		opex	$⊢ ⟨I (m), J (m)⟩ \in V$
57	55 5 56	fvmpt	$⊢ m \in (1 \dots N) \to T (m) = ⟨I (m), J (m)⟩$
58	57	adantl	$⊢ (φ \land m \in (1 \dots N)) \to T (m) = ⟨I (m), J (m)⟩$
59	58	eleq1d	$⊢ (φ \land m \in (1 \dots N)) \to (T (m) \in ((1 \dots R - 1) \times (1 \dots S - 1)) \leftrightarrow ⟨I (m), J (m)⟩ \in ((1 \dots R - 1) \times (1 \dots S - 1)))$
60		opelxp	$⊢ ⟨I (m), J (m)⟩ \in ((1 \dots R - 1) \times (1 \dots S - 1)) \leftrightarrow (I (m) \in (1 \dots R - 1) \land J (m) \in (1 \dots S - 1))$
61	59 60	syl6bb	$⊢ (φ \land m \in (1 \dots N)) \to (T (m) \in ((1 \dots R - 1) \times (1 \dots S - 1)) \leftrightarrow (I (m) \in (1 \dots R - 1) \land J (m) \in (1 \dots S - 1)))$
62	61	notbid	$⊢ (φ \land m \in (1 \dots N)) \to (\neg T (m) \in ((1 \dots R - 1) \times (1 \dots S - 1)) \leftrightarrow \neg (I (m) \in (1 \dots R - 1) \land J (m) \in (1 \dots S - 1)))$
63		ianor	$⊢ \neg (I (m) \in (1 \dots R - 1) \land J (m) \in (1 \dots S - 1)) \leftrightarrow (\neg I (m) \in (1 \dots R - 1) \lor \neg J (m) \in (1 \dots S - 1))$
64	62 63	syl6bb	$⊢ (φ \land m \in (1 \dots N)) \to (\neg T (m) \in ((1 \dots R - 1) \times (1 \dots S - 1)) \leftrightarrow (\neg I (m) \in (1 \dots R - 1) \lor \neg J (m) \in (1 \dots S - 1)))$
65	64	rexbidva	$⊢ φ \to (\exists m \in (1 \dots N) \neg T (m) \in ((1 \dots R - 1) \times (1 \dots S - 1)) \leftrightarrow \exists m \in (1 \dots N) (\neg I (m) \in (1 \dots R - 1) \lor \neg J (m) \in (1 \dots S - 1)))$
66	52 65	mpbid	$⊢ φ \to \exists m \in (1 \dots N) (\neg I (m) \in (1 \dots R - 1) \lor \neg J (m) \in (1 \dots S - 1))$

Metamath Proof Explorer

Theorem erdszelem10

Proof