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 25509

Description: Lemma for vitali 25512. (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 6822	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → (𝐺‘𝑛) = (𝐺‘𝑚))
4	3	oveq2d 7365	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑚 → (𝑠 − (𝐺‘𝑛)) = (𝑠 − (𝐺‘𝑚)))
5	4	eleq1d 2813	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → ((𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹 ↔ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹))
6	5	rabbidv 3402	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑚 → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹} = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹})
7		vitali.6	. . . . . . . . . . . . . 14 ⊢ 𝑇 = (𝑛 ∈ ℕ ↦ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹})
8		reex 11100	. . . . . . . . . . . . . . 15 ⊢ ℝ ∈ V
9	8	rabex 5278	. . . . . . . . . . . . . 14 ⊢ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹} ∈ V
10	6, 7, 9	fvmpt 6930	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ → (𝑇‘𝑚) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹})
11	2, 10	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑇‘𝑚) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹})
12	1, 11	eleqtrd 2830	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹})
13		oveq1 7356	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑤 → (𝑠 − (𝐺‘𝑚)) = (𝑤 − (𝐺‘𝑚)))
14	13	eleq1d 2813	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑤 → ((𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹 ↔ (𝑤 − (𝐺‘𝑚)) ∈ ran 𝐹))
15	14	elrab 3648	. . . . . . . . . . 11 ⊢ (𝑤 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹} ↔ (𝑤 ∈ ℝ ∧ (𝑤 − (𝐺‘𝑚)) ∈ ran 𝐹))
16	12, 15	sylib 218	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 ∈ ℝ ∧ (𝑤 − (𝐺‘𝑚)) ∈ ran 𝐹))
17	16	simpld 494	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ ℝ)
18	17	recnd 11143	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ ℂ)
19		vitali.5	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)))
20		f1of 6764	. . . . . . . . . . . . 13 ⊢ (𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) → 𝐺:ℕ⟶(ℚ ∩ (-1[,]1)))
21	19, 20	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:ℕ⟶(ℚ ∩ (-1[,]1)))
22		inss1 4188	. . . . . . . . . . . 12 ⊢ (ℚ ∩ (-1[,]1)) ⊆ ℚ
23		fss 6668	. . . . . . . . . . . 12 ⊢ ((𝐺:ℕ⟶(ℚ ∩ (-1[,]1)) ∧ (ℚ ∩ (-1[,]1)) ⊆ ℚ) → 𝐺:ℕ⟶ℚ)
24	21, 22, 23	sylancl 586	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺:ℕ⟶ℚ)
25	24	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝐺:ℕ⟶ℚ)
26	25, 2	ffvelcdmd 7019	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑚) ∈ ℚ)
27		qcn 12864	. . . . . . . . 9 ⊢ ((𝐺‘𝑚) ∈ ℚ → (𝐺‘𝑚) ∈ ℂ)
28	26, 27	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑚) ∈ ℂ)
29		simprrl 780	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑘 ∈ ℕ)
30	25, 29	ffvelcdmd 7019	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑘) ∈ ℚ)
31		qcn 12864	. . . . . . . . 9 ⊢ ((𝐺‘𝑘) ∈ ℚ → (𝐺‘𝑘) ∈ ℂ)
32	30, 31	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑘) ∈ ℂ)
33		vitali.1	. . . . . . . . . . . . 13 ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)}
34	33	vitalilem1 25507	. . . . . . . . . . . 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 25508	. . . . . . . . . . . . . . 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 3936	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑚)) ∈ (0[,]1))
45		simprrr 781	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ (𝑇‘𝑘))
46		fveq2 6822	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘))
47	46	oveq2d 7365	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑘 → (𝑠 − (𝐺‘𝑛)) = (𝑠 − (𝐺‘𝑘)))
48	47	eleq1d 2813	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → ((𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹 ↔ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹))
49	48	rabbidv 3402	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹} = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹})
50	8	rabex 5278	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹} ∈ V
51	49, 7, 50	fvmpt 6930	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ → (𝑇‘𝑘) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹})
52	29, 51	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑇‘𝑘) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹})
53	45, 52	eleqtrd 2830	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹})
54		oveq1 7356	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = 𝑤 → (𝑠 − (𝐺‘𝑘)) = (𝑤 − (𝐺‘𝑘)))
55	54	eleq1d 2813	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = 𝑤 → ((𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹 ↔ (𝑤 − (𝐺‘𝑘)) ∈ ran 𝐹))
56	55	elrab 3648	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹} ↔ (𝑤 ∈ ℝ ∧ (𝑤 − (𝐺‘𝑘)) ∈ ran 𝐹))
57	53, 56	sylib 218	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 ∈ ℝ ∧ (𝑤 − (𝐺‘𝑘)) ∈ ran 𝐹))
58	57	simprd 495	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑘)) ∈ ran 𝐹)
59	42, 58	sseldd 3936	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑘)) ∈ (0[,]1))
60	18, 28, 32	nnncan1d 11509	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘))) = ((𝐺‘𝑘) − (𝐺‘𝑚)))
61		qsubcl 12869	. . . . . . . . . . . . . 14 ⊢ (((𝐺‘𝑘) ∈ ℚ ∧ (𝐺‘𝑚) ∈ ℚ) → ((𝐺‘𝑘) − (𝐺‘𝑚)) ∈ ℚ)
62	30, 26, 61	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ((𝐺‘𝑘) − (𝐺‘𝑚)) ∈ ℚ)
63	60, 62	eqeltrd 2828	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘))) ∈ ℚ)
64		oveq12 7358	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = (𝑤 − (𝐺‘𝑚)) ∧ 𝑦 = (𝑤 − (𝐺‘𝑘))) → (𝑥 − 𝑦) = ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘))))
65	64	eleq1d 2813	. . . . . . . . . . . . 13 ⊢ ((𝑥 = (𝑤 − (𝐺‘𝑚)) ∧ 𝑦 = (𝑤 − (𝐺‘𝑘))) → ((𝑥 − 𝑦) ∈ ℚ ↔ ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘))) ∈ ℚ))
66	65, 33	brab2a 5712	. . . . . . . . . . . 12 ⊢ ((𝑤 − (𝐺‘𝑚)) ∼ (𝑤 − (𝐺‘𝑘)) ↔ (((𝑤 − (𝐺‘𝑚)) ∈ (0[,]1) ∧ (𝑤 − (𝐺‘𝑘)) ∈ (0[,]1)) ∧ ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘))) ∈ ℚ))
67	44, 59, 63, 66	syl21anbrc 1345	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑚)) ∼ (𝑤 − (𝐺‘𝑘)))
68	35, 67	erthi 8681	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → [(𝑤 − (𝐺‘𝑚))] ∼ = [(𝑤 − (𝐺‘𝑘))] ∼ )
69	68	fveq2d 6826	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐹‘[(𝑤 − (𝐺‘𝑚))] ∼ ) = (𝐹‘[(𝑤 − (𝐺‘𝑘))] ∼ ))
70		eceq1 8664	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑚)) → [𝑧] ∼ = [(𝑤 − (𝐺‘𝑚))] ∼ )
71	70	fveq2d 6826	. . . . . . . . . . 11 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑚)) → (𝐹‘[𝑧] ∼ ) = (𝐹‘[(𝑤 − (𝐺‘𝑚))] ∼ ))
72		id 22	. . . . . . . . . . 11 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑚)) → 𝑧 = (𝑤 − (𝐺‘𝑚)))
73	71, 72	eqeq12d 2745	. . . . . . . . . 10 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑚)) → ((𝐹‘[𝑧] ∼ ) = 𝑧 ↔ (𝐹‘[(𝑤 − (𝐺‘𝑚))] ∼ ) = (𝑤 − (𝐺‘𝑚))))
74		fveq2 6822	. . . . . . . . . . . . . . . . 17 ⊢ ([𝑣] ∼ = 𝑤 → (𝐹‘[𝑣] ∼ ) = (𝐹‘𝑤))
75	74	eceq1d 8665	. . . . . . . . . . . . . . . 16 ⊢ ([𝑣] ∼ = 𝑤 → [(𝐹‘[𝑣] ∼ )] ∼ = [(𝐹‘𝑤)] ∼ )
76	75	fveq2d 6826	. . . . . . . . . . . . . . 15 ⊢ ([𝑣] ∼ = 𝑤 → (𝐹‘[(𝐹‘[𝑣] ∼ )] ∼ ) = (𝐹‘[(𝐹‘𝑤)] ∼ ))
77	76, 74	eqeq12d 2745	. . . . . . . . . . . . . 14 ⊢ ([𝑣] ∼ = 𝑤 → ((𝐹‘[(𝐹‘[𝑣] ∼ )] ∼ ) = (𝐹‘[𝑣] ∼ ) ↔ (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤)))
78	34	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ∼ Er (0[,]1))
79		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝑣 ∈ (0[,]1))
80		erdm 8635	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ( ∼ Er (0[,]1) → dom ∼ = (0[,]1))
81	34, 80	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ dom ∼ = (0[,]1)
82	81	eleq2i 2820	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ dom ∼ ↔ 𝑣 ∈ (0[,]1))
83		ecdmn0 8677	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ dom ∼ ↔ [𝑣] ∼ ≠ ∅)
84	82, 83	bitr3i 277	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ (0[,]1) ↔ [𝑣] ∼ ≠ ∅)
85	79, 84	sylib 218	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [𝑣] ∼ ≠ ∅)
86		neeq1 2987	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = [𝑣] ∼ → (𝑧 ≠ ∅ ↔ [𝑣] ∼ ≠ ∅))
87		fveq2 6822	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = [𝑣] ∼ → (𝐹‘𝑧) = (𝐹‘[𝑣] ∼ ))
88		id 22	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = [𝑣] ∼ → 𝑧 = [𝑣] ∼ )
89	87, 88	eleq12d 2822	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = [𝑣] ∼ → ((𝐹‘𝑧) ∈ 𝑧 ↔ (𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ ))
90	86, 89	imbi12d 344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = [𝑣] ∼ → ((𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧) ↔ ([𝑣] ∼ ≠ ∅ → (𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ )))
91	38	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧))
92		ovex 7382	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0[,]1) ∈ V
93		erex 8649	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ( ∼ Er (0[,]1) → ((0[,]1) ∈ V → ∼ ∈ V))
94	34, 92, 93	mp2 9	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∼ ∈ V
95	94	ecelqsi 8697	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ (0[,]1) → [𝑣] ∼ ∈ ((0[,]1) / ∼ ))
96	95, 36	eleqtrrdi 2839	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ (0[,]1) → [𝑣] ∼ ∈ 𝑆)
97	96	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [𝑣] ∼ ∈ 𝑆)
98	90, 91, 97	rspcdva 3578	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ([𝑣] ∼ ≠ ∅ → (𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ ))
99	85, 98	mpd 15	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ )
100		fvex 6835	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹‘[𝑣] ∼ ) ∈ V
101		vex 3440	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑣 ∈ V
102	100, 101	elec 8671	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ ↔ 𝑣 ∼ (𝐹‘[𝑣] ∼ ))
103	99, 102	sylib 218	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝑣 ∼ (𝐹‘[𝑣] ∼ ))
104	78, 103	erthi 8681	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [𝑣] ∼ = [(𝐹‘[𝑣] ∼ )] ∼ )
105	104	eqcomd 2735	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [(𝐹‘[𝑣] ∼ )] ∼ = [𝑣] ∼ )
106	105	fveq2d 6826	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝐹‘[(𝐹‘[𝑣] ∼ )] ∼ ) = (𝐹‘[𝑣] ∼ ))
107	36, 77, 106	ectocld 8709	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑆) → (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤))
108	107	ralrimiva 3121	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑤 ∈ 𝑆 (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤))
109		eceq1 8664	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝐹‘𝑤) → [𝑧] ∼ = [(𝐹‘𝑤)] ∼ )
110	109	fveq2d 6826	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑤) → (𝐹‘[𝑧] ∼ ) = (𝐹‘[(𝐹‘𝑤)] ∼ ))
111		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑤) → 𝑧 = (𝐹‘𝑤))
112	110, 111	eqeq12d 2745	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐹‘𝑤) → ((𝐹‘[𝑧] ∼ ) = 𝑧 ↔ (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤)))
113	112	ralrn 7022	. . . . . . . . . . . . 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 3578	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐹‘[(𝑤 − (𝐺‘𝑚))] ∼ ) = (𝑤 − (𝐺‘𝑚)))
118		eceq1 8664	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑘)) → [𝑧] ∼ = [(𝑤 − (𝐺‘𝑘))] ∼ )
119	118	fveq2d 6826	. . . . . . . . . . 11 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑘)) → (𝐹‘[𝑧] ∼ ) = (𝐹‘[(𝑤 − (𝐺‘𝑘))] ∼ ))
120		id 22	. . . . . . . . . . 11 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑘)) → 𝑧 = (𝑤 − (𝐺‘𝑘)))
121	119, 120	eqeq12d 2745	. . . . . . . . . 10 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑘)) → ((𝐹‘[𝑧] ∼ ) = 𝑧 ↔ (𝐹‘[(𝑤 − (𝐺‘𝑘))] ∼ ) = (𝑤 − (𝐺‘𝑘))))
122	121, 116, 58	rspcdva 3578	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐹‘[(𝑤 − (𝐺‘𝑘))] ∼ ) = (𝑤 − (𝐺‘𝑘)))
123	69, 117, 122	3eqtr3d 2772	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑚)) = (𝑤 − (𝐺‘𝑘)))
124	18, 28, 32, 123	subcand 11516	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑚) = (𝐺‘𝑘))
125	19	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)))
126		f1of1 6763	. . . . . . . . 9 ⊢ (𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) → 𝐺:ℕ–1-1→(ℚ ∩ (-1[,]1)))
127	125, 126	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝐺:ℕ–1-1→(ℚ ∩ (-1[,]1)))
128		f1fveq 7199	. . . . . . . 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 2811	. . . . . 6 ⊢ (𝑚 = 𝑘 → (𝑚 ∈ ℕ ↔ 𝑘 ∈ ℕ))
134		fveq2 6822	. . . . . . 7 ⊢ (𝑚 = 𝑘 → (𝑇‘𝑚) = (𝑇‘𝑘))
135	134	eleq2d 2814	. . . . . 6 ⊢ (𝑚 = 𝑘 → (𝑤 ∈ (𝑇‘𝑚) ↔ 𝑤 ∈ (𝑇‘𝑘)))
136	133, 135	anbi12d 632	. . . . 5 ⊢ (𝑚 = 𝑘 → ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ↔ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘))))
137	136	mo4 2559	. . . 4 ⊢ (∃*𝑚(𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ↔ ∀𝑚∀𝑘(((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘))) → 𝑚 = 𝑘))
138	132, 137	sylibr 234	. . 3 ⊢ (𝜑 → ∃*𝑚(𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)))
139	138	alrimiv 1927	. 2 ⊢ (𝜑 → ∀𝑤∃*𝑚(𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)))
140		dfdisj2 5061	. 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 2531 ≠ wne 2925 ∀wral 3044 {crab 3394 Vcvv 3436 ∖ cdif 3900 ∩ cin 3902 ⊆ wss 3903 ∅c0 4284 𝒫 cpw 4551 ∪ ciun 4941 Disj wdisj 5059 class class class wbr 5092 {copab 5154 ↦ cmpt 5173 dom cdm 5619 ran crn 5620 Fn wfn 6477 ⟶wf 6478 –1-1→wf1 6479 –1-1-onto→wf1o 6481 ‘cfv 6482 (class class class)co 7349 Er wer 8622 [cec 8623 / cqs 8624 ℂcc 11007 ℝcr 11008 0cc0 11009 1c1 11010 − cmin 11347 -cneg 11348 ℕcn 12128 2c2 12183 ℚcq 12849 [,]cicc 13251 volcvol 25362

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 2701 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086

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 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4859 df-iun 4943 df-disj 5060 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-om 7800 df-1st 7924 df-2nd 7925 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-er 8625 df-ec 8627 df-qs 8631 df-en 8873 df-dom 8874 df-sdom 8875 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-div 11778 df-nn 12129 df-2 12191 df-n0 12385 df-z 12472 df-q 12850 df-icc 13255

This theorem is referenced by: vitalilem4 25510

W3C validator