icceuelpart

Description: An element of a partitioned half-open interval of extended reals is an element of exactly one part of the partition. (Contributed by AV, 19-Jul-2020)

	Ref	Expression
Hypotheses	iccpartiun.m	$⊢ φ \to M \in ℕ$
	iccpartiun.p	$⊢ φ \to P \in RePart (M)$
Assertion	icceuelpart	$⊢ (φ \land X \in [P (0), P (M))) \to \exists! i \in (0 ..^M) X \in [P (i), P (i + 1))$

Proof

Step	Hyp	Ref	Expression
1		iccpartiun.m	$⊢ φ \to M \in ℕ$
2		iccpartiun.p	$⊢ φ \to P \in RePart (M)$
3	2	adantr	$⊢ (φ \land X \in [P (0), P (M))) \to P \in RePart (M)$
4		iccelpart	$⊢ M \in ℕ \to \forall p \in RePart (M) (X \in [p (0), p (M)) \to \exists i \in (0 ..^M) X \in [p (i), p (i + 1)))$
5	1 4	syl	$⊢ φ \to \forall p \in RePart (M) (X \in [p (0), p (M)) \to \exists i \in (0 ..^M) X \in [p (i), p (i + 1)))$
6	5	adantr	$⊢ (φ \land X \in [P (0), P (M))) \to \forall p \in RePart (M) (X \in [p (0), p (M)) \to \exists i \in (0 ..^M) X \in [p (i), p (i + 1)))$
7		fveq1	$⊢ p = P \to p (0) = P (0)$
8		fveq1	$⊢ p = P \to p (M) = P (M)$
9	7 8	oveq12d	$⊢ p = P \to [p (0), p (M)) = [P (0), P (M))$
10	9	eleq2d	$⊢ p = P \to (X \in [p (0), p (M)) \leftrightarrow X \in [P (0), P (M)))$
11		fveq1	$⊢ p = P \to p (i) = P (i)$
12		fveq1	$⊢ p = P \to p (i + 1) = P (i + 1)$
13	11 12	oveq12d	$⊢ p = P \to [p (i), p (i + 1)) = [P (i), P (i + 1))$
14	13	eleq2d	$⊢ p = P \to (X \in [p (i), p (i + 1)) \leftrightarrow X \in [P (i), P (i + 1)))$
15	14	rexbidv	$⊢ p = P \to (\exists i \in (0 ..^M) X \in [p (i), p (i + 1)) \leftrightarrow \exists i \in (0 ..^M) X \in [P (i), P (i + 1)))$
16	10 15	imbi12d	$⊢ p = P \to ((X \in [p (0), p (M)) \to \exists i \in (0 ..^M) X \in [p (i), p (i + 1))) \leftrightarrow (X \in [P (0), P (M)) \to \exists i \in (0 ..^M) X \in [P (i), P (i + 1))))$
17	16	rspcva	$⊢ (P \in RePart (M) \land \forall p \in RePart (M) (X \in [p (0), p (M)) \to \exists i \in (0 ..^M) X \in [p (i), p (i + 1)))) \to (X \in [P (0), P (M)) \to \exists i \in (0 ..^M) X \in [P (i), P (i + 1)))$
18	17	adantld	$⊢ (P \in RePart (M) \land \forall p \in RePart (M) (X \in [p (0), p (M)) \to \exists i \in (0 ..^M) X \in [p (i), p (i + 1)))) \to ((φ \land X \in [P (0), P (M))) \to \exists i \in (0 ..^M) X \in [P (i), P (i + 1)))$
19	18	com12	$⊢ (φ \land X \in [P (0), P (M))) \to ((P \in RePart (M) \land \forall p \in RePart (M) (X \in [p (0), p (M)) \to \exists i \in (0 ..^M) X \in [p (i), p (i + 1)))) \to \exists i \in (0 ..^M) X \in [P (i), P (i + 1)))$
20	3 6 19	mp2and	$⊢ (φ \land X \in [P (0), P (M))) \to \exists i \in (0 ..^M) X \in [P (i), P (i + 1))$
21	1	adantr	$⊢ (φ \land i \in (0 ..^M)) \to M \in ℕ$
22	2	adantr	$⊢ (φ \land i \in (0 ..^M)) \to P \in RePart (M)$
23		elfzofz	$⊢ i \in (0 ..^M) \to i \in (0 \dots M)$
24	23	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 \dots M)$
25	21 22 24	iccpartxr	$⊢ (φ \land i \in (0 ..^M)) \to P (i) \in ℝ^{*}$
26		fzofzp1	$⊢ i \in (0 ..^M) \to i + 1 \in (0 \dots M)$
27	26	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i + 1 \in (0 \dots M)$
28	21 22 27	iccpartxr	$⊢ (φ \land i \in (0 ..^M)) \to P (i + 1) \in ℝ^{*}$
29	25 28	jca	$⊢ (φ \land i \in (0 ..^M)) \to (P (i) \in ℝ^{} \land P (i + 1) \in ℝ^{})$
30	29	adantrr	$⊢ (φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \to (P (i) \in ℝ^{} \land P (i + 1) \in ℝ^{})$
31		elico1	$⊢ (P (i) \in ℝ^{} \land P (i + 1) \in ℝ^{}) \to (X \in [P (i), P (i + 1)) \leftrightarrow (X \in ℝ^{*} \land P (i) \leq X \land X < P (i + 1)))$
32	30 31	syl	$⊢ (φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \to (X \in [P (i), P (i + 1)) \leftrightarrow (X \in ℝ^{*} \land P (i) \leq X \land X < P (i + 1)))$
33	1	adantr	$⊢ (φ \land j \in (0 ..^M)) \to M \in ℕ$
34	2	adantr	$⊢ (φ \land j \in (0 ..^M)) \to P \in RePart (M)$
35		elfzofz	$⊢ j \in (0 ..^M) \to j \in (0 \dots M)$
36	35	adantl	$⊢ (φ \land j \in (0 ..^M)) \to j \in (0 \dots M)$
37	33 34 36	iccpartxr	$⊢ (φ \land j \in (0 ..^M)) \to P (j) \in ℝ^{*}$
38		fzofzp1	$⊢ j \in (0 ..^M) \to j + 1 \in (0 \dots M)$
39	38	adantl	$⊢ (φ \land j \in (0 ..^M)) \to j + 1 \in (0 \dots M)$
40	33 34 39	iccpartxr	$⊢ (φ \land j \in (0 ..^M)) \to P (j + 1) \in ℝ^{*}$
41	37 40	jca	$⊢ (φ \land j \in (0 ..^M)) \to (P (j) \in ℝ^{} \land P (j + 1) \in ℝ^{})$
42	41	adantrl	$⊢ (φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \to (P (j) \in ℝ^{} \land P (j + 1) \in ℝ^{})$
43		elico1	$⊢ (P (j) \in ℝ^{} \land P (j + 1) \in ℝ^{}) \to (X \in [P (j), P (j + 1)) \leftrightarrow (X \in ℝ^{*} \land P (j) \leq X \land X < P (j + 1)))$
44	42 43	syl	$⊢ (φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \to (X \in [P (j), P (j + 1)) \leftrightarrow (X \in ℝ^{*} \land P (j) \leq X \land X < P (j + 1)))$
45	32 44	anbi12d	$⊢ (φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \to ((X \in [P (i), P (i + 1)) \land X \in [P (j), P (j + 1))) \leftrightarrow ((X \in ℝ^{} \land P (i) \leq X \land X < P (i + 1)) \land (X \in ℝ^{} \land P (j) \leq X \land X < P (j + 1))))$
46		elfzoelz	$⊢ i \in (0 ..^M) \to i \in ℤ$
47	46	zred	$⊢ i \in (0 ..^M) \to i \in ℝ$
48		elfzoelz	$⊢ j \in (0 ..^M) \to j \in ℤ$
49	48	zred	$⊢ j \in (0 ..^M) \to j \in ℝ$
50	47 49	anim12i	$⊢ (i \in (0 ..^M) \land j \in (0 ..^M)) \to (i \in ℝ \land j \in ℝ)$
51	50	adantl	$⊢ (φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \to (i \in ℝ \land j \in ℝ)$
52		lttri4	$⊢ (i \in ℝ \land j \in ℝ) \to (i < j \lor i = j \lor j < i)$
53	51 52	syl	$⊢ (φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \to (i < j \lor i = j \lor j < i)$
54	1 2	icceuelpartlem	$⊢ φ \to ((i \in (0 ..^M) \land j \in (0 ..^M)) \to (i < j \to P (i + 1) \leq P (j)))$
55	54	imp31	$⊢ ((φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \land i < j) \to P (i + 1) \leq P (j)$
56		simpl	$⊢ (X \in ℝ^{} \land (φ \land (i \in (0 ..^M) \land j \in (0 ..^M)))) \to X \in ℝ^{}$
57	28	adantrr	$⊢ (φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \to P (i + 1) \in ℝ^{*}$
58	57	adantl	$⊢ (X \in ℝ^{} \land (φ \land (i \in (0 ..^M) \land j \in (0 ..^M)))) \to P (i + 1) \in ℝ^{}$
59	37	adantrl	$⊢ (φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \to P (j) \in ℝ^{*}$
60	59	adantl	$⊢ (X \in ℝ^{} \land (φ \land (i \in (0 ..^M) \land j \in (0 ..^M)))) \to P (j) \in ℝ^{}$
61		nltle2tri	$⊢ (X \in ℝ^{} \land P (i + 1) \in ℝ^{} \land P (j) \in ℝ^{*}) \to \neg (X < P (i + 1) \land P (i + 1) \leq P (j) \land P (j) \leq X)$
62	56 58 60 61	syl3anc	$⊢ (X \in ℝ^{*} \land (φ \land (i \in (0 ..^M) \land j \in (0 ..^M)))) \to \neg (X < P (i + 1) \land P (i + 1) \leq P (j) \land P (j) \leq X)$
63	62	pm2.21d	$⊢ (X \in ℝ^{*} \land (φ \land (i \in (0 ..^M) \land j \in (0 ..^M)))) \to ((X < P (i + 1) \land P (i + 1) \leq P (j) \land P (j) \leq X) \to i = j)$
64	63	3expd	$⊢ (X \in ℝ^{*} \land (φ \land (i \in (0 ..^M) \land j \in (0 ..^M)))) \to (X < P (i + 1) \to (P (i + 1) \leq P (j) \to (P (j) \leq X \to i = j)))$
65	64	ex	$⊢ X \in ℝ^{*} \to ((φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \to (X < P (i + 1) \to (P (i + 1) \leq P (j) \to (P (j) \leq X \to i = j))))$
66	65	com23	$⊢ X \in ℝ^{*} \to (X < P (i + 1) \to ((φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \to (P (i + 1) \leq P (j) \to (P (j) \leq X \to i = j))))$
67	66	com25	$⊢ X \in ℝ^{*} \to (P (j) \leq X \to ((φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \to (P (i + 1) \leq P (j) \to (X < P (i + 1) \to i = j))))$
68	67	imp4b	$⊢ (X \in ℝ^{*} \land P (j) \leq X) \to (((φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \land P (i + 1) \leq P (j)) \to (X < P (i + 1) \to i = j))$
69	68	com23	$⊢ (X \in ℝ^{*} \land P (j) \leq X) \to (X < P (i + 1) \to (((φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \land P (i + 1) \leq P (j)) \to i = j))$
70	69	3adant3	$⊢ (X \in ℝ^{*} \land P (j) \leq X \land X < P (j + 1)) \to (X < P (i + 1) \to (((φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \land P (i + 1) \leq P (j)) \to i = j))$
71	70	com12	$⊢ X < P (i + 1) \to ((X \in ℝ^{*} \land P (j) \leq X \land X < P (j + 1)) \to (((φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \land P (i + 1) \leq P (j)) \to i = j))$
72	71	3ad2ant3	$⊢ (X \in ℝ^{} \land P (i) \leq X \land X < P (i + 1)) \to ((X \in ℝ^{} \land P (j) \leq X \land X < P (j + 1)) \to (((φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \land P (i + 1) \leq P (j)) \to i = j))$
73	72	imp	$⊢ ((X \in ℝ^{} \land P (i) \leq X \land X < P (i + 1)) \land (X \in ℝ^{} \land P (j) \leq X \land X < P (j + 1))) \to (((φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \land P (i + 1) \leq P (j)) \to i = j)$
74	73	com12	$⊢ ((φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \land P (i + 1) \leq P (j)) \to (((X \in ℝ^{} \land P (i) \leq X \land X < P (i + 1)) \land (X \in ℝ^{} \land P (j) \leq X \land X < P (j + 1))) \to i = j)$
75	55 74	syldan	$⊢ ((φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \land i < j) \to (((X \in ℝ^{} \land P (i) \leq X \land X < P (i + 1)) \land (X \in ℝ^{} \land P (j) \leq X \land X < P (j + 1))) \to i = j)$
76	75	expcom	$⊢ i < j \to ((φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \to (((X \in ℝ^{} \land P (i) \leq X \land X < P (i + 1)) \land (X \in ℝ^{} \land P (j) \leq X \land X < P (j + 1))) \to i = j))$
77		2a1	$⊢ i = j \to ((φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \to (((X \in ℝ^{} \land P (i) \leq X \land X < P (i + 1)) \land (X \in ℝ^{} \land P (j) \leq X \land X < P (j + 1))) \to i = j))$
78	1 2	icceuelpartlem	$⊢ φ \to ((j \in (0 ..^M) \land i \in (0 ..^M)) \to (j < i \to P (j + 1) \leq P (i)))$
79	78	ancomsd	$⊢ φ \to ((i \in (0 ..^M) \land j \in (0 ..^M)) \to (j < i \to P (j + 1) \leq P (i)))$
80	79	imp31	$⊢ ((φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \land j < i) \to P (j + 1) \leq P (i)$
81	40	adantrl	$⊢ (φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \to P (j + 1) \in ℝ^{*}$
82	81	adantl	$⊢ (X \in ℝ^{} \land (φ \land (i \in (0 ..^M) \land j \in (0 ..^M)))) \to P (j + 1) \in ℝ^{}$
83	25	adantrr	$⊢ (φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \to P (i) \in ℝ^{*}$
84	83	adantl	$⊢ (X \in ℝ^{} \land (φ \land (i \in (0 ..^M) \land j \in (0 ..^M)))) \to P (i) \in ℝ^{}$
85		nltle2tri	$⊢ (X \in ℝ^{} \land P (j + 1) \in ℝ^{} \land P (i) \in ℝ^{*}) \to \neg (X < P (j + 1) \land P (j + 1) \leq P (i) \land P (i) \leq X)$
86	56 82 84 85	syl3anc	$⊢ (X \in ℝ^{*} \land (φ \land (i \in (0 ..^M) \land j \in (0 ..^M)))) \to \neg (X < P (j + 1) \land P (j + 1) \leq P (i) \land P (i) \leq X)$
87	86	pm2.21d	$⊢ (X \in ℝ^{*} \land (φ \land (i \in (0 ..^M) \land j \in (0 ..^M)))) \to ((X < P (j + 1) \land P (j + 1) \leq P (i) \land P (i) \leq X) \to i = j)$
88	87	3expd	$⊢ (X \in ℝ^{*} \land (φ \land (i \in (0 ..^M) \land j \in (0 ..^M)))) \to (X < P (j + 1) \to (P (j + 1) \leq P (i) \to (P (i) \leq X \to i = j)))$
89	88	ex	$⊢ X \in ℝ^{*} \to ((φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \to (X < P (j + 1) \to (P (j + 1) \leq P (i) \to (P (i) \leq X \to i = j))))$
90	89	com23	$⊢ X \in ℝ^{*} \to (X < P (j + 1) \to ((φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \to (P (j + 1) \leq P (i) \to (P (i) \leq X \to i = j))))$
91	90	imp4b	$⊢ (X \in ℝ^{*} \land X < P (j + 1)) \to (((φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \land P (j + 1) \leq P (i)) \to (P (i) \leq X \to i = j))$
92	91	com23	$⊢ (X \in ℝ^{*} \land X < P (j + 1)) \to (P (i) \leq X \to (((φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \land P (j + 1) \leq P (i)) \to i = j))$
93	92	3adant2	$⊢ (X \in ℝ^{*} \land P (j) \leq X \land X < P (j + 1)) \to (P (i) \leq X \to (((φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \land P (j + 1) \leq P (i)) \to i = j))$
94	93	com12	$⊢ P (i) \leq X \to ((X \in ℝ^{*} \land P (j) \leq X \land X < P (j + 1)) \to (((φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \land P (j + 1) \leq P (i)) \to i = j))$
95	94	3ad2ant2	$⊢ (X \in ℝ^{} \land P (i) \leq X \land X < P (i + 1)) \to ((X \in ℝ^{} \land P (j) \leq X \land X < P (j + 1)) \to (((φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \land P (j + 1) \leq P (i)) \to i = j))$
96	95	imp	$⊢ ((X \in ℝ^{} \land P (i) \leq X \land X < P (i + 1)) \land (X \in ℝ^{} \land P (j) \leq X \land X < P (j + 1))) \to (((φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \land P (j + 1) \leq P (i)) \to i = j)$
97	96	com12	$⊢ ((φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \land P (j + 1) \leq P (i)) \to (((X \in ℝ^{} \land P (i) \leq X \land X < P (i + 1)) \land (X \in ℝ^{} \land P (j) \leq X \land X < P (j + 1))) \to i = j)$
98	80 97	syldan	$⊢ ((φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \land j < i) \to (((X \in ℝ^{} \land P (i) \leq X \land X < P (i + 1)) \land (X \in ℝ^{} \land P (j) \leq X \land X < P (j + 1))) \to i = j)$
99	98	expcom	$⊢ j < i \to ((φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \to (((X \in ℝ^{} \land P (i) \leq X \land X < P (i + 1)) \land (X \in ℝ^{} \land P (j) \leq X \land X < P (j + 1))) \to i = j))$
100	76 77 99	3jaoi	$⊢ (i < j \lor i = j \lor j < i) \to ((φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \to (((X \in ℝ^{} \land P (i) \leq X \land X < P (i + 1)) \land (X \in ℝ^{} \land P (j) \leq X \land X < P (j + 1))) \to i = j))$
101	53 100	mpcom	$⊢ (φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \to (((X \in ℝ^{} \land P (i) \leq X \land X < P (i + 1)) \land (X \in ℝ^{} \land P (j) \leq X \land X < P (j + 1))) \to i = j)$
102	45 101	sylbid	$⊢ (φ \land (i \in (0 ..^M) \land j \in (0 ..^M))) \to ((X \in [P (i), P (i + 1)) \land X \in [P (j), P (j + 1))) \to i = j)$
103	102	ralrimivva	$⊢ φ \to \forall i \in (0 ..^M) \forall j \in (0 ..^M) ((X \in [P (i), P (i + 1)) \land X \in [P (j), P (j + 1))) \to i = j)$
104	103	adantr	$⊢ (φ \land X \in [P (0), P (M))) \to \forall i \in (0 ..^M) \forall j \in (0 ..^M) ((X \in [P (i), P (i + 1)) \land X \in [P (j), P (j + 1))) \to i = j)$
105		fveq2	$⊢ i = j \to P (i) = P (j)$
106		fvoveq1	$⊢ i = j \to P (i + 1) = P (j + 1)$
107	105 106	oveq12d	$⊢ i = j \to [P (i), P (i + 1)) = [P (j), P (j + 1))$
108	107	eleq2d	$⊢ i = j \to (X \in [P (i), P (i + 1)) \leftrightarrow X \in [P (j), P (j + 1)))$
109	108	reu4	$⊢ \exists! i \in (0 ..^M) X \in [P (i), P (i + 1)) \leftrightarrow (\exists i \in (0 ..^M) X \in [P (i), P (i + 1)) \land \forall i \in (0 ..^M) \forall j \in (0 ..^M) ((X \in [P (i), P (i + 1)) \land X \in [P (j), P (j + 1))) \to i = j))$
110	20 104 109	sylanbrc	$⊢ (φ \land X \in [P (0), P (M))) \to \exists! i \in (0 ..^M) X \in [P (i), P (i + 1))$

Metamath Proof Explorer

Theorem icceuelpart

Proof