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 syl5eq ( ( 𝜑𝑓 : ℕ –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 ffvelrn ( ( 𝑓 : ℕ ⟶ ran 𝐹𝑎 ∈ ℕ ) → ( 𝑓𝑎 ) ∈ ran 𝐹 )
54 51 52 53 syl2an ( ( ( 𝜑𝑓 : ℕ –1-1-onto𝐺 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( 𝑓𝑎 ) ∈ ran 𝐹 )
55 simpr ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) → 𝑏 ∈ ℕ )
56 ffvelrn ( ( 𝑓 : ℕ ⟶ 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 ffvelrn ( ( 𝑓 : ℕ ⟶ 𝐺𝑎 ∈ ℕ ) → ( 𝑓𝑎 ) ∈ 𝐺 )
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 ffvelrn ( ( 𝑓 : ℕ ⟶ 𝐺𝑏 ∈ ℕ ) → ( 𝑓𝑏 ) ∈ 𝐺 )
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 syl6bi ( ( ( 𝜑𝑓 : ℕ –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 )