vitalilem3 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > vitalilem3		Structured version Visualization version GIF version

Theorem vitalilem3 25518

Description: Lemma for vitali 25521. (Contributed by Mario Carneiro, 16-Jun-2014.)

**Hypotheses**
Ref	Expression
vitali.1	⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)}
vitali.2	⊢ 𝑆 = ((0[,]1) / ∼ )
vitali.3	⊢ (𝜑 → 𝐹 Fn 𝑆)
vitali.4	⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧))
vitali.5	⊢ (𝜑 → 𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)))
vitali.6	⊢ 𝑇 = (𝑛 ∈ ℕ ↦ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹})
vitali.7	⊢ (𝜑 → ¬ ran 𝐹 ∈ (𝒫 ℝ ∖ dom vol))

**Assertion**
Ref	Expression
vitalilem3	⊢ (𝜑 → Disj 𝑚 ∈ ℕ (𝑇‘𝑚))

Distinct variable groups: 𝑚,𝑛,𝑠,𝑥,𝑦,𝑧,𝐺 𝜑,𝑚,𝑛,𝑥,𝑧 𝑧,𝑆 𝑇,𝑚,𝑥 𝑚,𝐹,𝑛,𝑠,𝑥,𝑦,𝑧 ∼ ,𝑚,𝑛,𝑠,𝑥,𝑦,𝑧 Allowed substitution hints: 𝜑(𝑦,𝑠) 𝑆(𝑥,𝑦,𝑚,𝑛,𝑠) 𝑇(𝑦,𝑧,𝑛,𝑠)

