Metamath Proof Explorer

Theorem dyadmbl

Description: Any union of dyadic rational intervals is measurable. (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypotheses dyadmbl.1 ⊢ 𝐹 = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ )
dyadmbl.2 ⊢ 𝐺 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) }
dyadmbl.3 ⊢ ( 𝜑 → 𝐴 ⊆ ran 𝐹 )
Assertion dyadmbl ( 𝜑 → ∪ ( [,] “ 𝐴 ) ∈ dom vol )

Proof

Step Hyp Ref Expression
1 dyadmbl.1 ⊢ 𝐹 = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ )
2 dyadmbl.2 ⊢ 𝐺 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) }
3 dyadmbl.3 ⊢ ( 𝜑 → 𝐴 ⊆ ran 𝐹 )
4 1 2 3 dyadmbllem ⊢ ( 𝜑 → ∪ ( [,] “ 𝐴 ) = ∪ ( [,] “ 𝐺 ) )
5 isfinite ⊢ ( 𝐺 ∈ Fin ↔ 𝐺 ≺ ω )
6 iccf ⊢ [,] : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ*
7 ffun ⊢ ( [,] : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* → Fun [,] )
8 funiunfv ⊢ ( Fun [,] → ∪ 𝑛 ∈ 𝐺 ( [,] ‘ 𝑛 ) = ∪ ( [,] “ 𝐺 ) )
9 6 7 8 mp2b ⊢ ∪ 𝑛 ∈ 𝐺 ( [,] ‘ 𝑛 ) = ∪ ( [,] “ 𝐺 )
10 simpr ⊢ ( ( 𝜑 ∧ 𝐺 ∈ Fin ) → 𝐺 ∈ Fin )
11 2 ssrab3 ⊢ 𝐺 ⊆ 𝐴
12 11 3 sstrid ⊢ ( 𝜑 → 𝐺 ⊆ ran 𝐹 )
13 1 dyadf ⊢ 𝐹 : ( ℤ × ℕ0 ) ⟶ ( ≤ ∩ ( ℝ × ℝ ) )
14 frn ⊢ ( 𝐹 : ( ℤ × ℕ0 ) ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ran 𝐹 ⊆ ( ≤ ∩ ( ℝ × ℝ ) ) )
15 13 14 ax-mp ⊢ ran 𝐹 ⊆ ( ≤ ∩ ( ℝ × ℝ ) )
16 inss2 ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
17 15 16 sstri ⊢ ran 𝐹 ⊆ ( ℝ × ℝ )
18 12 17 sstrdi ⊢ ( 𝜑 → 𝐺 ⊆ ( ℝ × ℝ ) )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝐺 ∈ Fin ) → 𝐺 ⊆ ( ℝ × ℝ ) )
20 19 sselda ⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ Fin ) ∧ 𝑛 ∈ 𝐺 ) → 𝑛 ∈ ( ℝ × ℝ ) )
21 1st2nd2 ⊢ ( 𝑛 ∈ ( ℝ × ℝ ) → 𝑛 = ⟨ ( 1st ‘ 𝑛 ) , ( 2nd ‘ 𝑛 ) ⟩ )
22 20 21 syl ⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ Fin ) ∧ 𝑛 ∈ 𝐺 ) → 𝑛 = ⟨ ( 1st ‘ 𝑛 ) , ( 2nd ‘ 𝑛 ) ⟩ )
23 22 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ Fin ) ∧ 𝑛 ∈ 𝐺 ) → ( [,] ‘ 𝑛 ) = ( [,] ‘ ⟨ ( 1st ‘ 𝑛 ) , ( 2nd ‘ 𝑛 ) ⟩ ) )
24 df-ov ⊢ ( ( 1st ‘ 𝑛 ) [,] ( 2nd ‘ 𝑛 ) ) = ( [,] ‘ ⟨ ( 1st ‘ 𝑛 ) , ( 2nd ‘ 𝑛 ) ⟩ )
25 23 24 eqtr4di ⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ Fin ) ∧ 𝑛 ∈ 𝐺 ) → ( [,] ‘ 𝑛 ) = ( ( 1st ‘ 𝑛 ) [,] ( 2nd ‘ 𝑛 ) ) )
26 xp1st ⊢ ( 𝑛 ∈ ( ℝ × ℝ ) → ( 1st ‘ 𝑛 ) ∈ ℝ )
27 20 26 syl ⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ Fin ) ∧ 𝑛 ∈ 𝐺 ) → ( 1st ‘ 𝑛 ) ∈ ℝ )
28 xp2nd ⊢ ( 𝑛 ∈ ( ℝ × ℝ ) → ( 2nd ‘ 𝑛 ) ∈ ℝ )
29 20 28 syl ⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ Fin ) ∧ 𝑛 ∈ 𝐺 ) → ( 2nd ‘ 𝑛 ) ∈ ℝ )
30 iccmbl ⊢ ( ( ( 1st ‘ 𝑛 ) ∈ ℝ ∧ ( 2nd ‘ 𝑛 ) ∈ ℝ ) → ( ( 1st ‘ 𝑛 ) [,] ( 2nd ‘ 𝑛 ) ) ∈ dom vol )
31 27 29 30 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ Fin ) ∧ 𝑛 ∈ 𝐺 ) → ( ( 1st ‘ 𝑛 ) [,] ( 2nd ‘ 𝑛 ) ) ∈ dom vol )
32 25 31 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ Fin ) ∧ 𝑛 ∈ 𝐺 ) → ( [,] ‘ 𝑛 ) ∈ dom vol )
33 32 ralrimiva ⊢ ( ( 𝜑 ∧ 𝐺 ∈ Fin ) → ∀ 𝑛 ∈ 𝐺 ( [,] ‘ 𝑛 ) ∈ dom vol )
34 finiunmbl ⊢ ( ( 𝐺 ∈ Fin ∧ ∀ 𝑛 ∈ 𝐺 ( [,] ‘ 𝑛 ) ∈ dom vol ) → ∪ 𝑛 ∈ 𝐺 ( [,] ‘ 𝑛 ) ∈ dom vol )
35 10 33 34 syl2anc ⊢ ( ( 𝜑 ∧ 𝐺 ∈ Fin ) → ∪ 𝑛 ∈ 𝐺 ( [,] ‘ 𝑛 ) ∈ dom vol )
36 9 35 eqeltrrid ⊢ ( ( 𝜑 ∧ 𝐺 ∈ Fin ) → ∪ ( [,] “ 𝐺 ) ∈ dom vol )
37 5 36 sylan2br ⊢ ( ( 𝜑 ∧ 𝐺 ≺ ω ) → ∪ ( [,] “ 𝐺 ) ∈ dom vol )
38 rnco2 ⊢ ran ( [,] ∘ 𝑓 ) = ( [,] “ ran 𝑓 )
39 f1ofo ⊢ ( 𝑓 : ℕ –1-1-onto→ 𝐺 → 𝑓 : ℕ –onto→ 𝐺 )
40 39 adantl ⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) → 𝑓 : ℕ –onto→ 𝐺 )
41 forn ⊢ ( 𝑓 : ℕ –onto→ 𝐺 → ran 𝑓 = 𝐺 )
42 40 41 syl ⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) → ran 𝑓 = 𝐺 )
43 42 imaeq2d ⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) → ( [,] “ ran 𝑓 ) = ( [,] “ 𝐺 ) )
44 38 43 eqtrid ⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) → ran ( [,] ∘ 𝑓 ) = ( [,] “ 𝐺 ) )
45 44 unieqd ⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) → ∪ ran ( [,] ∘ 𝑓 ) = ∪ ( [,] “ 𝐺 ) )
46 f1of ⊢ ( 𝑓 : ℕ –1-1-onto→ 𝐺 → 𝑓 : ℕ ⟶ 𝐺 )
47 12 15 sstrdi ⊢ ( 𝜑 → 𝐺 ⊆ ( ≤ ∩ ( ℝ × ℝ ) ) )
48 fss ⊢ ( ( 𝑓 : ℕ ⟶ 𝐺 ∧ 𝐺 ⊆ ( ≤ ∩ ( ℝ × ℝ ) ) ) → 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
49 46 47 48 syl2anr ⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) → 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
50 fss ⊢ ( ( 𝑓 : ℕ ⟶ 𝐺 ∧ 𝐺 ⊆ ran 𝐹 ) → 𝑓 : ℕ ⟶ ran 𝐹 )
51 46 12 50 syl2anr ⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) → 𝑓 : ℕ ⟶ ran 𝐹 )
52 simpl ⊢ ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) → 𝑎 ∈ ℕ )
53 ffvelcdm ⊢ ( ( 𝑓 : ℕ ⟶ ran 𝐹 ∧ 𝑎 ∈ ℕ ) → ( 𝑓 ‘ 𝑎 ) ∈ ran 𝐹 )
54 51 52 53 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( 𝑓 ‘ 𝑎 ) ∈ ran 𝐹 )
55 simpr ⊢ ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) → 𝑏 ∈ ℕ )
56 ffvelcdm ⊢ ( ( 𝑓 : ℕ ⟶ ran 𝐹 ∧ 𝑏 ∈ ℕ ) → ( 𝑓 ‘ 𝑏 ) ∈ ran 𝐹 )
57 51 55 56 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( 𝑓 ‘ 𝑏 ) ∈ ran 𝐹 )
58 1 dyaddisj ⊢ ( ( ( 𝑓 ‘ 𝑎 ) ∈ ran 𝐹 ∧ ( 𝑓 ‘ 𝑏 ) ∈ ran 𝐹 ) → ( ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ∨ ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ∨ ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ ) )
59 54 57 58 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ∨ ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ∨ ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ ) )
60 fveq2 ⊢ ( 𝑤 = ( 𝑓 ‘ 𝑏 ) → ( [,] ‘ 𝑤 ) = ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) )
61 60 sseq2d ⊢ ( 𝑤 = ( 𝑓 ‘ 𝑏 ) → ( ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ 𝑤 ) ↔ ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ) )
62 eqeq2 ⊢ ( 𝑤 = ( 𝑓 ‘ 𝑏 ) → ( ( 𝑓 ‘ 𝑎 ) = 𝑤 ↔ ( 𝑓 ‘ 𝑎 ) = ( 𝑓 ‘ 𝑏 ) ) )
63 61 62 imbi12d ⊢ ( 𝑤 = ( 𝑓 ‘ 𝑏 ) → ( ( ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑓 ‘ 𝑎 ) = 𝑤 ) ↔ ( ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) → ( 𝑓 ‘ 𝑎 ) = ( 𝑓 ‘ 𝑏 ) ) ) )
64 46 adantl ⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) → 𝑓 : ℕ ⟶ 𝐺 )
65 ffvelcdm ⊢ ( ( 𝑓 : ℕ ⟶ 𝐺 ∧ 𝑎 ∈ ℕ ) → ( 𝑓 ‘ 𝑎 ) ∈ 𝐺 )
66 64 52 65 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( 𝑓 ‘ 𝑎 ) ∈ 𝐺 )
67 fveq2 ⊢ ( 𝑧 = ( 𝑓 ‘ 𝑎 ) → ( [,] ‘ 𝑧 ) = ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) )
68 67 sseq1d ⊢ ( 𝑧 = ( 𝑓 ‘ 𝑎 ) → ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) ↔ ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ 𝑤 ) ) )
69 eqeq1 ⊢ ( 𝑧 = ( 𝑓 ‘ 𝑎 ) → ( 𝑧 = 𝑤 ↔ ( 𝑓 ‘ 𝑎 ) = 𝑤 ) )
70 68 69 imbi12d ⊢ ( 𝑧 = ( 𝑓 ‘ 𝑎 ) → ( ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) ↔ ( ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑓 ‘ 𝑎 ) = 𝑤 ) ) )
71 70 ralbidv ⊢ ( 𝑧 = ( 𝑓 ‘ 𝑎 ) → ( ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) ↔ ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑓 ‘ 𝑎 ) = 𝑤 ) ) )
72 71 2 elrab2 ⊢ ( ( 𝑓 ‘ 𝑎 ) ∈ 𝐺 ↔ ( ( 𝑓 ‘ 𝑎 ) ∈ 𝐴 ∧ ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑓 ‘ 𝑎 ) = 𝑤 ) ) )
73 72 simprbi ⊢ ( ( 𝑓 ‘ 𝑎 ) ∈ 𝐺 → ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑓 ‘ 𝑎 ) = 𝑤 ) )
74 66 73 syl ⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑓 ‘ 𝑎 ) = 𝑤 ) )
75 ffvelcdm ⊢ ( ( 𝑓 : ℕ ⟶ 𝐺 ∧ 𝑏 ∈ ℕ ) → ( 𝑓 ‘ 𝑏 ) ∈ 𝐺 )
76 64 55 75 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( 𝑓 ‘ 𝑏 ) ∈ 𝐺 )
77 11 76 sselid ⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( 𝑓 ‘ 𝑏 ) ∈ 𝐴 )
78 63 74 77 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) → ( 𝑓 ‘ 𝑎 ) = ( 𝑓 ‘ 𝑏 ) ) )
79 f1of1 ⊢ ( 𝑓 : ℕ –1-1-onto→ 𝐺 → 𝑓 : ℕ –1-1→ 𝐺 )
80 79 adantl ⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) → 𝑓 : ℕ –1-1→ 𝐺 )
81 f1fveq ⊢ ( ( 𝑓 : ℕ –1-1→ 𝐺 ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( ( 𝑓 ‘ 𝑎 ) = ( 𝑓 ‘ 𝑏 ) ↔ 𝑎 = 𝑏 ) )
82 80 81 sylan ⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( ( 𝑓 ‘ 𝑎 ) = ( 𝑓 ‘ 𝑏 ) ↔ 𝑎 = 𝑏 ) )
83 orc ⊢ ( 𝑎 = 𝑏 → ( 𝑎 = 𝑏 ∨ ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ ) )
84 82 83 biimtrdi ⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( ( 𝑓 ‘ 𝑎 ) = ( 𝑓 ‘ 𝑏 ) → ( 𝑎 = 𝑏 ∨ ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ ) ) )
85 78 84 syld ⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) → ( 𝑎 = 𝑏 ∨ ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ ) ) )
86 fveq2 ⊢ ( 𝑤 = ( 𝑓 ‘ 𝑎 ) → ( [,] ‘ 𝑤 ) = ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) )
87 86 sseq2d ⊢ ( 𝑤 = ( 𝑓 ‘ 𝑎 ) → ( ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ 𝑤 ) ↔ ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ) )
88 eqeq2 ⊢ ( 𝑤 = ( 𝑓 ‘ 𝑎 ) → ( ( 𝑓 ‘ 𝑏 ) = 𝑤 ↔ ( 𝑓 ‘ 𝑏 ) = ( 𝑓 ‘ 𝑎 ) ) )
89 eqcom ⊢ ( ( 𝑓 ‘ 𝑏 ) = ( 𝑓 ‘ 𝑎 ) ↔ ( 𝑓 ‘ 𝑎 ) = ( 𝑓 ‘ 𝑏 ) )
90 88 89 bitrdi ⊢ ( 𝑤 = ( 𝑓 ‘ 𝑎 ) → ( ( 𝑓 ‘ 𝑏 ) = 𝑤 ↔ ( 𝑓 ‘ 𝑎 ) = ( 𝑓 ‘ 𝑏 ) ) )
91 87 90 imbi12d ⊢ ( 𝑤 = ( 𝑓 ‘ 𝑎 ) → ( ( ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑓 ‘ 𝑏 ) = 𝑤 ) ↔ ( ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) → ( 𝑓 ‘ 𝑎 ) = ( 𝑓 ‘ 𝑏 ) ) ) )
92 fveq2 ⊢ ( 𝑧 = ( 𝑓 ‘ 𝑏 ) → ( [,] ‘ 𝑧 ) = ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) )
93 92 sseq1d ⊢ ( 𝑧 = ( 𝑓 ‘ 𝑏 ) → ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) ↔ ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ 𝑤 ) ) )
94 eqeq1 ⊢ ( 𝑧 = ( 𝑓 ‘ 𝑏 ) → ( 𝑧 = 𝑤 ↔ ( 𝑓 ‘ 𝑏 ) = 𝑤 ) )
95 93 94 imbi12d ⊢ ( 𝑧 = ( 𝑓 ‘ 𝑏 ) → ( ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) ↔ ( ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑓 ‘ 𝑏 ) = 𝑤 ) ) )
96 95 ralbidv ⊢ ( 𝑧 = ( 𝑓 ‘ 𝑏 ) → ( ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) ↔ ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑓 ‘ 𝑏 ) = 𝑤 ) ) )
97 96 2 elrab2 ⊢ ( ( 𝑓 ‘ 𝑏 ) ∈ 𝐺 ↔ ( ( 𝑓 ‘ 𝑏 ) ∈ 𝐴 ∧ ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑓 ‘ 𝑏 ) = 𝑤 ) ) )
98 97 simprbi ⊢ ( ( 𝑓 ‘ 𝑏 ) ∈ 𝐺 → ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑓 ‘ 𝑏 ) = 𝑤 ) )
99 76 98 syl ⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑓 ‘ 𝑏 ) = 𝑤 ) )
100 11 66 sselid ⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( 𝑓 ‘ 𝑎 ) ∈ 𝐴 )
101 91 99 100 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) → ( 𝑓 ‘ 𝑎 ) = ( 𝑓 ‘ 𝑏 ) ) )
102 101 84 syld ⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) → ( 𝑎 = 𝑏 ∨ ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ ) ) )
103 olc ⊢ ( ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ → ( 𝑎 = 𝑏 ∨ ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ ) )
104 103 a1i ⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ → ( 𝑎 = 𝑏 ∨ ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ ) ) )
105 85 102 104 3jaod ⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( ( ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ⊆ ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ∨ ( [,] ‘ ( 𝑓 ‘ 𝑏 ) ) ⊆ ( [,] ‘ ( 𝑓 ‘ 𝑎 ) ) ∨ ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ ) → ( 𝑎 = 𝑏 ∨ ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ ) ) )
106 59 105 mpd ⊢ ( ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( 𝑎 = 𝑏 ∨ ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ ) )
107 106 ralrimivva ⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) → ∀ 𝑎 ∈ ℕ ∀ 𝑏 ∈ ℕ ( 𝑎 = 𝑏 ∨ ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ ) )
108 2fveq3 ⊢ ( 𝑎 = 𝑏 → ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) = ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) )
109 108 disjor ⊢ ( Disj 𝑎 ∈ ℕ ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ↔ ∀ 𝑎 ∈ ℕ ∀ 𝑏 ∈ ℕ ( 𝑎 = 𝑏 ∨ ( ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) ∩ ( (,) ‘ ( 𝑓 ‘ 𝑏 ) ) ) = ∅ ) )
110 107 109 sylibr ⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) → Disj 𝑎 ∈ ℕ ( (,) ‘ ( 𝑓 ‘ 𝑎 ) ) )
111 eqid ⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) )
112 49 110 111 uniiccmbl ⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) → ∪ ran ( [,] ∘ 𝑓 ) ∈ dom vol )
113 45 112 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ 𝐺 ) → ∪ ( [,] “ 𝐺 ) ∈ dom vol )
114 113 ex ⊢ ( 𝜑 → ( 𝑓 : ℕ –1-1-onto→ 𝐺 → ∪ ( [,] “ 𝐺 ) ∈ dom vol ) )
115 114 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑓 𝑓 : ℕ –1-1-onto→ 𝐺 → ∪ ( [,] “ 𝐺 ) ∈ dom vol ) )
116 nnenom ⊢ ℕ ≈ ω
117 ensym ⊢ ( 𝐺 ≈ ω → ω ≈ 𝐺 )
118 entr ⊢ ( ( ℕ ≈ ω ∧ ω ≈ 𝐺 ) → ℕ ≈ 𝐺 )
119 116 117 118 sylancr ⊢ ( 𝐺 ≈ ω → ℕ ≈ 𝐺 )
120 bren ⊢ ( ℕ ≈ 𝐺 ↔ ∃ 𝑓 𝑓 : ℕ –1-1-onto→ 𝐺 )
121 119 120 sylib ⊢ ( 𝐺 ≈ ω → ∃ 𝑓 𝑓 : ℕ –1-1-onto→ 𝐺 )
122 115 121 impel ⊢ ( ( 𝜑 ∧ 𝐺 ≈ ω ) → ∪ ( [,] “ 𝐺 ) ∈ dom vol )
123 reex ⊢ ℝ ∈ V
124 123 123 xpex ⊢ ( ℝ × ℝ ) ∈ V
125 124 inex2 ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ∈ V
126 125 15 ssexi ⊢ ran 𝐹 ∈ V
127 ssdomg ⊢ ( ran 𝐹 ∈ V → ( 𝐺 ⊆ ran 𝐹 → 𝐺 ≼ ran 𝐹 ) )
128 126 12 127 mpsyl ⊢ ( 𝜑 → 𝐺 ≼ ran 𝐹 )
129 omelon ⊢ ω ∈ On
130 znnen ⊢ ℤ ≈ ℕ
131 130 116 entri ⊢ ℤ ≈ ω
132 nn0ennn ⊢ ℕ0 ≈ ℕ
133 132 116 entri ⊢ ℕ0 ≈ ω
134 xpen ⊢ ( ( ℤ ≈ ω ∧ ℕ0 ≈ ω ) → ( ℤ × ℕ0 ) ≈ ( ω × ω ) )
135 131 133 134 mp2an ⊢ ( ℤ × ℕ0 ) ≈ ( ω × ω )
136 xpomen ⊢ ( ω × ω ) ≈ ω
137 135 136 entri ⊢ ( ℤ × ℕ0 ) ≈ ω
138 137 ensymi ⊢ ω ≈ ( ℤ × ℕ0 )
139 isnumi ⊢ ( ( ω ∈ On ∧ ω ≈ ( ℤ × ℕ0 ) ) → ( ℤ × ℕ0 ) ∈ dom card )
140 129 138 139 mp2an ⊢ ( ℤ × ℕ0 ) ∈ dom card
141 ffn ⊢ ( 𝐹 : ( ℤ × ℕ0 ) ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐹 Fn ( ℤ × ℕ0 ) )
142 13 141 ax-mp ⊢ 𝐹 Fn ( ℤ × ℕ0 )
143 dffn4 ⊢ ( 𝐹 Fn ( ℤ × ℕ0 ) ↔ 𝐹 : ( ℤ × ℕ0 ) –onto→ ran 𝐹 )
144 142 143 mpbi ⊢ 𝐹 : ( ℤ × ℕ0 ) –onto→ ran 𝐹
145 fodomnum ⊢ ( ( ℤ × ℕ0 ) ∈ dom card → ( 𝐹 : ( ℤ × ℕ0 ) –onto→ ran 𝐹 → ran 𝐹 ≼ ( ℤ × ℕ0 ) ) )
146 140 144 145 mp2 ⊢ ran 𝐹 ≼ ( ℤ × ℕ0 )
147 domentr ⊢ ( ( ran 𝐹 ≼ ( ℤ × ℕ0 ) ∧ ( ℤ × ℕ0 ) ≈ ω ) → ran 𝐹 ≼ ω )
148 146 137 147 mp2an ⊢ ran 𝐹 ≼ ω
149 domtr ⊢ ( ( 𝐺 ≼ ran 𝐹 ∧ ran 𝐹 ≼ ω ) → 𝐺 ≼ ω )
150 128 148 149 sylancl ⊢ ( 𝜑 → 𝐺 ≼ ω )
151 brdom2 ⊢ ( 𝐺 ≼ ω ↔ ( 𝐺 ≺ ω ∨ 𝐺 ≈ ω ) )
152 150 151 sylib ⊢ ( 𝜑 → ( 𝐺 ≺ ω ∨ 𝐺 ≈ ω ) )
153 37 122 152 mpjaodan ⊢ ( 𝜑 → ∪ ( [,] “ 𝐺 ) ∈ dom vol )
154 4 153 eqeltrd ⊢ ( 𝜑 → ∪ ( [,] “ 𝐴 ) ∈ dom vol )