iccpartgt

Description: If there is a partition, then all intermediate points and the bounds are strictly ordered. (Contributed by AV, 18-Jul-2020)

	Ref	Expression
Hypotheses	iccpartgtprec.m	$⊢ φ \to M \in ℕ$
	iccpartgtprec.p	$⊢ φ \to P \in RePart (M)$
Assertion	iccpartgt	$⊢ φ \to \forall i \in (0 \dots M) \forall j \in (0 \dots M) (i < j \to P (i) < P (j))$

Proof

Step	Hyp	Ref	Expression
1		iccpartgtprec.m	$⊢ φ \to M \in ℕ$
2		iccpartgtprec.p	$⊢ φ \to P \in RePart (M)$
3	1	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
4		elnn0uz	$⊢ M \in ℕ_{0} \leftrightarrow M \in ℤ_{\geq 0}$
5	3 4	sylib	$⊢ φ \to M \in ℤ_{\geq 0}$
6		fzpred	$⊢ M \in ℤ_{\geq 0} \to (0 \dots M) = \{0\} \cup (0 + 1 \dots M)$
7	5 6	syl	$⊢ φ \to (0 \dots M) = \{0\} \cup (0 + 1 \dots M)$
8		0p1e1	$⊢ 0 + 1 = 1$
9	8	oveq1i	$⊢ (0 + 1 \dots M) = (1 \dots M)$
10	9	a1i	$⊢ φ \to (0 + 1 \dots M) = (1 \dots M)$
11	10	uneq2d	$⊢ φ \to \{0\} \cup (0 + 1 \dots M) = \{0\} \cup (1 \dots M)$
12	7 11	eqtrd	$⊢ φ \to (0 \dots M) = \{0\} \cup (1 \dots M)$
13	12	eleq2d	$⊢ φ \to (i \in (0 \dots M) \leftrightarrow i \in (\{0\} \cup (1 \dots M)))$
14		elun	$⊢ i \in (\{0\} \cup (1 \dots M)) \leftrightarrow (i \in \{0\} \lor i \in (1 \dots M))$
15		velsn	$⊢ i \in \{0\} \leftrightarrow i = 0$
16	15	orbi1i	$⊢ (i \in \{0\} \lor i \in (1 \dots M)) \leftrightarrow (i = 0 \lor i \in (1 \dots M))$
17	14 16	bitri	$⊢ i \in (\{0\} \cup (1 \dots M)) \leftrightarrow (i = 0 \lor i \in (1 \dots M))$
18		fzisfzounsn	$⊢ M \in ℤ_{\geq 0} \to (0 \dots M) = (0 ..^M) \cup \{M\}$
19	5 18	syl	$⊢ φ \to (0 \dots M) = (0 ..^M) \cup \{M\}$
20	19	eleq2d	$⊢ φ \to (j \in (0 \dots M) \leftrightarrow j \in ((0 ..^M) \cup \{M\}))$
21		elun	$⊢ j \in ((0 ..^M) \cup \{M\}) \leftrightarrow (j \in (0 ..^M) \lor j \in \{M\})$
22		velsn	$⊢ j \in \{M\} \leftrightarrow j = M$
23	22	orbi2i	$⊢ (j \in (0 ..^M) \lor j \in \{M\}) \leftrightarrow (j \in (0 ..^M) \lor j = M)$
24	21 23	bitri	$⊢ j \in ((0 ..^M) \cup \{M\}) \leftrightarrow (j \in (0 ..^M) \lor j = M)$
25	20 24	bitrdi	$⊢ φ \to (j \in (0 \dots M) \leftrightarrow (j \in (0 ..^M) \lor j = M))$
26		simpl	$⊢ (j \in (0 ..^M) \land 0 < j) \to j \in (0 ..^M)$
27		simpr	$⊢ (j \in (0 ..^M) \land 0 < j) \to 0 < j$
28	27	gt0ne0d	$⊢ (j \in (0 ..^M) \land 0 < j) \to j \neq 0$
29		fzo1fzo0n0	$⊢ j \in (1 ..^M) \leftrightarrow (j \in (0 ..^M) \land j \neq 0)$
30	26 28 29	sylanbrc	$⊢ (j \in (0 ..^M) \land 0 < j) \to j \in (1 ..^M)$
31	1 2	iccpartigtl	$⊢ φ \to \forall k \in (1 ..^M) P (0) < P (k)$
32		fveq2	$⊢ k = j \to P (k) = P (j)$
33	32	breq2d	$⊢ k = j \to (P (0) < P (k) \leftrightarrow P (0) < P (j))$
34	33	rspcv	$⊢ j \in (1 ..^M) \to (\forall k \in (1 ..^M) P (0) < P (k) \to P (0) < P (j))$
35	30 31 34	syl2imc	$⊢ φ \to ((j \in (0 ..^M) \land 0 < j) \to P (0) < P (j))$
36	35	expd	$⊢ φ \to (j \in (0 ..^M) \to (0 < j \to P (0) < P (j)))$
37	36	impcom	$⊢ (j \in (0 ..^M) \land φ) \to (0 < j \to P (0) < P (j))$
38		breq1	$⊢ i = 0 \to (i < j \leftrightarrow 0 < j)$
39		fveq2	$⊢ i = 0 \to P (i) = P (0)$
40	39	breq1d	$⊢ i = 0 \to (P (i) < P (j) \leftrightarrow P (0) < P (j))$
41	38 40	imbi12d	$⊢ i = 0 \to ((i < j \to P (i) < P (j)) \leftrightarrow (0 < j \to P (0) < P (j)))$
42	37 41	imbitrrid	$⊢ i = 0 \to ((j \in (0 ..^M) \land φ) \to (i < j \to P (i) < P (j)))$
43	42	expd	$⊢ i = 0 \to (j \in (0 ..^M) \to (φ \to (i < j \to P (i) < P (j))))$
44	43	com12	$⊢ j \in (0 ..^M) \to (i = 0 \to (φ \to (i < j \to P (i) < P (j))))$
45	1 2	iccpartlt	$⊢ φ \to P (0) < P (M)$
46		fveq2	$⊢ j = M \to P (j) = P (M)$
47	39 46	breqan12rd	$⊢ (j = M \land i = 0) \to (P (i) < P (j) \leftrightarrow P (0) < P (M))$
48	45 47	imbitrrid	$⊢ (j = M \land i = 0) \to (φ \to P (i) < P (j))$
49	48	a1dd	$⊢ (j = M \land i = 0) \to (φ \to (i < j \to P (i) < P (j)))$
50	49	ex	$⊢ j = M \to (i = 0 \to (φ \to (i < j \to P (i) < P (j))))$
51	44 50	jaoi	$⊢ (j \in (0 ..^M) \lor j = M) \to (i = 0 \to (φ \to (i < j \to P (i) < P (j))))$
52	51	com12	$⊢ i = 0 \to ((j \in (0 ..^M) \lor j = M) \to (φ \to (i < j \to P (i) < P (j))))$
53		elfzelz	$⊢ i \in (1 \dots M) \to i \in ℤ$
54	53	ad3antlr	$⊢ (((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \to i \in ℤ$
55	53	peano2zd	$⊢ i \in (1 \dots M) \to i + 1 \in ℤ$
56	55	ad2antlr	$⊢ ((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \to i + 1 \in ℤ$
57		elfzoelz	$⊢ j \in (0 ..^M) \to j \in ℤ$
58	57	ad2antrr	$⊢ ((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \to j \in ℤ$
59		simpr	$⊢ ((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \to i < j$
60	57 53	anim12ci	$⊢ (j \in (0 ..^M) \land i \in (1 \dots M)) \to (i \in ℤ \land j \in ℤ)$
61	60	adantr	$⊢ ((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \to (i \in ℤ \land j \in ℤ)$
62		zltp1le	$⊢ (i \in ℤ \land j \in ℤ) \to (i < j \leftrightarrow i + 1 \leq j)$
63	61 62	syl	$⊢ ((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \to (i < j \leftrightarrow i + 1 \leq j)$
64	59 63	mpbid	$⊢ ((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \to i + 1 \leq j$
65	56 58 64	3jca	$⊢ ((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \to (i + 1 \in ℤ \land j \in ℤ \land i + 1 \leq j)$
66	65	adantr	$⊢ (((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \to (i + 1 \in ℤ \land j \in ℤ \land i + 1 \leq j)$
67		eluz2	$⊢ j \in ℤ_{\geq (i + 1)} \leftrightarrow (i + 1 \in ℤ \land j \in ℤ \land i + 1 \leq j)$
68	66 67	sylibr	$⊢ (((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \to j \in ℤ_{\geq (i + 1)}$
69	1	ad2antlr	$⊢ ((((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \land k \in (i \dots j)) \to M \in ℕ$
70	2	ad2antlr	$⊢ ((((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \land k \in (i \dots j)) \to P \in RePart (M)$
71		1zzd	$⊢ ((((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \land k \in (i \dots j)) \to 1 \in ℤ$
72		elfzelz	$⊢ k \in (i \dots j) \to k \in ℤ$
73	72	adantl	$⊢ ((((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \land k \in (i \dots j)) \to k \in ℤ$
74		elfzle1	$⊢ i \in (1 \dots M) \to 1 \leq i$
75		elfzle1	$⊢ k \in (i \dots j) \to i \leq k$
76		1red	$⊢ k \in (i \dots j) \to 1 \in ℝ$
77		elfzel1	$⊢ k \in (i \dots j) \to i \in ℤ$
78	77	zred	$⊢ k \in (i \dots j) \to i \in ℝ$
79	72	zred	$⊢ k \in (i \dots j) \to k \in ℝ$
80		letr	$⊢ (1 \in ℝ \land i \in ℝ \land k \in ℝ) \to ((1 \leq i \land i \leq k) \to 1 \leq k)$
81	76 78 79 80	syl3anc	$⊢ k \in (i \dots j) \to ((1 \leq i \land i \leq k) \to 1 \leq k)$
82	75 81	mpan2d	$⊢ k \in (i \dots j) \to (1 \leq i \to 1 \leq k)$
83	74 82	syl5com	$⊢ i \in (1 \dots M) \to (k \in (i \dots j) \to 1 \leq k)$
84	83	ad3antlr	$⊢ (((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \to (k \in (i \dots j) \to 1 \leq k)$
85	84	imp	$⊢ ((((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \land k \in (i \dots j)) \to 1 \leq k$
86		eluz2	$⊢ k \in ℤ_{\geq 1} \leftrightarrow (1 \in ℤ \land k \in ℤ \land 1 \leq k)$
87	71 73 85 86	syl3anbrc	$⊢ ((((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \land k \in (i \dots j)) \to k \in ℤ_{\geq 1}$
88		elfzel2	$⊢ i \in (1 \dots M) \to M \in ℤ$
89	88	ad2antlr	$⊢ ((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \to M \in ℤ$
90	89	ad2antrr	$⊢ ((((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \land k \in (i \dots j)) \to M \in ℤ$
91	79	adantl	$⊢ ((((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \land k \in (i \dots j)) \to k \in ℝ$
92	57	zred	$⊢ j \in (0 ..^M) \to j \in ℝ$
93	92	ad4antr	$⊢ ((((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \land k \in (i \dots j)) \to j \in ℝ$
94	69	nnred	$⊢ ((((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \land k \in (i \dots j)) \to M \in ℝ$
95		elfzle2	$⊢ k \in (i \dots j) \to k \leq j$
96	95	adantl	$⊢ ((((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \land k \in (i \dots j)) \to k \leq j$
97		elfzolt2	$⊢ j \in (0 ..^M) \to j < M$
98	97	ad4antr	$⊢ ((((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \land k \in (i \dots j)) \to j < M$
99	91 93 94 96 98	lelttrd	$⊢ ((((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \land k \in (i \dots j)) \to k < M$
100		elfzo2	$⊢ k \in (1 ..^M) \leftrightarrow (k \in ℤ_{\geq 1} \land M \in ℤ \land k < M)$
101	87 90 99 100	syl3anbrc	$⊢ ((((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \land k \in (i \dots j)) \to k \in (1 ..^M)$
102	69 70 101	iccpartipre	$⊢ ((((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \land k \in (i \dots j)) \to P (k) \in ℝ$
103	1	ad2antlr	$⊢ ((((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \land k \in (i \dots j - 1)) \to M \in ℕ$
104	2	ad2antlr	$⊢ ((((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \land k \in (i \dots j - 1)) \to P \in RePart (M)$
105	57	ad3antrrr	$⊢ (((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \to j \in ℤ$
106		fzoval	$⊢ j \in ℤ \to (i ..^j) = (i \dots j - 1)$
107	105 106	syl	$⊢ (((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \to (i ..^j) = (i \dots j - 1)$
108		elfzo0le	$⊢ j \in (0 ..^M) \to j \leq M$
109		0le1	$⊢ 0 \leq 1$
110		0red	$⊢ i \in (1 \dots M) \to 0 \in ℝ$
111		1red	$⊢ i \in (1 \dots M) \to 1 \in ℝ$
112	53	zred	$⊢ i \in (1 \dots M) \to i \in ℝ$
113		letr	$⊢ (0 \in ℝ \land 1 \in ℝ \land i \in ℝ) \to ((0 \leq 1 \land 1 \leq i) \to 0 \leq i)$
114	110 111 112 113	syl3anc	$⊢ i \in (1 \dots M) \to ((0 \leq 1 \land 1 \leq i) \to 0 \leq i)$
115	109 114	mpani	$⊢ i \in (1 \dots M) \to (1 \leq i \to 0 \leq i)$
116	74 115	mpd	$⊢ i \in (1 \dots M) \to 0 \leq i$
117	108 116	anim12ci	$⊢ (j \in (0 ..^M) \land i \in (1 \dots M)) \to (0 \leq i \land j \leq M)$
118	117	adantr	$⊢ ((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \to (0 \leq i \land j \leq M)$
119		0zd	$⊢ j \in (0 ..^M) \to 0 \in ℤ$
120		elfzoel2	$⊢ j \in (0 ..^M) \to M \in ℤ$
121	119 120	jca	$⊢ j \in (0 ..^M) \to (0 \in ℤ \land M \in ℤ)$
122	121	ad2antrr	$⊢ ((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \to (0 \in ℤ \land M \in ℤ)$
123		ssfzo12bi	$⊢ ((i \in ℤ \land j \in ℤ) \land (0 \in ℤ \land M \in ℤ) \land i < j) \to ((i ..^j) \subseteq (0 ..^M) \leftrightarrow (0 \leq i \land j \leq M))$
124	61 122 59 123	syl3anc	$⊢ ((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \to ((i ..^j) \subseteq (0 ..^M) \leftrightarrow (0 \leq i \land j \leq M))$
125	118 124	mpbird	$⊢ ((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \to (i ..^j) \subseteq (0 ..^M)$
126	125	adantr	$⊢ (((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \to (i ..^j) \subseteq (0 ..^M)$
127	107 126	eqsstrrd	$⊢ (((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \to (i \dots j - 1) \subseteq (0 ..^M)$
128	127	sselda	$⊢ ((((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \land k \in (i \dots j - 1)) \to k \in (0 ..^M)$
129		iccpartimp	$⊢ (M \in ℕ \land P \in RePart (M) \land k \in (0 ..^M)) \to (P \in ({ℝ^{*}}^{(0 \dots M)}) \land P (k) < P (k + 1))$
130	103 104 128 129	syl3anc	$⊢ ((((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \land k \in (i \dots j - 1)) \to (P \in ({ℝ^{*}}^{(0 \dots M)}) \land P (k) < P (k + 1))$
131	130	simprd	$⊢ ((((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \land k \in (i \dots j - 1)) \to P (k) < P (k + 1)$
132	54 68 102 131	smonoord	$⊢ (((j \in (0 ..^M) \land i \in (1 \dots M)) \land i < j) \land φ) \to P (i) < P (j)$
133	132	exp31	$⊢ (j \in (0 ..^M) \land i \in (1 \dots M)) \to (i < j \to (φ \to P (i) < P (j)))$
134	133	com23	$⊢ (j \in (0 ..^M) \land i \in (1 \dots M)) \to (φ \to (i < j \to P (i) < P (j)))$
135	134	ex	$⊢ j \in (0 ..^M) \to (i \in (1 \dots M) \to (φ \to (i < j \to P (i) < P (j))))$
136		elfzuz	$⊢ i \in (1 \dots M) \to i \in ℤ_{\geq 1}$
137	136	adantr	$⊢ (i \in (1 \dots M) \land i < M) \to i \in ℤ_{\geq 1}$
138	88	adantr	$⊢ (i \in (1 \dots M) \land i < M) \to M \in ℤ$
139		simpr	$⊢ (i \in (1 \dots M) \land i < M) \to i < M$
140		elfzo2	$⊢ i \in (1 ..^M) \leftrightarrow (i \in ℤ_{\geq 1} \land M \in ℤ \land i < M)$
141	137 138 139 140	syl3anbrc	$⊢ (i \in (1 \dots M) \land i < M) \to i \in (1 ..^M)$
142	1 2	iccpartiltu	$⊢ φ \to \forall k \in (1 ..^M) P (k) < P (M)$
143		fveq2	$⊢ k = i \to P (k) = P (i)$
144	143	breq1d	$⊢ k = i \to (P (k) < P (M) \leftrightarrow P (i) < P (M))$
145	144	rspcv	$⊢ i \in (1 ..^M) \to (\forall k \in (1 ..^M) P (k) < P (M) \to P (i) < P (M))$
146	141 142 145	syl2imc	$⊢ φ \to ((i \in (1 \dots M) \land i < M) \to P (i) < P (M))$
147	146	expd	$⊢ φ \to (i \in (1 \dots M) \to (i < M \to P (i) < P (M)))$
148	147	impcom	$⊢ (i \in (1 \dots M) \land φ) \to (i < M \to P (i) < P (M))$
149	148	imp	$⊢ ((i \in (1 \dots M) \land φ) \land i < M) \to P (i) < P (M)$
150	149	a1i	$⊢ j = M \to (((i \in (1 \dots M) \land φ) \land i < M) \to P (i) < P (M))$
151		breq2	$⊢ j = M \to (i < j \leftrightarrow i < M)$
152	151	anbi2d	$⊢ j = M \to (((i \in (1 \dots M) \land φ) \land i < j) \leftrightarrow ((i \in (1 \dots M) \land φ) \land i < M))$
153	46	breq2d	$⊢ j = M \to (P (i) < P (j) \leftrightarrow P (i) < P (M))$
154	150 152 153	3imtr4d	$⊢ j = M \to (((i \in (1 \dots M) \land φ) \land i < j) \to P (i) < P (j))$
155	154	exp4c	$⊢ j = M \to (i \in (1 \dots M) \to (φ \to (i < j \to P (i) < P (j))))$
156	135 155	jaoi	$⊢ (j \in (0 ..^M) \lor j = M) \to (i \in (1 \dots M) \to (φ \to (i < j \to P (i) < P (j))))$
157	156	com12	$⊢ i \in (1 \dots M) \to ((j \in (0 ..^M) \lor j = M) \to (φ \to (i < j \to P (i) < P (j))))$
158	52 157	jaoi	$⊢ (i = 0 \lor i \in (1 \dots M)) \to ((j \in (0 ..^M) \lor j = M) \to (φ \to (i < j \to P (i) < P (j))))$
159	158	com13	$⊢ φ \to ((j \in (0 ..^M) \lor j = M) \to ((i = 0 \lor i \in (1 \dots M)) \to (i < j \to P (i) < P (j))))$
160	25 159	sylbid	$⊢ φ \to (j \in (0 \dots M) \to ((i = 0 \lor i \in (1 \dots M)) \to (i < j \to P (i) < P (j))))$
161	160	com3r	$⊢ (i = 0 \lor i \in (1 \dots M)) \to (φ \to (j \in (0 \dots M) \to (i < j \to P (i) < P (j))))$
162	17 161	sylbi	$⊢ i \in (\{0\} \cup (1 \dots M)) \to (φ \to (j \in (0 \dots M) \to (i < j \to P (i) < P (j))))$
163	162	com12	$⊢ φ \to (i \in (\{0\} \cup (1 \dots M)) \to (j \in (0 \dots M) \to (i < j \to P (i) < P (j))))$
164	13 163	sylbid	$⊢ φ \to (i \in (0 \dots M) \to (j \in (0 \dots M) \to (i < j \to P (i) < P (j))))$
165	164	imp32	$⊢ (φ \land (i \in (0 \dots M) \land j \in (0 \dots M))) \to (i < j \to P (i) < P (j))$
166	165	ralrimivva	$⊢ φ \to \forall i \in (0 \dots M) \forall j \in (0 \dots M) (i < j \to P (i) < P (j))$

Metamath Proof Explorer

Theorem iccpartgt

Proof