Proof of Theorem vitalilem3 Dummy variables 𝑘 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simprlr 779	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ (𝑇‘𝑚))
2		simprll 778	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑚 ∈ ℕ)
3		fveq2 6861	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → (𝐺‘𝑛) = (𝐺‘𝑚))
4	3	oveq2d 7406	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑚 → (𝑠 − (𝐺‘𝑛)) = (𝑠 − (𝐺‘𝑚)))
5	4	eleq1d 2814	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → ((𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹 ↔ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹))
6	5	rabbidv 3416	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑚 → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹} = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹})
7		vitali.6	. . . . . . . . . . . . . 14 ⊢ 𝑇 = (𝑛 ∈ ℕ ↦ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹})
8		reex 11166	. . . . . . . . . . . . . . 15 ⊢ ℝ ∈ V
9	8	rabex 5297	. . . . . . . . . . . . . 14 ⊢ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹} ∈ V
10	6, 7, 9	fvmpt 6971	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ → (𝑇‘𝑚) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹})
11	2, 10	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑇‘𝑚) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹})
12	1, 11	eleqtrd 2831	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹})
13		oveq1 7397	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑤 → (𝑠 − (𝐺‘𝑚)) = (𝑤 − (𝐺‘𝑚)))
14	13	eleq1d 2814	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑤 → ((𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹 ↔ (𝑤 − (𝐺‘𝑚)) ∈ ran 𝐹))
15	14	elrab 3662	. . . . . . . . . . 11 ⊢ (𝑤 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹} ↔ (𝑤 ∈ ℝ ∧ (𝑤 − (𝐺‘𝑚)) ∈ ran 𝐹))
16	12, 15	sylib 218	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 ∈ ℝ ∧ (𝑤 − (𝐺‘𝑚)) ∈ ran 𝐹))
17	16	simpld 494	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ ℝ)
18	17	recnd 11209	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ ℂ)
19		vitali.5	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)))
20		f1of 6803	. . . . . . . . . . . . 13 ⊢ (𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) → 𝐺:ℕ⟶(ℚ ∩ (-1[,]1)))
21	19, 20	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:ℕ⟶(ℚ ∩ (-1[,]1)))
22		inss1 4203	. . . . . . . . . . . 12 ⊢ (ℚ ∩ (-1[,]1)) ⊆ ℚ
23		fss 6707	. . . . . . . . . . . 12 ⊢ ((𝐺:ℕ⟶(ℚ ∩ (-1[,]1)) ∧ (ℚ ∩ (-1[,]1)) ⊆ ℚ) → 𝐺:ℕ⟶ℚ)
24	21, 22, 23	sylancl 586	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺:ℕ⟶ℚ)
25	24	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝐺:ℕ⟶ℚ)
26	25, 2	ffvelcdmd 7060	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑚) ∈ ℚ)
27		qcn 12929	. . . . . . . . 9 ⊢ ((𝐺‘𝑚) ∈ ℚ → (𝐺‘𝑚) ∈ ℂ)
28	26, 27	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑚) ∈ ℂ)
29		simprrl 780	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑘 ∈ ℕ)
30	25, 29	ffvelcdmd 7060	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑘) ∈ ℚ)
31		qcn 12929	. . . . . . . . 9 ⊢ ((𝐺‘𝑘) ∈ ℚ → (𝐺‘𝑘) ∈ ℂ)
32	30, 31	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑘) ∈ ℂ)
33		vitali.1	. . . . . . . . . . . . 13 ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)}
34	33	vitalilem1 25516	. . . . . . . . . . . 12 ⊢ ∼ Er (0[,]1)
35	34	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ∼ Er (0[,]1))
36		vitali.2	. . . . . . . . . . . . . . . 16 ⊢ 𝑆 = ((0[,]1) / ∼ )
37		vitali.3	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹 Fn 𝑆)
38		vitali.4	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧))
39		vitali.7	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ¬ ran 𝐹 ∈ (𝒫 ℝ ∖ dom vol))
40	33, 36, 37, 38, 19, 7, 39	vitalilem2 25517	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ran 𝐹 ⊆ (0[,]1) ∧ (0[,]1) ⊆ ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∧ ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ (-1[,]2)))
41	40	simp1d 1142	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran 𝐹 ⊆ (0[,]1))
42	41	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ran 𝐹 ⊆ (0[,]1))
43	16	simprd 495	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑚)) ∈ ran 𝐹)
44	42, 43	sseldd 3950	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑚)) ∈ (0[,]1))
45		simprrr 781	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ (𝑇‘𝑘))
46		fveq2 6861	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘))
47	46	oveq2d 7406	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑘 → (𝑠 − (𝐺‘𝑛)) = (𝑠 − (𝐺‘𝑘)))
48	47	eleq1d 2814	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → ((𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹 ↔ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹))
49	48	rabbidv 3416	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹} = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹})
50	8	rabex 5297	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹} ∈ V
51	49, 7, 50	fvmpt 6971	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ → (𝑇‘𝑘) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹})
52	29, 51	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑇‘𝑘) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹})
53	45, 52	eleqtrd 2831	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹})
54		oveq1 7397	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = 𝑤 → (𝑠 − (𝐺‘𝑘)) = (𝑤 − (𝐺‘𝑘)))
55	54	eleq1d 2814	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = 𝑤 → ((𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹 ↔ (𝑤 − (𝐺‘𝑘)) ∈ ran 𝐹))
56	55	elrab 3662	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹} ↔ (𝑤 ∈ ℝ ∧ (𝑤 − (𝐺‘𝑘)) ∈ ran 𝐹))
57	53, 56	sylib 218	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 ∈ ℝ ∧ (𝑤 − (𝐺‘𝑘)) ∈ ran 𝐹))
58	57	simprd 495	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑘)) ∈ ran 𝐹)
59	42, 58	sseldd 3950	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑘)) ∈ (0[,]1))
60	18, 28, 32	nnncan1d 11574	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘))) = ((𝐺‘𝑘) − (𝐺‘𝑚)))
61		qsubcl 12934	. . . . . . . . . . . . . 14 ⊢ (((𝐺‘𝑘) ∈ ℚ ∧ (𝐺‘𝑚) ∈ ℚ) → ((𝐺‘𝑘) − (𝐺‘𝑚)) ∈ ℚ)
62	30, 26, 61	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ((𝐺‘𝑘) − (𝐺‘𝑚)) ∈ ℚ)
63	60, 62	eqeltrd 2829	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘))) ∈ ℚ)
64		oveq12 7399	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = (𝑤 − (𝐺‘𝑚)) ∧ 𝑦 = (𝑤 − (𝐺‘𝑘))) → (𝑥 − 𝑦) = ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘))))
65	64	eleq1d 2814	. . . . . . . . . . . . 13 ⊢ ((𝑥 = (𝑤 − (𝐺‘𝑚)) ∧ 𝑦 = (𝑤 − (𝐺‘𝑘))) → ((𝑥 − 𝑦) ∈ ℚ ↔ ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘))) ∈ ℚ))
66	65, 33	brab2a 5735	. . . . . . . . . . . 12 ⊢ ((𝑤 − (𝐺‘𝑚)) ∼ (𝑤 − (𝐺‘𝑘)) ↔ (((𝑤 − (𝐺‘𝑚)) ∈ (0[,]1) ∧ (𝑤 − (𝐺‘𝑘)) ∈ (0[,]1)) ∧ ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘))) ∈ ℚ))
67	44, 59, 63, 66	syl21anbrc 1345	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑚)) ∼ (𝑤 − (𝐺‘𝑘)))
68	35, 67	erthi 8730	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → [(𝑤 − (𝐺‘𝑚))] ∼ = [(𝑤 − (𝐺‘𝑘))] ∼ )
69	68	fveq2d 6865	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐹‘[(𝑤 − (𝐺‘𝑚))] ∼ ) = (𝐹‘[(𝑤 − (𝐺‘𝑘))] ∼ ))
70		eceq1 8713	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑚)) → [𝑧] ∼ = [(𝑤 − (𝐺‘𝑚))] ∼ )
71	70	fveq2d 6865	. . . . . . . . . . 11 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑚)) → (𝐹‘[𝑧] ∼ ) = (𝐹‘[(𝑤 − (𝐺‘𝑚))] ∼ ))
72		id 22	. . . . . . . . . . 11 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑚)) → 𝑧 = (𝑤 − (𝐺‘𝑚)))
73	71, 72	eqeq12d 2746	. . . . . . . . . 10 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑚)) → ((𝐹‘[𝑧] ∼ ) = 𝑧 ↔ (𝐹‘[(𝑤 − (𝐺‘𝑚))] ∼ ) = (𝑤 − (𝐺‘𝑚))))
74		fveq2 6861	. . . . . . . . . . . . . . . . 17 ⊢ ([𝑣] ∼ = 𝑤 → (𝐹‘[𝑣] ∼ ) = (𝐹‘𝑤))
75	74	eceq1d 8714	. . . . . . . . . . . . . . . 16 ⊢ ([𝑣] ∼ = 𝑤 → [(𝐹‘[𝑣] ∼ )] ∼ = [(𝐹‘𝑤)] ∼ )
76	75	fveq2d 6865	. . . . . . . . . . . . . . 15 ⊢ ([𝑣] ∼ = 𝑤 → (𝐹‘[(𝐹‘[𝑣] ∼ )] ∼ ) = (𝐹‘[(𝐹‘𝑤)] ∼ ))
77	76, 74	eqeq12d 2746	. . . . . . . . . . . . . 14 ⊢ ([𝑣] ∼ = 𝑤 → ((𝐹‘[(𝐹‘[𝑣] ∼ )] ∼ ) = (𝐹‘[𝑣] ∼ ) ↔ (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤)))
78	34	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ∼ Er (0[,]1))
79		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝑣 ∈ (0[,]1))
80		erdm 8684	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ( ∼ Er (0[,]1) → dom ∼ = (0[,]1))
81	34, 80	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ dom ∼ = (0[,]1)
82	81	eleq2i 2821	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ dom ∼ ↔ 𝑣 ∈ (0[,]1))
83		ecdmn0 8726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ dom ∼ ↔ [𝑣] ∼ ≠ ∅)
84	82, 83	bitr3i 277	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ (0[,]1) ↔ [𝑣] ∼ ≠ ∅)
85	79, 84	sylib 218	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [𝑣] ∼ ≠ ∅)
86		neeq1 2988	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = [𝑣] ∼ → (𝑧 ≠ ∅ ↔ [𝑣] ∼ ≠ ∅))
87		fveq2 6861	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = [𝑣] ∼ → (𝐹‘𝑧) = (𝐹‘[𝑣] ∼ ))
88		id 22	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = [𝑣] ∼ → 𝑧 = [𝑣] ∼ )
89	87, 88	eleq12d 2823	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = [𝑣] ∼ → ((𝐹‘𝑧) ∈ 𝑧 ↔ (𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ ))
90	86, 89	imbi12d 344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = [𝑣] ∼ → ((𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧) ↔ ([𝑣] ∼ ≠ ∅ → (𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ )))
91	38	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧))
92		ovex 7423	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0[,]1) ∈ V
93		erex 8698	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ( ∼ Er (0[,]1) → ((0[,]1) ∈ V → ∼ ∈ V))
94	34, 92, 93	mp2 9	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∼ ∈ V
95	94	ecelqsi 8746	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ (0[,]1) → [𝑣] ∼ ∈ ((0[,]1) / ∼ ))
96	95, 36	eleqtrrdi 2840	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ (0[,]1) → [𝑣] ∼ ∈ 𝑆)
97	96	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [𝑣] ∼ ∈ 𝑆)
98	90, 91, 97	rspcdva 3592	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ([𝑣] ∼ ≠ ∅ → (𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ ))
99	85, 98	mpd 15	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ )
100		fvex 6874	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹‘[𝑣] ∼ ) ∈ V
101		vex 3454	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑣 ∈ V
102	100, 101	elec 8720	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ ↔ 𝑣 ∼ (𝐹‘[𝑣] ∼ ))
103	99, 102	sylib 218	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝑣 ∼ (𝐹‘[𝑣] ∼ ))
104	78, 103	erthi 8730	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [𝑣] ∼ = [(𝐹‘[𝑣] ∼ )] ∼ )
105	104	eqcomd 2736	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [(𝐹‘[𝑣] ∼ )] ∼ = [𝑣] ∼ )
106	105	fveq2d 6865	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝐹‘[(𝐹‘[𝑣] ∼ )] ∼ ) = (𝐹‘[𝑣] ∼ ))
107	36, 77, 106	ectocld 8758	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑆) → (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤))
108	107	ralrimiva 3126	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑤 ∈ 𝑆 (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤))
109		eceq1 8713	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝐹‘𝑤) → [𝑧] ∼ = [(𝐹‘𝑤)] ∼ )
110	109	fveq2d 6865	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑤) → (𝐹‘[𝑧] ∼ ) = (𝐹‘[(𝐹‘𝑤)] ∼ ))
111		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑤) → 𝑧 = (𝐹‘𝑤))
112	110, 111	eqeq12d 2746	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐹‘𝑤) → ((𝐹‘[𝑧] ∼ ) = 𝑧 ↔ (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤)))
113	112	ralrn 7063	. . . . . . . . . . . . 13 ⊢ (𝐹 Fn 𝑆 → (∀𝑧 ∈ ran 𝐹(𝐹‘[𝑧] ∼ ) = 𝑧 ↔ ∀𝑤 ∈ 𝑆 (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤)))
114	37, 113	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (∀𝑧 ∈ ran 𝐹(𝐹‘[𝑧] ∼ ) = 𝑧 ↔ ∀𝑤 ∈ 𝑆 (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤)))
115	108, 114	mpbird 257	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑧 ∈ ran 𝐹(𝐹‘[𝑧] ∼ ) = 𝑧)
116	115	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ∀𝑧 ∈ ran 𝐹(𝐹‘[𝑧] ∼ ) = 𝑧)
117	73, 116, 43	rspcdva 3592	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐹‘[(𝑤 − (𝐺‘𝑚))] ∼ ) = (𝑤 − (𝐺‘𝑚)))
118		eceq1 8713	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑘)) → [𝑧] ∼ = [(𝑤 − (𝐺‘𝑘))] ∼ )
119	118	fveq2d 6865	. . . . . . . . . . 11 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑘)) → (𝐹‘[𝑧] ∼ ) = (𝐹‘[(𝑤 − (𝐺‘𝑘))] ∼ ))
120		id 22	. . . . . . . . . . 11 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑘)) → 𝑧 = (𝑤 − (𝐺‘𝑘)))
121	119, 120	eqeq12d 2746	. . . . . . . . . 10 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑘)) → ((𝐹‘[𝑧] ∼ ) = 𝑧 ↔ (𝐹‘[(𝑤 − (𝐺‘𝑘))] ∼ ) = (𝑤 − (𝐺‘𝑘))))
122	121, 116, 58	rspcdva 3592	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐹‘[(𝑤 − (𝐺‘𝑘))] ∼ ) = (𝑤 − (𝐺‘𝑘)))
123	69, 117, 122	3eqtr3d 2773	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑚)) = (𝑤 − (𝐺‘𝑘)))
124	18, 28, 32, 123	subcand 11581	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑚) = (𝐺‘𝑘))
125	19	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)))
126		f1of1 6802	. . . . . . . . 9 ⊢ (𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) → 𝐺:ℕ–1-1→(ℚ ∩ (-1[,]1)))
127	125, 126	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝐺:ℕ–1-1→(ℚ ∩ (-1[,]1)))
128		f1fveq 7240	. . . . . . . 8 ⊢ ((𝐺:ℕ–1-1→(ℚ ∩ (-1[,]1)) ∧ (𝑚 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐺‘𝑚) = (𝐺‘𝑘) ↔ 𝑚 = 𝑘))
129	127, 2, 29, 128	syl12anc 836	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ((𝐺‘𝑚) = (𝐺‘𝑘) ↔ 𝑚 = 𝑘))
130	124, 129	mpbid 232	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑚 = 𝑘)
131	130	ex 412	. . . . 5 ⊢ (𝜑 → (((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘))) → 𝑚 = 𝑘))
132	131	alrimivv 1928	. . . 4 ⊢ (𝜑 → ∀𝑚∀𝑘(((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘))) → 𝑚 = 𝑘))
133		eleq1w 2812	. . . . . 6 ⊢ (𝑚 = 𝑘 → (𝑚 ∈ ℕ ↔ 𝑘 ∈ ℕ))
134		fveq2 6861	. . . . . . 7 ⊢ (𝑚 = 𝑘 → (𝑇‘𝑚) = (𝑇‘𝑘))
135	134	eleq2d 2815	. . . . . 6 ⊢ (𝑚 = 𝑘 → (𝑤 ∈ (𝑇‘𝑚) ↔ 𝑤 ∈ (𝑇‘𝑘)))
136	133, 135	anbi12d 632	. . . . 5 ⊢ (𝑚 = 𝑘 → ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ↔ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘))))
137	136	mo4 2560	. . . 4 ⊢ (∃*𝑚(𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ↔ ∀𝑚∀𝑘(((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘))) → 𝑚 = 𝑘))
138	132, 137	sylibr 234	. . 3 ⊢ (𝜑 → ∃*𝑚(𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)))
139	138	alrimiv 1927	. 2 ⊢ (𝜑 → ∀𝑤∃*𝑚(𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)))
140		dfdisj2 5079	. 2 ⊢ (Disj 𝑚 ∈ ℕ (𝑇‘𝑚) ↔ ∀𝑤∃*𝑚(𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)))
141	139, 140	sylibr 234	1 ⊢ (𝜑 → Disj 𝑚 ∈ ℕ (𝑇‘𝑚))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∀wal 1538 = wceq 1540 ∈ wcel 2109 ∃*wmo 2532 ≠ wne 2926 ∀wral 3045 {crab 3408 Vcvv 3450 ∖ cdif 3914 ∩ cin 3916 ⊆ wss 3917 ∅c0 4299 𝒫 cpw 4566 ∪ ciun 4958 Disj wdisj 5077 class class class wbr 5110 {copab 5172 ↦ cmpt 5191 dom cdm 5641 ran crn 5642 Fn wfn 6509 ⟶wf 6510 –1-1→wf1 6511 –1-1-onto→wf1o 6513 ‘cfv 6514 (class class class)co 7390 Er wer 8671 [cec 8672 / cqs 8673 ℂcc 11073 ℝcr 11074 0cc0 11075 1c1 11076 − cmin 11412 -cneg 11413 ℕcn 12193 2c2 12248 ℚcq 12914 [,]cicc 13316 volcvol 25371

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rmo 3356 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-pss 3937 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-iun 4960 df-disj 5078 df-br 5111 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5536 df-eprel 5541 df-po 5549 df-so 5550 df-fr 5594 df-we 5596 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-om 7846 df-1st 7971 df-2nd 7972 df-frecs 8263 df-wrecs 8294 df-recs 8343 df-rdg 8381 df-er 8674 df-ec 8676 df-qs 8680 df-en 8922 df-dom 8923 df-sdom 8924 df-pnf 11217 df-mnf 11218 df-xr 11219 df-ltxr 11220 df-le 11221 df-sub 11414 df-neg 11415 df-div 11843 df-nn 12194 df-2 12256 df-n0 12450 df-z 12537 df-q 12915 df-icc 13320

This theorem is referenced by: vitalilem4 25519

W3C validator