Metamath Proof Explorer

Theorem vitalilem3

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

Ref Expression
Hypotheses 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 vitalilem3 ( 𝜑 → Disj 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) )

Proof

Step Hyp Ref Expression
1 vitali.1 ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑥 − 𝑦 ) ∈ ℚ ) }
2 vitali.2 ⊢ 𝑆 = ( ( 0 [,] 1 ) / ∼ )
3 vitali.3 ⊢ ( 𝜑 → 𝐹 Fn 𝑆 )
4 vitali.4 ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑆 ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) )
5 vitali.5 ⊢ ( 𝜑 → 𝐺 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) ) )
6 vitali.6 ⊢ 𝑇 = ( 𝑛 ∈ ℕ ↦ { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑛 ) ) ∈ ran 𝐹 } )
7 vitali.7 ⊢ ( 𝜑 → ¬ ran 𝐹 ∈ ( 𝒫 ℝ ∖ dom vol ) )
8 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) )
9 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → 𝑚 ∈ ℕ )
10 fveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑚 ) )
11 10 oveq2d ⊢ ( 𝑛 = 𝑚 → ( 𝑠 − ( 𝐺 ‘ 𝑛 ) ) = ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) )
12 11 eleq1d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑠 − ( 𝐺 ‘ 𝑛 ) ) ∈ ran 𝐹 ↔ ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 ) )
13 12 rabbidv ⊢ ( 𝑛 = 𝑚 → { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑛 ) ) ∈ ran 𝐹 } = { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 } )
14 reex ⊢ ℝ ∈ V
15 14 rabex ⊢ { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 } ∈ V
16 13 6 15 fvmpt ⊢ ( 𝑚 ∈ ℕ → ( 𝑇 ‘ 𝑚 ) = { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 } )
17 9 16 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( 𝑇 ‘ 𝑚 ) = { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 } )
18 8 17 eleqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → 𝑤 ∈ { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 } )
19 oveq1 ⊢ ( 𝑠 = 𝑤 → ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) = ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) )
20 19 eleq1d ⊢ ( 𝑠 = 𝑤 → ( ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 ↔ ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 ) )
21 20 elrab ⊢ ( 𝑤 ∈ { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 } ↔ ( 𝑤 ∈ ℝ ∧ ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 ) )
22 18 21 sylib ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( 𝑤 ∈ ℝ ∧ ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 ) )
23 22 simpld ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → 𝑤 ∈ ℝ )
24 23 recnd ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → 𝑤 ∈ ℂ )
25 f1of ⊢ ( 𝐺 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) ) → 𝐺 : ℕ ⟶ ( ℚ ∩ ( - 1 [,] 1 ) ) )
26 5 25 syl ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ℚ ∩ ( - 1 [,] 1 ) ) )
27 inss1 ⊢ ( ℚ ∩ ( - 1 [,] 1 ) ) ⊆ ℚ
28 fss ⊢ ( ( 𝐺 : ℕ ⟶ ( ℚ ∩ ( - 1 [,] 1 ) ) ∧ ( ℚ ∩ ( - 1 [,] 1 ) ) ⊆ ℚ ) → 𝐺 : ℕ ⟶ ℚ )
29 26 27 28 sylancl ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ℚ )
30 29 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → 𝐺 : ℕ ⟶ ℚ )
31 30 9 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( 𝐺 ‘ 𝑚 ) ∈ ℚ )
32 qcn ⊢ ( ( 𝐺 ‘ 𝑚 ) ∈ ℚ → ( 𝐺 ‘ 𝑚 ) ∈ ℂ )
33 31 32 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( 𝐺 ‘ 𝑚 ) ∈ ℂ )
34 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → 𝑘 ∈ ℕ )
35 30 34 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℚ )
36 qcn ⊢ ( ( 𝐺 ‘ 𝑘 ) ∈ ℚ → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
37 35 36 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
38 1 vitalilem1 ⊢ ∼ Er ( 0 [,] 1 )
39 38 a1i ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ∼ Er ( 0 [,] 1 ) )
40 1 2 3 4 5 6 7 vitalilem2 ⊢ ( 𝜑 → ( ran 𝐹 ⊆ ( 0 [,] 1 ) ∧ ( 0 [,] 1 ) ⊆ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ∧ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ⊆ ( - 1 [,] 2 ) ) )
41 40 simp1d ⊢ ( 𝜑 → ran 𝐹 ⊆ ( 0 [,] 1 ) )
42 41 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ran 𝐹 ⊆ ( 0 [,] 1 ) )
43 22 simprd ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 )
44 42 43 sseldd ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) ∈ ( 0 [,] 1 ) )
45 simprrr ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) )
46 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑘 ) )
47 46 oveq2d ⊢ ( 𝑛 = 𝑘 → ( 𝑠 − ( 𝐺 ‘ 𝑛 ) ) = ( 𝑠 − ( 𝐺 ‘ 𝑘 ) ) )
48 47 eleq1d ⊢ ( 𝑛 = 𝑘 → ( ( 𝑠 − ( 𝐺 ‘ 𝑛 ) ) ∈ ran 𝐹 ↔ ( 𝑠 − ( 𝐺 ‘ 𝑘 ) ) ∈ ran 𝐹 ) )
49 48 rabbidv ⊢ ( 𝑛 = 𝑘 → { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑛 ) ) ∈ ran 𝐹 } = { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑘 ) ) ∈ ran 𝐹 } )
50 14 rabex ⊢ { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑘 ) ) ∈ ran 𝐹 } ∈ V
51 49 6 50 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( 𝑇 ‘ 𝑘 ) = { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑘 ) ) ∈ ran 𝐹 } )
52 34 51 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( 𝑇 ‘ 𝑘 ) = { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑘 ) ) ∈ ran 𝐹 } )
53 45 52 eleqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → 𝑤 ∈ { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑘 ) ) ∈ ran 𝐹 } )
54 oveq1 ⊢ ( 𝑠 = 𝑤 → ( 𝑠 − ( 𝐺 ‘ 𝑘 ) ) = ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) )
55 54 eleq1d ⊢ ( 𝑠 = 𝑤 → ( ( 𝑠 − ( 𝐺 ‘ 𝑘 ) ) ∈ ran 𝐹 ↔ ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) ∈ ran 𝐹 ) )
56 55 elrab ⊢ ( 𝑤 ∈ { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑘 ) ) ∈ ran 𝐹 } ↔ ( 𝑤 ∈ ℝ ∧ ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) ∈ ran 𝐹 ) )
57 53 56 sylib ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( 𝑤 ∈ ℝ ∧ ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) ∈ ran 𝐹 ) )
58 57 simprd ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) ∈ ran 𝐹 )
59 42 58 sseldd ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) ∈ ( 0 [,] 1 ) )
60 24 33 37 nnncan1d ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) − ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) ) = ( ( 𝐺 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑚 ) ) )
61 qsubcl ⊢ ( ( ( 𝐺 ‘ 𝑘 ) ∈ ℚ ∧ ( 𝐺 ‘ 𝑚 ) ∈ ℚ ) → ( ( 𝐺 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑚 ) ) ∈ ℚ )
62 35 31 61 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( ( 𝐺 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑚 ) ) ∈ ℚ )
63 60 62 eqeltrd ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) − ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) ) ∈ ℚ )
64 oveq12 ⊢ ( ( 𝑥 = ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) ∧ 𝑦 = ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) ) → ( 𝑥 − 𝑦 ) = ( ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) − ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) ) )
65 64 eleq1d ⊢ ( ( 𝑥 = ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) ∧ 𝑦 = ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) ) → ( ( 𝑥 − 𝑦 ) ∈ ℚ ↔ ( ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) − ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) ) ∈ ℚ ) )
66 65 1 brab2a ⊢ ( ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) ∼ ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) ↔ ( ( ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) ∈ ( 0 [,] 1 ) ∧ ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) ∈ ( 0 [,] 1 ) ) ∧ ( ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) − ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) ) ∈ ℚ ) )
67 44 59 63 66 syl21anbrc ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) ∼ ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) )
68 39 67 erthi ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → [ ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) ] ∼ = [ ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) ] ∼ )
69 68 fveq2d ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( 𝐹 ‘ [ ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) ] ∼ ) = ( 𝐹 ‘ [ ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) ] ∼ ) )
70 eceq1 ⊢ ( 𝑧 = ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) → [ 𝑧 ] ∼ = [ ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) ] ∼ )
71 70 fveq2d ⊢ ( 𝑧 = ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) → ( 𝐹 ‘ [ 𝑧 ] ∼ ) = ( 𝐹 ‘ [ ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) ] ∼ ) )
72 id ⊢ ( 𝑧 = ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) → 𝑧 = ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) )
73 71 72 eqeq12d ⊢ ( 𝑧 = ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) → ( ( 𝐹 ‘ [ 𝑧 ] ∼ ) = 𝑧 ↔ ( 𝐹 ‘ [ ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) ] ∼ ) = ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) ) )
74 fveq2 ⊢ ( [ 𝑣 ] ∼ = 𝑤 → ( 𝐹 ‘ [ 𝑣 ] ∼ ) = ( 𝐹 ‘ 𝑤 ) )
75 74 eceq1d ⊢ ( [ 𝑣 ] ∼ = 𝑤 → [ ( 𝐹 ‘ [ 𝑣 ] ∼ ) ] ∼ = [ ( 𝐹 ‘ 𝑤 ) ] ∼ )
76 75 fveq2d ⊢ ( [ 𝑣 ] ∼ = 𝑤 → ( 𝐹 ‘ [ ( 𝐹 ‘ [ 𝑣 ] ∼ ) ] ∼ ) = ( 𝐹 ‘ [ ( 𝐹 ‘ 𝑤 ) ] ∼ ) )
77 76 74 eqeq12d ⊢ ( [ 𝑣 ] ∼ = 𝑤 → ( ( 𝐹 ‘ [ ( 𝐹 ‘ [ 𝑣 ] ∼ ) ] ∼ ) = ( 𝐹 ‘ [ 𝑣 ] ∼ ) ↔ ( 𝐹 ‘ [ ( 𝐹 ‘ 𝑤 ) ] ∼ ) = ( 𝐹 ‘ 𝑤 ) ) )
78 38 a1i ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ∼ Er ( 0 [,] 1 ) )
79 erdm ⊢ ( ∼ Er ( 0 [,] 1 ) → dom ∼ = ( 0 [,] 1 ) )
80 38 79 ax-mp ⊢ dom ∼ = ( 0 [,] 1 )
81 80 eleq2i ⊢ ( 𝑣 ∈ dom ∼ ↔ 𝑣 ∈ ( 0 [,] 1 ) )
82 ecdmn0 ⊢ ( 𝑣 ∈ dom ∼ ↔ [ 𝑣 ] ∼ ≠ ∅ )
83 81 82 bitr3i ⊢ ( 𝑣 ∈ ( 0 [,] 1 ) ↔ [ 𝑣 ] ∼ ≠ ∅ )
84 83 bilani ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → [ 𝑣 ] ∼ ≠ ∅ )
85 neeq1 ⊢ ( 𝑧 = [ 𝑣 ] ∼ → ( 𝑧 ≠ ∅ ↔ [ 𝑣 ] ∼ ≠ ∅ ) )
86 fveq2 ⊢ ( 𝑧 = [ 𝑣 ] ∼ → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ [ 𝑣 ] ∼ ) )
87 id ⊢ ( 𝑧 = [ 𝑣 ] ∼ → 𝑧 = [ 𝑣 ] ∼ )
88 86 87 eleq12d ⊢ ( 𝑧 = [ 𝑣 ] ∼ → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ↔ ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ [ 𝑣 ] ∼ ) )
89 85 88 imbi12d ⊢ ( 𝑧 = [ 𝑣 ] ∼ → ( ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( [ 𝑣 ] ∼ ≠ ∅ → ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ [ 𝑣 ] ∼ ) ) )
90 4 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ∀ 𝑧 ∈ 𝑆 ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) )
91 ovex ⊢ ( 0 [,] 1 ) ∈ V
92 erex ⊢ ( ∼ Er ( 0 [,] 1 ) → ( ( 0 [,] 1 ) ∈ V → ∼ ∈ V ) )
93 38 91 92 mp2 ⊢ ∼ ∈ V
94 93 ecelqsi ⊢ ( 𝑣 ∈ ( 0 [,] 1 ) → [ 𝑣 ] ∼ ∈ ( ( 0 [,] 1 ) / ∼ ) )
95 94 2 eleqtrrdi ⊢ ( 𝑣 ∈ ( 0 [,] 1 ) → [ 𝑣 ] ∼ ∈ 𝑆 )
96 95 adantl ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → [ 𝑣 ] ∼ ∈ 𝑆 )
97 89 90 96 rspcdva ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( [ 𝑣 ] ∼ ≠ ∅ → ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ [ 𝑣 ] ∼ ) )
98 84 97 mpd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ [ 𝑣 ] ∼ )
99 fvex ⊢ ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ V
100 vex ⊢ 𝑣 ∈ V
101 99 100 elec ⊢ ( ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ [ 𝑣 ] ∼ ↔ 𝑣 ∼ ( 𝐹 ‘ [ 𝑣 ] ∼ ) )
102 98 101 sylib ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → 𝑣 ∼ ( 𝐹 ‘ [ 𝑣 ] ∼ ) )
103 78 102 erthi ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → [ 𝑣 ] ∼ = [ ( 𝐹 ‘ [ 𝑣 ] ∼ ) ] ∼ )
104 103 eqcomd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → [ ( 𝐹 ‘ [ 𝑣 ] ∼ ) ] ∼ = [ 𝑣 ] ∼ )
105 104 fveq2d ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ [ ( 𝐹 ‘ [ 𝑣 ] ∼ ) ] ∼ ) = ( 𝐹 ‘ [ 𝑣 ] ∼ ) )
106 2 77 105 ectocld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑆 ) → ( 𝐹 ‘ [ ( 𝐹 ‘ 𝑤 ) ] ∼ ) = ( 𝐹 ‘ 𝑤 ) )
107 106 ralrimiva ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝑆 ( 𝐹 ‘ [ ( 𝐹 ‘ 𝑤 ) ] ∼ ) = ( 𝐹 ‘ 𝑤 ) )
108 eceq1 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑤 ) → [ 𝑧 ] ∼ = [ ( 𝐹 ‘ 𝑤 ) ] ∼ )
109 108 fveq2d ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑤 ) → ( 𝐹 ‘ [ 𝑧 ] ∼ ) = ( 𝐹 ‘ [ ( 𝐹 ‘ 𝑤 ) ] ∼ ) )
110 id ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑤 ) → 𝑧 = ( 𝐹 ‘ 𝑤 ) )
111 109 110 eqeq12d ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑤 ) → ( ( 𝐹 ‘ [ 𝑧 ] ∼ ) = 𝑧 ↔ ( 𝐹 ‘ [ ( 𝐹 ‘ 𝑤 ) ] ∼ ) = ( 𝐹 ‘ 𝑤 ) ) )
112 111 ralrn ⊢ ( 𝐹 Fn 𝑆 → ( ∀ 𝑧 ∈ ran 𝐹 ( 𝐹 ‘ [ 𝑧 ] ∼ ) = 𝑧 ↔ ∀ 𝑤 ∈ 𝑆 ( 𝐹 ‘ [ ( 𝐹 ‘ 𝑤 ) ] ∼ ) = ( 𝐹 ‘ 𝑤 ) ) )
113 3 112 syl ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran 𝐹 ( 𝐹 ‘ [ 𝑧 ] ∼ ) = 𝑧 ↔ ∀ 𝑤 ∈ 𝑆 ( 𝐹 ‘ [ ( 𝐹 ‘ 𝑤 ) ] ∼ ) = ( 𝐹 ‘ 𝑤 ) ) )
114 107 113 mpbird ⊢ ( 𝜑 → ∀ 𝑧 ∈ ran 𝐹 ( 𝐹 ‘ [ 𝑧 ] ∼ ) = 𝑧 )
115 114 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ∀ 𝑧 ∈ ran 𝐹 ( 𝐹 ‘ [ 𝑧 ] ∼ ) = 𝑧 )
116 73 115 43 rspcdva ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( 𝐹 ‘ [ ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) ] ∼ ) = ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) )
117 eceq1 ⊢ ( 𝑧 = ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) → [ 𝑧 ] ∼ = [ ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) ] ∼ )
118 117 fveq2d ⊢ ( 𝑧 = ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) → ( 𝐹 ‘ [ 𝑧 ] ∼ ) = ( 𝐹 ‘ [ ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) ] ∼ ) )
119 id ⊢ ( 𝑧 = ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) → 𝑧 = ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) )
120 118 119 eqeq12d ⊢ ( 𝑧 = ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) → ( ( 𝐹 ‘ [ 𝑧 ] ∼ ) = 𝑧 ↔ ( 𝐹 ‘ [ ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) ] ∼ ) = ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) ) )
121 120 115 58 rspcdva ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( 𝐹 ‘ [ ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) ] ∼ ) = ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) )
122 69 116 121 3eqtr3d ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) = ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) )
123 24 33 37 122 subcand ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( 𝐺 ‘ 𝑚 ) = ( 𝐺 ‘ 𝑘 ) )
124 5 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → 𝐺 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) ) )
125 f1of1 ⊢ ( 𝐺 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) ) → 𝐺 : ℕ –1-1→ ( ℚ ∩ ( - 1 [,] 1 ) ) )
126 124 125 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → 𝐺 : ℕ –1-1→ ( ℚ ∩ ( - 1 [,] 1 ) ) )
127 f1fveq ⊢ ( ( 𝐺 : ℕ –1-1→ ( ℚ ∩ ( - 1 [,] 1 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( ( 𝐺 ‘ 𝑚 ) = ( 𝐺 ‘ 𝑘 ) ↔ 𝑚 = 𝑘 ) )
128 126 9 34 127 syl12anc ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( ( 𝐺 ‘ 𝑚 ) = ( 𝐺 ‘ 𝑘 ) ↔ 𝑚 = 𝑘 ) )
129 123 128 mpbid ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → 𝑚 = 𝑘 )
130 129 ex ⊢ ( 𝜑 → ( ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) → 𝑚 = 𝑘 ) )
131 130 alrimivv ⊢ ( 𝜑 → ∀ 𝑚 ∀ 𝑘 ( ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) → 𝑚 = 𝑘 ) )
132 eleq1w ⊢ ( 𝑚 = 𝑘 → ( 𝑚 ∈ ℕ ↔ 𝑘 ∈ ℕ ) )
133 fveq2 ⊢ ( 𝑚 = 𝑘 → ( 𝑇 ‘ 𝑚 ) = ( 𝑇 ‘ 𝑘 ) )
134 133 eleq2d ⊢ ( 𝑚 = 𝑘 → ( 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ↔ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) )
135 132 134 anbi12d ⊢ ( 𝑚 = 𝑘 → ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ↔ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) )
136 135 mo4 ⊢ ( ∃* 𝑚 ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ↔ ∀ 𝑚 ∀ 𝑘 ( ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) → 𝑚 = 𝑘 ) )
137 131 136 sylibr ⊢ ( 𝜑 → ∃* 𝑚 ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) )
138 137 alrimiv ⊢ ( 𝜑 → ∀ 𝑤 ∃* 𝑚 ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) )
139 dfdisj2 ⊢ ( Disj 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ↔ ∀ 𝑤 ∃* 𝑚 ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) )
140 138 139 sylibr ⊢ ( 𝜑 → Disj 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) )