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 25931

Description: Lemma for vitali 25934. (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 792	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ (𝑇‘𝑚))
2		simprll 791	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑚 ∈ ℕ)
3		fveq2 6885	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → (𝐺‘𝑛) = (𝐺‘𝑚))
4	3	oveq2d 7436	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑚 → (𝑠 − (𝐺‘𝑛)) = (𝑠 − (𝐺‘𝑚)))
5	4	eleq1d 2845	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → ((𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹 ↔ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹))
6	5	rabbidv 3419	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑚 → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹} = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹})
7		vitali.6	. . . . . . . . . . . . . 14 ⊢ 𝑇 = (𝑛 ∈ ℕ ↦ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹})
8		reex 11291	. . . . . . . . . . . . . . 15 ⊢ ℝ ∈ V
9	8	rabex 5299	. . . . . . . . . . . . . 14 ⊢ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹} ∈ V
10	6, 7, 9	fvmpt 6993	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ → (𝑇‘𝑚) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹})
11	2, 10	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑇‘𝑚) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹})
12	1, 11	eleqtrd 2862	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹})
13		oveq1 7427	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑤 → (𝑠 − (𝐺‘𝑚)) = (𝑤 − (𝐺‘𝑚)))
14	13	eleq1d 2845	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑤 → ((𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹 ↔ (𝑤 − (𝐺‘𝑚)) ∈ ran 𝐹))
15	14	elrab 3644	. . . . . . . . . . 11 ⊢ (𝑤 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹} ↔ (𝑤 ∈ ℝ ∧ (𝑤 − (𝐺‘𝑚)) ∈ ran 𝐹))
16	12, 15	sylib 221	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 ∈ ℝ ∧ (𝑤 − (𝐺‘𝑚)) ∈ ran 𝐹))
17	16	simpld 500	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ ℝ)
18	17	recnd 11337	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ ℂ)
19		vitali.5	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺:ℕ–1-1-onto→(ℚ ∩ ( -1[,]1)))
20		f1of 6824	. . . . . . . . . . . . 13 ⊢ (𝐺:ℕ–1-1-onto→(ℚ ∩ ( -1[,]1)) → 𝐺:ℕ⟶(ℚ ∩ ( -1[,]1)))
21	19, 20	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:ℕ⟶(ℚ ∩ ( -1[,]1)))
22		inss1 4133	. . . . . . . . . . . 12 ⊢ (ℚ ∩ ( -1[,]1)) ⊆ ℚ
23		fss 6726	. . . . . . . . . . . 12 ⊢ ((𝐺:ℕ⟶(ℚ ∩ ( -1[,]1)) ∧ (ℚ ∩ ( -1[,]1)) ⊆ ℚ) → 𝐺:ℕ⟶ℚ)
24	21, 22, 23	sylancl 598	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺:ℕ⟶ℚ)
25	24	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝐺:ℕ⟶ℚ)
26	25, 2	ffvelcdmd 7085	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑚) ∈ ℚ)
27		qcn 13090	. . . . . . . . 9 ⊢ ((𝐺‘𝑚) ∈ ℚ → (𝐺‘𝑚) ∈ ℂ)
28	26, 27	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑚) ∈ ℂ)
29		simprrl 793	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑘 ∈ ℕ)
30	25, 29	ffvelcdmd 7085	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑘) ∈ ℚ)
31		qcn 13090	. . . . . . . . 9 ⊢ ((𝐺‘𝑘) ∈ ℚ → (𝐺‘𝑘) ∈ ℂ)
32	30, 31	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑘) ∈ ℂ)
33		vitali.1	. . . . . . . . . . . . 13 ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)}
34	33	vitalilem1 25929	. . . . . . . . . . . 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 25930	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ran 𝐹 ⊆ (0[,]1) ∧ (0[,]1) ⊆ ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∧ ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ ( -1[,]2)))
41	40	simp1d 1160	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran 𝐹 ⊆ (0[,]1))
42	41	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ran 𝐹 ⊆ (0[,]1))
43	16	simprd 501	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑚)) ∈ ran 𝐹)
44	42, 43	sseldd 3909	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑚)) ∈ (0[,]1))
45		simprrr 794	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ (𝑇‘𝑘))
46		fveq2 6885	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘))
47	46	oveq2d 7436	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑘 → (𝑠 − (𝐺‘𝑛)) = (𝑠 − (𝐺‘𝑘)))
48	47	eleq1d 2845	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → ((𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹 ↔ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹))
49	48	rabbidv 3419	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹} = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹})
50	8	rabex 5299	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹} ∈ V
51	49, 7, 50	fvmpt 6993	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ → (𝑇‘𝑘) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹})
52	29, 51	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑇‘𝑘) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹})
53	45, 52	eleqtrd 2862	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹})
54		oveq1 7427	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = 𝑤 → (𝑠 − (𝐺‘𝑘)) = (𝑤 − (𝐺‘𝑘)))
55	54	eleq1d 2845	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = 𝑤 → ((𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹 ↔ (𝑤 − (𝐺‘𝑘)) ∈ ran 𝐹))
56	55	elrab 3644	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹} ↔ (𝑤 ∈ ℝ ∧ (𝑤 − (𝐺‘𝑘)) ∈ ran 𝐹))
57	53, 56	sylib 221	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 ∈ ℝ ∧ (𝑤 − (𝐺‘𝑘)) ∈ ran 𝐹))
58	57	simprd 501	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑘)) ∈ ran 𝐹)
59	42, 58	sseldd 3909	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑘)) ∈ (0[,]1))
60	18, 28, 32	nnncan1d 11703	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘))) = ((𝐺‘𝑘) − (𝐺‘𝑚)))
61		qsubcl 13096	. . . . . . . . . . . . . 14 ⊢ (((𝐺‘𝑘) ∈ ℚ ∧ (𝐺‘𝑚) ∈ ℚ) → ((𝐺‘𝑘) − (𝐺‘𝑚)) ∈ ℚ)
62	30, 26, 61	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ((𝐺‘𝑘) − (𝐺‘𝑚)) ∈ ℚ)
63	60, 62	eqeltrd 2860	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘))) ∈ ℚ)
64		oveq12 7429	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = (𝑤 − (𝐺‘𝑚)) ∧ 𝑦 = (𝑤 − (𝐺‘𝑘))) → (𝑥 − 𝑦) = ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘))))
65	64	eleq1d 2845	. . . . . . . . . . . . 13 ⊢ ((𝑥 = (𝑤 − (𝐺‘𝑚)) ∧ 𝑦 = (𝑤 − (𝐺‘𝑘))) → ((𝑥 − 𝑦) ∈ ℚ ↔ ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘))) ∈ ℚ))
66	65, 33	brab2a 5743	. . . . . . . . . . . 12 ⊢ ((𝑤 − (𝐺‘𝑚)) ∼ (𝑤 − (𝐺‘𝑘)) ↔ (((𝑤 − (𝐺‘𝑚)) ∈ (0[,]1) ∧ (𝑤 − (𝐺‘𝑘)) ∈ (0[,]1)) ∧ ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘))) ∈ ℚ))
67	44, 59, 63, 66	syl21anbrc 1363	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑚)) ∼ (𝑤 − (𝐺‘𝑘)))
68	35, 67	erthi 8774	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → [(𝑤 − (𝐺‘𝑚))] ∼ = [(𝑤 − (𝐺‘𝑘))] ∼ )
69	68	fveq2d 6889	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐹‘[(𝑤 − (𝐺‘𝑚))] ∼ ) = (𝐹‘[(𝑤 − (𝐺‘𝑘))] ∼ ))
70		eceq1 8757	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑚)) → [𝑧] ∼ = [(𝑤 − (𝐺‘𝑚))] ∼ )
71	70	fveq2d 6889	. . . . . . . . . . 11 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑚)) → (𝐹‘[𝑧] ∼ ) = (𝐹‘[(𝑤 − (𝐺‘𝑚))] ∼ ))
72		id 23	. . . . . . . . . . 11 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑚)) → 𝑧 = (𝑤 − (𝐺‘𝑚)))
73	71, 72	eqeq12d 2776	. . . . . . . . . 10 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑚)) → ((𝐹‘[𝑧] ∼ ) = 𝑧 ↔ (𝐹‘[(𝑤 − (𝐺‘𝑚))] ∼ ) = (𝑤 − (𝐺‘𝑚))))
74		fveq2 6885	. . . . . . . . . . . . . . . . 17 ⊢ ([𝑣] ∼ = 𝑤 → (𝐹‘[𝑣] ∼ ) = (𝐹‘𝑤))
75	74	eceq1d 8758	. . . . . . . . . . . . . . . 16 ⊢ ([𝑣] ∼ = 𝑤 → [(𝐹‘[𝑣] ∼ )] ∼ = [(𝐹‘𝑤)] ∼ )
76	75	fveq2d 6889	. . . . . . . . . . . . . . 15 ⊢ ([𝑣] ∼ = 𝑤 → (𝐹‘[(𝐹‘[𝑣] ∼ )] ∼ ) = (𝐹‘[(𝐹‘𝑤)] ∼ ))
77	76, 74	eqeq12d 2776	. . . . . . . . . . . . . 14 ⊢ ([𝑣] ∼ = 𝑤 → ((𝐹‘[(𝐹‘[𝑣] ∼ )] ∼ ) = (𝐹‘[𝑣] ∼ ) ↔ (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤)))
78	34	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ∼ Er (0[,]1))
79		erdm 8728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ( ∼ Er (0[,]1) → dom ∼ = (0[,]1))
80	34, 79	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ dom ∼ = (0[,]1)
81	80	eleq2i 2852	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ dom ∼ ↔ 𝑣 ∈ (0[,]1))
82		ecdmn0 8770	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ dom ∼ ↔ [𝑣] ∼ ≠ ∅)
83	81, 82	bitr3i 280	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ (0[,]1) ↔ [𝑣] ∼ ≠ ∅)
84	83	bilani 510	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [𝑣] ∼ ≠ ∅)
85		neeq1 3017	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = [𝑣] ∼ → (𝑧 ≠ ∅ ↔ [𝑣] ∼ ≠ ∅))
86		fveq2 6885	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = [𝑣] ∼ → (𝐹‘𝑧) = (𝐹‘[𝑣] ∼ ))
87		id 23	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = [𝑣] ∼ → 𝑧 = [𝑣] ∼ )
88	86, 87	eleq12d 2854	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = [𝑣] ∼ → ((𝐹‘𝑧) ∈ 𝑧 ↔ (𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ ))
89	85, 88	imbi12d 347	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = [𝑣] ∼ → ((𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧) ↔ ([𝑣] ∼ ≠ ∅ → (𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ )))
90	38	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧))
91		ovex 7453	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0[,]1) ∈ V
92		erex 8742	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ( ∼ Er (0[,]1) → ((0[,]1) ∈ V → ∼ ∈ V))
93	34, 91, 92	mp2 9	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∼ ∈ V
94	93	ecelqsi 8790	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ (0[,]1) → [𝑣] ∼ ∈ ((0[,]1) / ∼ ))
95	94, 36	eleqtrrdi 2871	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ (0[,]1) → [𝑣] ∼ ∈ 𝑆)
96	95	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [𝑣] ∼ ∈ 𝑆)
97	89, 90, 96	rspcdva 3577	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ([𝑣] ∼ ≠ ∅ → (𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ ))
98	84, 97	mpd 16	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ )
99		fvex 6898	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹‘[𝑣] ∼ ) ∈ V
100		vex 3454	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑣 ∈ V
101	99, 100	elec 8764	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ ↔ 𝑣 ∼ (𝐹‘[𝑣] ∼ ))
102	98, 101	sylib 221	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝑣 ∼ (𝐹‘[𝑣] ∼ ))
103	78, 102	erthi 8774	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [𝑣] ∼ = [(𝐹‘[𝑣] ∼ )] ∼ )
104	103	eqcomd 2766	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [(𝐹‘[𝑣] ∼ )] ∼ = [𝑣] ∼ )
105	104	fveq2d 6889	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝐹‘[(𝐹‘[𝑣] ∼ )] ∼ ) = (𝐹‘[𝑣] ∼ ))
106	36, 77, 105	ectocld 8803	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑆) → (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤))
107	106	ralrimiva 3154	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑤 ∈ 𝑆 (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤))
108		eceq1 8757	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝐹‘𝑤) → [𝑧] ∼ = [(𝐹‘𝑤)] ∼ )
109	108	fveq2d 6889	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑤) → (𝐹‘[𝑧] ∼ ) = (𝐹‘[(𝐹‘𝑤)] ∼ ))
110		id 23	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑤) → 𝑧 = (𝐹‘𝑤))
111	109, 110	eqeq12d 2776	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐹‘𝑤) → ((𝐹‘[𝑧] ∼ ) = 𝑧 ↔ (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤)))
112	111	ralrn 7088	. . . . . . . . . . . . 13 ⊢ (𝐹 Fn 𝑆 → (∀𝑧 ∈ ran 𝐹(𝐹‘[𝑧] ∼ ) = 𝑧 ↔ ∀𝑤 ∈ 𝑆 (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤)))
113	37, 112	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (∀𝑧 ∈ ran 𝐹(𝐹‘[𝑧] ∼ ) = 𝑧 ↔ ∀𝑤 ∈ 𝑆 (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤)))
114	107, 113	mpbird 260	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑧 ∈ ran 𝐹(𝐹‘[𝑧] ∼ ) = 𝑧)
115	114	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ∀𝑧 ∈ ran 𝐹(𝐹‘[𝑧] ∼ ) = 𝑧)
116	73, 115, 43	rspcdva 3577	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐹‘[(𝑤 − (𝐺‘𝑚))] ∼ ) = (𝑤 − (𝐺‘𝑚)))
117		eceq1 8757	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑘)) → [𝑧] ∼ = [(𝑤 − (𝐺‘𝑘))] ∼ )
118	117	fveq2d 6889	. . . . . . . . . . 11 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑘)) → (𝐹‘[𝑧] ∼ ) = (𝐹‘[(𝑤 − (𝐺‘𝑘))] ∼ ))
119		id 23	. . . . . . . . . . 11 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑘)) → 𝑧 = (𝑤 − (𝐺‘𝑘)))
120	118, 119	eqeq12d 2776	. . . . . . . . . 10 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑘)) → ((𝐹‘[𝑧] ∼ ) = 𝑧 ↔ (𝐹‘[(𝑤 − (𝐺‘𝑘))] ∼ ) = (𝑤 − (𝐺‘𝑘))))
121	120, 115, 58	rspcdva 3577	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐹‘[(𝑤 − (𝐺‘𝑘))] ∼ ) = (𝑤 − (𝐺‘𝑘)))
122	69, 116, 121	3eqtr3d 2803	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑚)) = (𝑤 − (𝐺‘𝑘)))
123	18, 28, 32, 122	subcand 11710	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑚) = (𝐺‘𝑘))
124	19	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝐺:ℕ–1-1-onto→(ℚ ∩ ( -1[,]1)))
125		f1of1 6823	. . . . . . . . 9 ⊢ (𝐺:ℕ–1-1-onto→(ℚ ∩ ( -1[,]1)) → 𝐺:ℕ–1-1→(ℚ ∩ ( -1[,]1)))
126	124, 125	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝐺:ℕ–1-1→(ℚ ∩ ( -1[,]1)))
127		f1fveq 7266	. . . . . . . 8 ⊢ ((𝐺:ℕ–1-1→(ℚ ∩ ( -1[,]1)) ∧ (𝑚 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐺‘𝑚) = (𝐺‘𝑘) ↔ 𝑚 = 𝑘))
128	126, 2, 29, 127	syl12anc 850	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ((𝐺‘𝑚) = (𝐺‘𝑘) ↔ 𝑚 = 𝑘))
129	123, 128	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑚 = 𝑘)
130	129	ex 418	. . . . 5 ⊢ (𝜑 → (((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘))) → 𝑚 = 𝑘))
131	130	alrimivv 1960	. . . 4 ⊢ (𝜑 → ∀𝑚∀𝑘(((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘))) → 𝑚 = 𝑘))
132		eleq1w 2843	. . . . . 6 ⊢ (𝑚 = 𝑘 → (𝑚 ∈ ℕ ↔ 𝑘 ∈ ℕ))
133		fveq2 6885	. . . . . . 7 ⊢ (𝑚 = 𝑘 → (𝑇‘𝑚) = (𝑇‘𝑘))
134	133	eleq2d 2846	. . . . . 6 ⊢ (𝑚 = 𝑘 → (𝑤 ∈ (𝑇‘𝑚) ↔ 𝑤 ∈ (𝑇‘𝑘)))
135	132, 134	anbi12d 644	. . . . 5 ⊢ (𝑚 = 𝑘 → ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ↔ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘))))
136	135	mo4 2591	. . . 4 ⊢ (∃*𝑚(𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ↔ ∀𝑚∀𝑘(((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘))) → 𝑚 = 𝑘))
137	131, 136	sylibr 237	. . 3 ⊢ (𝜑 → ∃*𝑚(𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)))
138	137	alrimiv 1959	. 2 ⊢ (𝜑 → ∀𝑤∃*𝑚(𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)))
139		dfdisj2 5071	. 2 ⊢ (Disj 𝑚 ∈ ℕ (𝑇‘𝑚) ↔ ∀𝑤∃*𝑚(𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)))
140	138, 139	sylibr 237	1 ⊢ (𝜑 → Disj 𝑚 ∈ ℕ (𝑇‘𝑚))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∀wal 1567 = wceq 1569 ∈ wcel 2144 ∃*wmo 2562 ≠ wne 2955 ∀wral 3076 {crab 3412 Vcvv 3450 ⊆ wss 3895 ∖ cdif 4045 ∩ cin 4089 ∅c0 4278 𝒫 cpw 4556 ∪ ciun 4950 Disj wdisj 5069 class class class wbr 5102 {copab 5166 ↦ cmpt 5185 dom cdm 5650 ran crn 5651 Fn wfn 6533 ⟶wf 6534 –1-1→wf1 6535 –1-1-onto→wf1o 6537 ‘cfv 6538 (class class class)co 7420 Er wer 8714 [cec 8715 / cqs 8716 ℂcc 11198 ℝcr 11199 0cc0 11200 1c1 11201 − cmin 11541 -cneg 11542 ℕcn 12335 2c2 12397 ℚcq 13075 [,]cicc 13479 volcvol 25784

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-iun 4952 df-disj 5070 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-er 8717 df-ec 8719 df-qs 8723 df-en 8974 df-dom 8975 df-sdom 8976 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-div 11974 df-nn 12336 df-2 12405 df-n0 12607 df-z 12694 df-q 13076 df-icc 13483

This theorem is used by: vitalilem4 25932

W3C validator