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 24211

Description: Lemma for vitali 24214. (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 778	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ (𝑇‘𝑚))
2		simprll 777	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑚 ∈ ℕ)
3		fveq2 6670	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → (𝐺‘𝑛) = (𝐺‘𝑚))
4	3	oveq2d 7172	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑚 → (𝑠 − (𝐺‘𝑛)) = (𝑠 − (𝐺‘𝑚)))
5	4	eleq1d 2897	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → ((𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹 ↔ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹))
6	5	rabbidv 3480	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑚 → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹} = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹})
7		vitali.6	. . . . . . . . . . . . . 14 ⊢ 𝑇 = (𝑛 ∈ ℕ ↦ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹})
8		reex 10628	. . . . . . . . . . . . . . 15 ⊢ ℝ ∈ V
9	8	rabex 5235	. . . . . . . . . . . . . 14 ⊢ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹} ∈ V
10	6, 7, 9	fvmpt 6768	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ → (𝑇‘𝑚) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹})
11	2, 10	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑇‘𝑚) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹})
12	1, 11	eleqtrd 2915	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹})
13		oveq1 7163	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑤 → (𝑠 − (𝐺‘𝑚)) = (𝑤 − (𝐺‘𝑚)))
14	13	eleq1d 2897	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑤 → ((𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹 ↔ (𝑤 − (𝐺‘𝑚)) ∈ ran 𝐹))
15	14	elrab 3680	. . . . . . . . . . 11 ⊢ (𝑤 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹} ↔ (𝑤 ∈ ℝ ∧ (𝑤 − (𝐺‘𝑚)) ∈ ran 𝐹))
16	12, 15	sylib 220	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 ∈ ℝ ∧ (𝑤 − (𝐺‘𝑚)) ∈ ran 𝐹))
17	16	simpld 497	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ ℝ)
18	17	recnd 10669	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ ℂ)
19		vitali.5	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)))
20		f1of 6615	. . . . . . . . . . . . 13 ⊢ (𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) → 𝐺:ℕ⟶(ℚ ∩ (-1[,]1)))
21	19, 20	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:ℕ⟶(ℚ ∩ (-1[,]1)))
22		inss1 4205	. . . . . . . . . . . 12 ⊢ (ℚ ∩ (-1[,]1)) ⊆ ℚ
23		fss 6527	. . . . . . . . . . . 12 ⊢ ((𝐺:ℕ⟶(ℚ ∩ (-1[,]1)) ∧ (ℚ ∩ (-1[,]1)) ⊆ ℚ) → 𝐺:ℕ⟶ℚ)
24	21, 22, 23	sylancl 588	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺:ℕ⟶ℚ)
25	24	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝐺:ℕ⟶ℚ)
26	25, 2	ffvelrnd 6852	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑚) ∈ ℚ)
27		qcn 12363	. . . . . . . . 9 ⊢ ((𝐺‘𝑚) ∈ ℚ → (𝐺‘𝑚) ∈ ℂ)
28	26, 27	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑚) ∈ ℂ)
29		simprrl 779	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑘 ∈ ℕ)
30	25, 29	ffvelrnd 6852	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑘) ∈ ℚ)
31		qcn 12363	. . . . . . . . 9 ⊢ ((𝐺‘𝑘) ∈ ℚ → (𝐺‘𝑘) ∈ ℂ)
32	30, 31	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑘) ∈ ℂ)
33		vitali.1	. . . . . . . . . . . . 13 ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)}
34	33	vitalilem1 24209	. . . . . . . . . . . 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 24210	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ran 𝐹 ⊆ (0[,]1) ∧ (0[,]1) ⊆ ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∧ ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ (-1[,]2)))
41	40	simp1d 1138	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran 𝐹 ⊆ (0[,]1))
42	41	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ran 𝐹 ⊆ (0[,]1))
43	16	simprd 498	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑚)) ∈ ran 𝐹)
44	42, 43	sseldd 3968	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑚)) ∈ (0[,]1))
45		simprrr 780	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ (𝑇‘𝑘))
46		fveq2 6670	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘))
47	46	oveq2d 7172	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑘 → (𝑠 − (𝐺‘𝑛)) = (𝑠 − (𝐺‘𝑘)))
48	47	eleq1d 2897	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → ((𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹 ↔ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹))
49	48	rabbidv 3480	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹} = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹})
50	8	rabex 5235	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹} ∈ V
51	49, 7, 50	fvmpt 6768	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ → (𝑇‘𝑘) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹})
52	29, 51	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑇‘𝑘) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹})
53	45, 52	eleqtrd 2915	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹})
54		oveq1 7163	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = 𝑤 → (𝑠 − (𝐺‘𝑘)) = (𝑤 − (𝐺‘𝑘)))
55	54	eleq1d 2897	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = 𝑤 → ((𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹 ↔ (𝑤 − (𝐺‘𝑘)) ∈ ran 𝐹))
56	55	elrab 3680	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹} ↔ (𝑤 ∈ ℝ ∧ (𝑤 − (𝐺‘𝑘)) ∈ ran 𝐹))
57	53, 56	sylib 220	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 ∈ ℝ ∧ (𝑤 − (𝐺‘𝑘)) ∈ ran 𝐹))
58	57	simprd 498	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑘)) ∈ ran 𝐹)
59	42, 58	sseldd 3968	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑘)) ∈ (0[,]1))
60	18, 28, 32	nnncan1d 11031	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘))) = ((𝐺‘𝑘) − (𝐺‘𝑚)))
61		qsubcl 12368	. . . . . . . . . . . . . 14 ⊢ (((𝐺‘𝑘) ∈ ℚ ∧ (𝐺‘𝑚) ∈ ℚ) → ((𝐺‘𝑘) − (𝐺‘𝑚)) ∈ ℚ)
62	30, 26, 61	syl2anc 586	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ((𝐺‘𝑘) − (𝐺‘𝑚)) ∈ ℚ)
63	60, 62	eqeltrd 2913	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘))) ∈ ℚ)
64		oveq12 7165	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = (𝑤 − (𝐺‘𝑚)) ∧ 𝑦 = (𝑤 − (𝐺‘𝑘))) → (𝑥 − 𝑦) = ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘))))
65	64	eleq1d 2897	. . . . . . . . . . . . 13 ⊢ ((𝑥 = (𝑤 − (𝐺‘𝑚)) ∧ 𝑦 = (𝑤 − (𝐺‘𝑘))) → ((𝑥 − 𝑦) ∈ ℚ ↔ ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘))) ∈ ℚ))
66	65, 33	brab2a 5644	. . . . . . . . . . . 12 ⊢ ((𝑤 − (𝐺‘𝑚)) ∼ (𝑤 − (𝐺‘𝑘)) ↔ (((𝑤 − (𝐺‘𝑚)) ∈ (0[,]1) ∧ (𝑤 − (𝐺‘𝑘)) ∈ (0[,]1)) ∧ ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘))) ∈ ℚ))
67	44, 59, 63, 66	syl21anbrc 1340	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑚)) ∼ (𝑤 − (𝐺‘𝑘)))
68	35, 67	erthi 8340	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → [(𝑤 − (𝐺‘𝑚))] ∼ = [(𝑤 − (𝐺‘𝑘))] ∼ )
69	68	fveq2d 6674	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐹‘[(𝑤 − (𝐺‘𝑚))] ∼ ) = (𝐹‘[(𝑤 − (𝐺‘𝑘))] ∼ ))
70		eceq1 8327	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑚)) → [𝑧] ∼ = [(𝑤 − (𝐺‘𝑚))] ∼ )
71	70	fveq2d 6674	. . . . . . . . . . 11 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑚)) → (𝐹‘[𝑧] ∼ ) = (𝐹‘[(𝑤 − (𝐺‘𝑚))] ∼ ))
72		id 22	. . . . . . . . . . 11 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑚)) → 𝑧 = (𝑤 − (𝐺‘𝑚)))
73	71, 72	eqeq12d 2837	. . . . . . . . . 10 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑚)) → ((𝐹‘[𝑧] ∼ ) = 𝑧 ↔ (𝐹‘[(𝑤 − (𝐺‘𝑚))] ∼ ) = (𝑤 − (𝐺‘𝑚))))
74		fveq2 6670	. . . . . . . . . . . . . . . . 17 ⊢ ([𝑣] ∼ = 𝑤 → (𝐹‘[𝑣] ∼ ) = (𝐹‘𝑤))
75	74	eceq1d 8328	. . . . . . . . . . . . . . . 16 ⊢ ([𝑣] ∼ = 𝑤 → [(𝐹‘[𝑣] ∼ )] ∼ = [(𝐹‘𝑤)] ∼ )
76	75	fveq2d 6674	. . . . . . . . . . . . . . 15 ⊢ ([𝑣] ∼ = 𝑤 → (𝐹‘[(𝐹‘[𝑣] ∼ )] ∼ ) = (𝐹‘[(𝐹‘𝑤)] ∼ ))
77	76, 74	eqeq12d 2837	. . . . . . . . . . . . . 14 ⊢ ([𝑣] ∼ = 𝑤 → ((𝐹‘[(𝐹‘[𝑣] ∼ )] ∼ ) = (𝐹‘[𝑣] ∼ ) ↔ (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤)))
78	34	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ∼ Er (0[,]1))
79		simpr 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝑣 ∈ (0[,]1))
80		erdm 8299	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ( ∼ Er (0[,]1) → dom ∼ = (0[,]1))
81	34, 80	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ dom ∼ = (0[,]1)
82	81	eleq2i 2904	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ dom ∼ ↔ 𝑣 ∈ (0[,]1))
83		ecdmn0 8336	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ dom ∼ ↔ [𝑣] ∼ ≠ ∅)
84	82, 83	bitr3i 279	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ (0[,]1) ↔ [𝑣] ∼ ≠ ∅)
85	79, 84	sylib 220	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [𝑣] ∼ ≠ ∅)
86		neeq1 3078	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = [𝑣] ∼ → (𝑧 ≠ ∅ ↔ [𝑣] ∼ ≠ ∅))
87		fveq2 6670	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = [𝑣] ∼ → (𝐹‘𝑧) = (𝐹‘[𝑣] ∼ ))
88		id 22	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = [𝑣] ∼ → 𝑧 = [𝑣] ∼ )
89	87, 88	eleq12d 2907	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = [𝑣] ∼ → ((𝐹‘𝑧) ∈ 𝑧 ↔ (𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ ))
90	86, 89	imbi12d 347	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = [𝑣] ∼ → ((𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧) ↔ ([𝑣] ∼ ≠ ∅ → (𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ )))
91	38	adantr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧))
92		ovex 7189	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0[,]1) ∈ V
93		erex 8313	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ( ∼ Er (0[,]1) → ((0[,]1) ∈ V → ∼ ∈ V))
94	34, 92, 93	mp2 9	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∼ ∈ V
95	94	ecelqsi 8353	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ (0[,]1) → [𝑣] ∼ ∈ ((0[,]1) / ∼ ))
96	95, 36	eleqtrrdi 2924	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ (0[,]1) → [𝑣] ∼ ∈ 𝑆)
97	96	adantl 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [𝑣] ∼ ∈ 𝑆)
98	90, 91, 97	rspcdva 3625	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ([𝑣] ∼ ≠ ∅ → (𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ ))
99	85, 98	mpd 15	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ )
100		fvex 6683	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹‘[𝑣] ∼ ) ∈ V
101		vex 3497	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑣 ∈ V
102	100, 101	elec 8333	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ ↔ 𝑣 ∼ (𝐹‘[𝑣] ∼ ))
103	99, 102	sylib 220	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝑣 ∼ (𝐹‘[𝑣] ∼ ))
104	78, 103	erthi 8340	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [𝑣] ∼ = [(𝐹‘[𝑣] ∼ )] ∼ )
105	104	eqcomd 2827	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [(𝐹‘[𝑣] ∼ )] ∼ = [𝑣] ∼ )
106	105	fveq2d 6674	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝐹‘[(𝐹‘[𝑣] ∼ )] ∼ ) = (𝐹‘[𝑣] ∼ ))
107	36, 77, 106	ectocld 8364	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑆) → (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤))
108	107	ralrimiva 3182	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑤 ∈ 𝑆 (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤))
109		eceq1 8327	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝐹‘𝑤) → [𝑧] ∼ = [(𝐹‘𝑤)] ∼ )
110	109	fveq2d 6674	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑤) → (𝐹‘[𝑧] ∼ ) = (𝐹‘[(𝐹‘𝑤)] ∼ ))
111		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑤) → 𝑧 = (𝐹‘𝑤))
112	110, 111	eqeq12d 2837	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐹‘𝑤) → ((𝐹‘[𝑧] ∼ ) = 𝑧 ↔ (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤)))
113	112	ralrn 6854	. . . . . . . . . . . . 13 ⊢ (𝐹 Fn 𝑆 → (∀𝑧 ∈ ran 𝐹(𝐹‘[𝑧] ∼ ) = 𝑧 ↔ ∀𝑤 ∈ 𝑆 (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤)))
114	37, 113	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (∀𝑧 ∈ ran 𝐹(𝐹‘[𝑧] ∼ ) = 𝑧 ↔ ∀𝑤 ∈ 𝑆 (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤)))
115	108, 114	mpbird 259	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑧 ∈ ran 𝐹(𝐹‘[𝑧] ∼ ) = 𝑧)
116	115	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ∀𝑧 ∈ ran 𝐹(𝐹‘[𝑧] ∼ ) = 𝑧)
117	73, 116, 43	rspcdva 3625	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐹‘[(𝑤 − (𝐺‘𝑚))] ∼ ) = (𝑤 − (𝐺‘𝑚)))
118		eceq1 8327	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑘)) → [𝑧] ∼ = [(𝑤 − (𝐺‘𝑘))] ∼ )
119	118	fveq2d 6674	. . . . . . . . . . 11 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑘)) → (𝐹‘[𝑧] ∼ ) = (𝐹‘[(𝑤 − (𝐺‘𝑘))] ∼ ))
120		id 22	. . . . . . . . . . 11 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑘)) → 𝑧 = (𝑤 − (𝐺‘𝑘)))
121	119, 120	eqeq12d 2837	. . . . . . . . . 10 ⊢ (𝑧 = (𝑤 − (𝐺‘𝑘)) → ((𝐹‘[𝑧] ∼ ) = 𝑧 ↔ (𝐹‘[(𝑤 − (𝐺‘𝑘))] ∼ ) = (𝑤 − (𝐺‘𝑘))))
122	121, 116, 58	rspcdva 3625	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐹‘[(𝑤 − (𝐺‘𝑘))] ∼ ) = (𝑤 − (𝐺‘𝑘)))
123	69, 117, 122	3eqtr3d 2864	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑚)) = (𝑤 − (𝐺‘𝑘)))
124	18, 28, 32, 123	subcand 11038	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑚) = (𝐺‘𝑘))
125	19	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)))
126		f1of1 6614	. . . . . . . . 9 ⊢ (𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) → 𝐺:ℕ–1-1→(ℚ ∩ (-1[,]1)))
127	125, 126	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝐺:ℕ–1-1→(ℚ ∩ (-1[,]1)))
128		f1fveq 7020	. . . . . . . 8 ⊢ ((𝐺:ℕ–1-1→(ℚ ∩ (-1[,]1)) ∧ (𝑚 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐺‘𝑚) = (𝐺‘𝑘) ↔ 𝑚 = 𝑘))
129	127, 2, 29, 128	syl12anc 834	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ((𝐺‘𝑚) = (𝐺‘𝑘) ↔ 𝑚 = 𝑘))
130	124, 129	mpbid 234	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑚 = 𝑘)
131	130	ex 415	. . . . 5 ⊢ (𝜑 → (((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘))) → 𝑚 = 𝑘))
132	131	alrimivv 1929	. . . 4 ⊢ (𝜑 → ∀𝑚∀𝑘(((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘))) → 𝑚 = 𝑘))
133		eleq1w 2895	. . . . . 6 ⊢ (𝑚 = 𝑘 → (𝑚 ∈ ℕ ↔ 𝑘 ∈ ℕ))
134		fveq2 6670	. . . . . . 7 ⊢ (𝑚 = 𝑘 → (𝑇‘𝑚) = (𝑇‘𝑘))
135	134	eleq2d 2898	. . . . . 6 ⊢ (𝑚 = 𝑘 → (𝑤 ∈ (𝑇‘𝑚) ↔ 𝑤 ∈ (𝑇‘𝑘)))
136	133, 135	anbi12d 632	. . . . 5 ⊢ (𝑚 = 𝑘 → ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ↔ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘))))
137	136	mo4 2650	. . . 4 ⊢ (∃*𝑚(𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ↔ ∀𝑚∀𝑘(((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘))) → 𝑚 = 𝑘))
138	132, 137	sylibr 236	. . 3 ⊢ (𝜑 → ∃*𝑚(𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)))
139	138	alrimiv 1928	. 2 ⊢ (𝜑 → ∀𝑤∃*𝑚(𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)))
140		dfdisj2 5033	. 2 ⊢ (Disj 𝑚 ∈ ℕ (𝑇‘𝑚) ↔ ∀𝑤∃*𝑚(𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)))
141	139, 140	sylibr 236	1 ⊢ (𝜑 → Disj 𝑚 ∈ ℕ (𝑇‘𝑚))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∀wal 1535 = wceq 1537 ∈ wcel 2114 ∃*wmo 2620 ≠ wne 3016 ∀wral 3138 {crab 3142 Vcvv 3494 ∖ cdif 3933 ∩ cin 3935 ⊆ wss 3936 ∅c0 4291 𝒫 cpw 4539 ∪ ciun 4919 Disj wdisj 5031 class class class wbr 5066 {copab 5128 ↦ cmpt 5146 dom cdm 5555 ran crn 5556 Fn wfn 6350 ⟶wf 6351 –1-1→wf1 6352 –1-1-onto→wf1o 6354 ‘cfv 6355 (class class class)co 7156 Er wer 8286 [cec 8287 / cqs 8288 ℂcc 10535 ℝcr 10536 0cc0 10537 1c1 10538 − cmin 10870 -cneg 10871 ℕcn 11638 2c2 11693 ℚcq 12349 [,]cicc 12742 volcvol 24064

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 ax-cnex 10593 ax-resscn 10594 ax-1cn 10595 ax-icn 10596 ax-addcl 10597 ax-addrcl 10598 ax-mulcl 10599 ax-mulrcl 10600 ax-mulcom 10601 ax-addass 10602 ax-mulass 10603 ax-distr 10604 ax-i2m1 10605 ax-1ne0 10606 ax-1rid 10607 ax-rnegex 10608 ax-rrecex 10609 ax-cnre 10610 ax-pre-lttri 10611 ax-pre-lttrn 10612 ax-pre-ltadd 10613 ax-pre-mulgt0 10614

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-iun 4921 df-disj 5032 df-br 5067 df-opab 5129 df-mpt 5147 df-tr 5173 df-id 5460 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-we 5516 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-pred 6148 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-om 7581 df-1st 7689 df-2nd 7690 df-wrecs 7947 df-recs 8008 df-rdg 8046 df-er 8289 df-ec 8291 df-qs 8295 df-en 8510 df-dom 8511 df-sdom 8512 df-pnf 10677 df-mnf 10678 df-xr 10679 df-ltxr 10680 df-le 10681 df-sub 10872 df-neg 10873 df-div 11298 df-nn 11639 df-2 11701 df-n0 11899 df-z 11983 df-q 12350 df-icc 12746

This theorem is referenced by: vitalilem4 24212

W3C validator