vitalilem1

Description: Lemma for vitali . (Contributed by Mario Carneiro, 16-Jun-2014) (Proof shortened by AV, 1-May-2021)

		Ref	Expression
	Hypothesis	vitali.1	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| ((x \in [0, 1] \land y \in [0, 1]) \land x - y \in ℚ)\}$
	Assertion	vitalilem1	$⊢ \underset{˙}{\sim} Er [0, 1]$

Proof

Step	Hyp	Ref	Expression
1		vitali.1	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| ((x \in [0, 1] \land y \in [0, 1]) \land x - y \in ℚ)\}$
2	1	relopabiv	$⊢ Rel \underset{˙}{\sim}$
3		simplr	$⊢ ((u \in [0, 1] \land v \in [0, 1]) \land u - v \in ℚ) \to v \in [0, 1]$
4		simpll	$⊢ ((u \in [0, 1] \land v \in [0, 1]) \land u - v \in ℚ) \to u \in [0, 1]$
5		unitssre	$⊢ [0, 1] \subseteq ℝ$
6	5	sseli	$⊢ u \in [0, 1] \to u \in ℝ$
7	6	recnd	$⊢ u \in [0, 1] \to u \in ℂ$
8	7	ad2antrr	$⊢ ((u \in [0, 1] \land v \in [0, 1]) \land u - v \in ℚ) \to u \in ℂ$
9	5	sseli	$⊢ v \in [0, 1] \to v \in ℝ$
10	9	recnd	$⊢ v \in [0, 1] \to v \in ℂ$
11	10	ad2antlr	$⊢ ((u \in [0, 1] \land v \in [0, 1]) \land u - v \in ℚ) \to v \in ℂ$
12	8 11	negsubdi2d	$⊢ ((u \in [0, 1] \land v \in [0, 1]) \land u - v \in ℚ) \to - (u - v) = v - u$
13		qnegcl	$⊢ u - v \in ℚ \to - (u - v) \in ℚ$
14	13	adantl	$⊢ ((u \in [0, 1] \land v \in [0, 1]) \land u - v \in ℚ) \to - (u - v) \in ℚ$
15	12 14	eqeltrrd	$⊢ ((u \in [0, 1] \land v \in [0, 1]) \land u - v \in ℚ) \to v - u \in ℚ$
16	3 4 15	jca31	$⊢ ((u \in [0, 1] \land v \in [0, 1]) \land u - v \in ℚ) \to ((v \in [0, 1] \land u \in [0, 1]) \land v - u \in ℚ)$
17		oveq12	$⊢ (x = u \land y = v) \to x - y = u - v$
18	17	eleq1d	$⊢ (x = u \land y = v) \to (x - y \in ℚ \leftrightarrow u - v \in ℚ)$
19	18 1	brab2a	$⊢ u \underset{˙}{\sim} v \leftrightarrow ((u \in [0, 1] \land v \in [0, 1]) \land u - v \in ℚ)$
20		oveq12	$⊢ (x = v \land y = u) \to x - y = v - u$
21	20	eleq1d	$⊢ (x = v \land y = u) \to (x - y \in ℚ \leftrightarrow v - u \in ℚ)$
22	21 1	brab2a	$⊢ v \underset{˙}{\sim} u \leftrightarrow ((v \in [0, 1] \land u \in [0, 1]) \land v - u \in ℚ)$
23	16 19 22	3imtr4i	$⊢ u \underset{˙}{\sim} v \to v \underset{˙}{\sim} u$
24	19	birani	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to ((u \in [0, 1] \land v \in [0, 1]) \land u - v \in ℚ)$
25	24	simpld	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to (u \in [0, 1] \land v \in [0, 1])$
26	25	simpld	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to u \in [0, 1]$
27		oveq12	$⊢ (x = v \land y = w) \to x - y = v - w$
28	27	eleq1d	$⊢ (x = v \land y = w) \to (x - y \in ℚ \leftrightarrow v - w \in ℚ)$
29	28 1	brab2a	$⊢ v \underset{˙}{\sim} w \leftrightarrow ((v \in [0, 1] \land w \in [0, 1]) \land v - w \in ℚ)$
30	29	bilani	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to ((v \in [0, 1] \land w \in [0, 1]) \land v - w \in ℚ)$
31	30	simpld	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to (v \in [0, 1] \land w \in [0, 1])$
32	31	simprd	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to w \in [0, 1]$
33	26 7	syl	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to u \in ℂ$
34	24 11	syl	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to v \in ℂ$
35	5 32	sselid	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to w \in ℝ$
36	35	recnd	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to w \in ℂ$
37	33 34 36	npncand	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to (u - v) + v - w = u - w$
38	24	simprd	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to u - v \in ℚ$
39	30	simprd	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to v - w \in ℚ$
40		qaddcl	$⊢ (u - v \in ℚ \land v - w \in ℚ) \to (u - v) + v - w \in ℚ$
41	38 39 40	syl2anc	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to (u - v) + v - w \in ℚ$
42	37 41	eqeltrrd	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to u - w \in ℚ$
43		oveq12	$⊢ (x = u \land y = w) \to x - y = u - w$
44	43	eleq1d	$⊢ (x = u \land y = w) \to (x - y \in ℚ \leftrightarrow u - w \in ℚ)$
45	44 1	brab2a	$⊢ u \underset{˙}{\sim} w \leftrightarrow ((u \in [0, 1] \land w \in [0, 1]) \land u - w \in ℚ)$
46	26 32 42 45	syl21anbrc	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to u \underset{˙}{\sim} w$
47	7	subidd	$⊢ u \in [0, 1] \to u - u = 0$
48		0z	$⊢ 0 \in ℤ$
49		zq	$⊢ 0 \in ℤ \to 0 \in ℚ$
50	48 49	ax-mp	$⊢ 0 \in ℚ$
51	47 50	eqeltrdi	$⊢ u \in [0, 1] \to u - u \in ℚ$
52	51	adantr	$⊢ (u \in [0, 1] \land u \in [0, 1]) \to u - u \in ℚ$
53	52	pm4.71i	$⊢ (u \in [0, 1] \land u \in [0, 1]) \leftrightarrow ((u \in [0, 1] \land u \in [0, 1]) \land u - u \in ℚ)$
54		pm4.24	$⊢ u \in [0, 1] \leftrightarrow (u \in [0, 1] \land u \in [0, 1])$
55		oveq12	$⊢ (x = u \land y = u) \to x - y = u - u$
56	55	eleq1d	$⊢ (x = u \land y = u) \to (x - y \in ℚ \leftrightarrow u - u \in ℚ)$
57	56 1	brab2a	$⊢ u \underset{˙}{\sim} u \leftrightarrow ((u \in [0, 1] \land u \in [0, 1]) \land u - u \in ℚ)$
58	53 54 57	3bitr4i	$⊢ u \in [0, 1] \leftrightarrow u \underset{˙}{\sim} u$
59	2 23 46 58	iseri	$⊢ \underset{˙}{\sim} Er [0, 1]$

Metamath Proof Explorer

Theorem vitalilem1

Proof