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		simpl	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to u \underset{˙}{\sim} v$
25	24 19	sylib	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to ((u \in [0, 1] \land v \in [0, 1]) \land u - v \in ℚ)$
26	25	simpld	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to (u \in [0, 1] \land v \in [0, 1])$
27	26	simpld	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to u \in [0, 1]$
28		simpr	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to v \underset{˙}{\sim} w$
29		oveq12	$⊢ (x = v \land y = w) \to x - y = v - w$
30	29	eleq1d	$⊢ (x = v \land y = w) \to (x - y \in ℚ \leftrightarrow v - w \in ℚ)$
31	30 1	brab2a	$⊢ v \underset{˙}{\sim} w \leftrightarrow ((v \in [0, 1] \land w \in [0, 1]) \land v - w \in ℚ)$
32	28 31	sylib	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to ((v \in [0, 1] \land w \in [0, 1]) \land v - w \in ℚ)$
33	32	simpld	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to (v \in [0, 1] \land w \in [0, 1])$
34	33	simprd	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to w \in [0, 1]$
35	27 7	syl	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to u \in ℂ$
36	25 11	syl	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to v \in ℂ$
37	5 34	sselid	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to w \in ℝ$
38	37	recnd	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to w \in ℂ$
39	35 36 38	npncand	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to (u - v) + v - w = u - w$
40	25	simprd	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to u - v \in ℚ$
41	32	simprd	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to v - w \in ℚ$
42		qaddcl	$⊢ (u - v \in ℚ \land v - w \in ℚ) \to (u - v) + v - w \in ℚ$
43	40 41 42	syl2anc	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to (u - v) + v - w \in ℚ$
44	39 43	eqeltrrd	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to u - w \in ℚ$
45		oveq12	$⊢ (x = u \land y = w) \to x - y = u - w$
46	45	eleq1d	$⊢ (x = u \land y = w) \to (x - y \in ℚ \leftrightarrow u - w \in ℚ)$
47	46 1	brab2a	$⊢ u \underset{˙}{\sim} w \leftrightarrow ((u \in [0, 1] \land w \in [0, 1]) \land u - w \in ℚ)$
48	27 34 44 47	syl21anbrc	$⊢ (u \underset{˙}{\sim} v \land v \underset{˙}{\sim} w) \to u \underset{˙}{\sim} w$
49	7	subidd	$⊢ u \in [0, 1] \to u - u = 0$
50		0z	$⊢ 0 \in ℤ$
51		zq	$⊢ 0 \in ℤ \to 0 \in ℚ$
52	50 51	ax-mp	$⊢ 0 \in ℚ$
53	49 52	eqeltrdi	$⊢ u \in [0, 1] \to u - u \in ℚ$
54	53	adantr	$⊢ (u \in [0, 1] \land u \in [0, 1]) \to u - u \in ℚ$
55	54	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 ℚ)$
56		pm4.24	$⊢ u \in [0, 1] \leftrightarrow (u \in [0, 1] \land u \in [0, 1])$
57		oveq12	$⊢ (x = u \land y = u) \to x - y = u - u$
58	57	eleq1d	$⊢ (x = u \land y = u) \to (x - y \in ℚ \leftrightarrow u - u \in ℚ)$
59	58 1	brab2a	$⊢ u \underset{˙}{\sim} u \leftrightarrow ((u \in [0, 1] \land u \in [0, 1]) \land u - u \in ℚ)$
60	55 56 59	3bitr4i	$⊢ u \in [0, 1] \leftrightarrow u \underset{˙}{\sim} u$
61	2 23 48 60	iseri	$⊢ \underset{˙}{\sim} Er [0, 1]$

Metamath Proof Explorer

Theorem vitalilem1

Proof