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 ffvelrnd ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( 𝐺 ‘ 𝑚 ) ∈ ℚ )
32 qcn ⊢ ( ( 𝐺 ‘ 𝑚 ) ∈ ℚ → ( 𝐺 ‘ 𝑚 ) ∈ ℂ )
33 31 32 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( 𝐺 ‘ 𝑚 ) ∈ ℂ )
34 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → 𝑘 ∈ ℕ )
35 30 34 ffvelrnd ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℚ )
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 simpr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → 𝑣 ∈ ( 0 [,] 1 ) )
80 erdm ⊢ ( ∼ Er ( 0 [,] 1 ) → dom ∼ = ( 0 [,] 1 ) )
81 38 80 ax-mp ⊢ dom ∼ = ( 0 [,] 1 )
82 81 eleq2i ⊢ ( 𝑣 ∈ dom ∼ ↔ 𝑣 ∈ ( 0 [,] 1 ) )
83 ecdmn0 ⊢ ( 𝑣 ∈ dom ∼ ↔ [ 𝑣 ] ∼ ≠ ∅ )
84 82 83 bitr3i ⊢ ( 𝑣 ∈ ( 0 [,] 1 ) ↔ [ 𝑣 ] ∼ ≠ ∅ )
85 79 84 sylib ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → [ 𝑣 ] ∼ ≠ ∅ )
86 neeq1 ⊢ ( 𝑧 = [ 𝑣 ] ∼ → ( 𝑧 ≠ ∅ ↔ [ 𝑣 ] ∼ ≠ ∅ ) )
87 fveq2 ⊢ ( 𝑧 = [ 𝑣 ] ∼ → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ [ 𝑣 ] ∼ ) )
88 id ⊢ ( 𝑧 = [ 𝑣 ] ∼ → 𝑧 = [ 𝑣 ] ∼ )
89 87 88 eleq12d ⊢ ( 𝑧 = [ 𝑣 ] ∼ → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ↔ ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ [ 𝑣 ] ∼ ) )
90 86 89 imbi12d ⊢ ( 𝑧 = [ 𝑣 ] ∼ → ( ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( [ 𝑣 ] ∼ ≠ ∅ → ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ [ 𝑣 ] ∼ ) ) )
91 4 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ∀ 𝑧 ∈ 𝑆 ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) )
92 ovex ⊢ ( 0 [,] 1 ) ∈ V
93 erex ⊢ ( ∼ Er ( 0 [,] 1 ) → ( ( 0 [,] 1 ) ∈ V → ∼ ∈ V ) )
94 38 92 93 mp2 ⊢ ∼ ∈ V
95 94 ecelqsi ⊢ ( 𝑣 ∈ ( 0 [,] 1 ) → [ 𝑣 ] ∼ ∈ ( ( 0 [,] 1 ) / ∼ ) )
96 95 2 eleqtrrdi ⊢ ( 𝑣 ∈ ( 0 [,] 1 ) → [ 𝑣 ] ∼ ∈ 𝑆 )
97 96 adantl ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → [ 𝑣 ] ∼ ∈ 𝑆 )
98 90 91 97 rspcdva ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( [ 𝑣 ] ∼ ≠ ∅ → ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ [ 𝑣 ] ∼ ) )
99 85 98 mpd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ [ 𝑣 ] ∼ )
100 fvex ⊢ ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ V
101 vex ⊢ 𝑣 ∈ V
102 100 101 elec ⊢ ( ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ [ 𝑣 ] ∼ ↔ 𝑣 ∼ ( 𝐹 ‘ [ 𝑣 ] ∼ ) )
103 99 102 sylib ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → 𝑣 ∼ ( 𝐹 ‘ [ 𝑣 ] ∼ ) )
104 78 103 erthi ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → [ 𝑣 ] ∼ = [ ( 𝐹 ‘ [ 𝑣 ] ∼ ) ] ∼ )
105 104 eqcomd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → [ ( 𝐹 ‘ [ 𝑣 ] ∼ ) ] ∼ = [ 𝑣 ] ∼ )
106 105 fveq2d ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ [ ( 𝐹 ‘ [ 𝑣 ] ∼ ) ] ∼ ) = ( 𝐹 ‘ [ 𝑣 ] ∼ ) )
107 2 77 106 ectocld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑆 ) → ( 𝐹 ‘ [ ( 𝐹 ‘ 𝑤 ) ] ∼ ) = ( 𝐹 ‘ 𝑤 ) )
108 107 ralrimiva ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝑆 ( 𝐹 ‘ [ ( 𝐹 ‘ 𝑤 ) ] ∼ ) = ( 𝐹 ‘ 𝑤 ) )
109 eceq1 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑤 ) → [ 𝑧 ] ∼ = [ ( 𝐹 ‘ 𝑤 ) ] ∼ )
110 109 fveq2d ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑤 ) → ( 𝐹 ‘ [ 𝑧 ] ∼ ) = ( 𝐹 ‘ [ ( 𝐹 ‘ 𝑤 ) ] ∼ ) )
111 id ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑤 ) → 𝑧 = ( 𝐹 ‘ 𝑤 ) )
112 110 111 eqeq12d ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑤 ) → ( ( 𝐹 ‘ [ 𝑧 ] ∼ ) = 𝑧 ↔ ( 𝐹 ‘ [ ( 𝐹 ‘ 𝑤 ) ] ∼ ) = ( 𝐹 ‘ 𝑤 ) ) )
113 112 ralrn ⊢ ( 𝐹 Fn 𝑆 → ( ∀ 𝑧 ∈ ran 𝐹 ( 𝐹 ‘ [ 𝑧 ] ∼ ) = 𝑧 ↔ ∀ 𝑤 ∈ 𝑆 ( 𝐹 ‘ [ ( 𝐹 ‘ 𝑤 ) ] ∼ ) = ( 𝐹 ‘ 𝑤 ) ) )
114 3 113 syl ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran 𝐹 ( 𝐹 ‘ [ 𝑧 ] ∼ ) = 𝑧 ↔ ∀ 𝑤 ∈ 𝑆 ( 𝐹 ‘ [ ( 𝐹 ‘ 𝑤 ) ] ∼ ) = ( 𝐹 ‘ 𝑤 ) ) )
115 108 114 mpbird ⊢ ( 𝜑 → ∀ 𝑧 ∈ ran 𝐹 ( 𝐹 ‘ [ 𝑧 ] ∼ ) = 𝑧 )
116 115 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ∀ 𝑧 ∈ ran 𝐹 ( 𝐹 ‘ [ 𝑧 ] ∼ ) = 𝑧 )
117 73 116 43 rspcdva ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( 𝐹 ‘ [ ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) ] ∼ ) = ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) )
118 eceq1 ⊢ ( 𝑧 = ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) → [ 𝑧 ] ∼ = [ ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) ] ∼ )
119 118 fveq2d ⊢ ( 𝑧 = ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) → ( 𝐹 ‘ [ 𝑧 ] ∼ ) = ( 𝐹 ‘ [ ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) ] ∼ ) )
120 id ⊢ ( 𝑧 = ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) → 𝑧 = ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) )
121 119 120 eqeq12d ⊢ ( 𝑧 = ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) → ( ( 𝐹 ‘ [ 𝑧 ] ∼ ) = 𝑧 ↔ ( 𝐹 ‘ [ ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) ] ∼ ) = ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) ) )
122 121 116 58 rspcdva ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( 𝐹 ‘ [ ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) ] ∼ ) = ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) )
123 69 117 122 3eqtr3d ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( 𝑤 − ( 𝐺 ‘ 𝑚 ) ) = ( 𝑤 − ( 𝐺 ‘ 𝑘 ) ) )
124 24 33 37 123 subcand ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( 𝐺 ‘ 𝑚 ) = ( 𝐺 ‘ 𝑘 ) )
125 5 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → 𝐺 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) ) )
126 f1of1 ⊢ ( 𝐺 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) ) → 𝐺 : ℕ –1-1→ ( ℚ ∩ ( - 1 [,] 1 ) ) )
127 125 126 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → 𝐺 : ℕ –1-1→ ( ℚ ∩ ( - 1 [,] 1 ) ) )
128 f1fveq ⊢ ( ( 𝐺 : ℕ –1-1→ ( ℚ ∩ ( - 1 [,] 1 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( ( 𝐺 ‘ 𝑚 ) = ( 𝐺 ‘ 𝑘 ) ↔ 𝑚 = 𝑘 ) )
129 127 9 34 128 syl12anc ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → ( ( 𝐺 ‘ 𝑚 ) = ( 𝐺 ‘ 𝑘 ) ↔ 𝑚 = 𝑘 ) )
130 124 129 mpbid ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) ) → 𝑚 = 𝑘 )
131 130 ex ⊢ ( 𝜑 → ( ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) → 𝑚 = 𝑘 ) )
132 131 alrimivv ⊢ ( 𝜑 → ∀ 𝑚 ∀ 𝑘 ( ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) → 𝑚 = 𝑘 ) )
133 eleq1w ⊢ ( 𝑚 = 𝑘 → ( 𝑚 ∈ ℕ ↔ 𝑘 ∈ ℕ ) )
134 fveq2 ⊢ ( 𝑚 = 𝑘 → ( 𝑇 ‘ 𝑚 ) = ( 𝑇 ‘ 𝑘 ) )
135 134 eleq2d ⊢ ( 𝑚 = 𝑘 → ( 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ↔ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) )
136 133 135 anbi12d ⊢ ( 𝑚 = 𝑘 → ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ↔ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) )
137 136 mo4 ⊢ ( ∃* 𝑚 ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ↔ ∀ 𝑚 ∀ 𝑘 ( ( ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑘 ) ) ) → 𝑚 = 𝑘 ) )
138 132 137 sylibr ⊢ ( 𝜑 → ∃* 𝑚 ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) )
139 138 alrimiv ⊢ ( 𝜑 → ∀ 𝑤 ∃* 𝑚 ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) )
140 dfdisj2 ⊢ ( Disj 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ↔ ∀ 𝑤 ∃* 𝑚 ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ( 𝑇 ‘ 𝑚 ) ) )
141 139 140 sylibr ⊢ ( 𝜑 → Disj 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) )