Metamath Proof Explorer

Theorem mbfimaopnlem

Description: Lemma for mbfimaopn . (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses mbfimaopn.1 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
mbfimaopn.2 ⊢ 𝐺 = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + ( i · 𝑦 ) ) )
mbfimaopn.3 ⊢ 𝐵 = ( (,) “ ( ℚ × ℚ ) )
mbfimaopn.4 ⊢ 𝐾 = ran ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 × 𝑦 ) )
Assertion mbfimaopnlem ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽 ) → ( ◡ 𝐹 “ 𝐴 ) ∈ dom vol )

Proof

Step Hyp Ref Expression
1 mbfimaopn.1 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2 mbfimaopn.2 ⊢ 𝐺 = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + ( i · 𝑦 ) ) )
3 mbfimaopn.3 ⊢ 𝐵 = ( (,) “ ( ℚ × ℚ ) )
4 mbfimaopn.4 ⊢ 𝐾 = ran ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 × 𝑦 ) )
5 eqid ⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
6 2 5 1 cnrehmeo ⊢ 𝐺 ∈ ( ( ( topGen ‘ ran (,) ) ×t ( topGen ‘ ran (,) ) ) Homeo 𝐽 )
7 hmeocn ⊢ ( 𝐺 ∈ ( ( ( topGen ‘ ran (,) ) ×t ( topGen ‘ ran (,) ) ) Homeo 𝐽 ) → 𝐺 ∈ ( ( ( topGen ‘ ran (,) ) ×t ( topGen ‘ ran (,) ) ) Cn 𝐽 ) )
8 6 7 ax-mp ⊢ 𝐺 ∈ ( ( ( topGen ‘ ran (,) ) ×t ( topGen ‘ ran (,) ) ) Cn 𝐽 )
9 cnima ⊢ ( ( 𝐺 ∈ ( ( ( topGen ‘ ran (,) ) ×t ( topGen ‘ ran (,) ) ) Cn 𝐽 ) ∧ 𝐴 ∈ 𝐽 ) → ( ◡ 𝐺 “ 𝐴 ) ∈ ( ( topGen ‘ ran (,) ) ×t ( topGen ‘ ran (,) ) ) )
10 8 9 mpan ⊢ ( 𝐴 ∈ 𝐽 → ( ◡ 𝐺 “ 𝐴 ) ∈ ( ( topGen ‘ ran (,) ) ×t ( topGen ‘ ran (,) ) ) )
11 3 fveq2i ⊢ ( topGen ‘ 𝐵 ) = ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) )
12 11 tgqioo ⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ 𝐵 )
13 12 12 oveq12i ⊢ ( ( topGen ‘ ran (,) ) ×t ( topGen ‘ ran (,) ) ) = ( ( topGen ‘ 𝐵 ) ×t ( topGen ‘ 𝐵 ) )
14 qtopbas ⊢ ( (,) “ ( ℚ × ℚ ) ) ∈ TopBases
15 3 14 eqeltri ⊢ 𝐵 ∈ TopBases
16 txbasval ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝐵 ∈ TopBases ) → ( ( topGen ‘ 𝐵 ) ×t ( topGen ‘ 𝐵 ) ) = ( 𝐵 ×t 𝐵 ) )
17 15 15 16 mp2an ⊢ ( ( topGen ‘ 𝐵 ) ×t ( topGen ‘ 𝐵 ) ) = ( 𝐵 ×t 𝐵 )
18 4 txval ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝐵 ∈ TopBases ) → ( 𝐵 ×t 𝐵 ) = ( topGen ‘ 𝐾 ) )
19 15 15 18 mp2an ⊢ ( 𝐵 ×t 𝐵 ) = ( topGen ‘ 𝐾 )
20 13 17 19 3eqtri ⊢ ( ( topGen ‘ ran (,) ) ×t ( topGen ‘ ran (,) ) ) = ( topGen ‘ 𝐾 )
21 10 20 eleqtrdi ⊢ ( 𝐴 ∈ 𝐽 → ( ◡ 𝐺 “ 𝐴 ) ∈ ( topGen ‘ 𝐾 ) )
22 4 txbas ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝐵 ∈ TopBases ) → 𝐾 ∈ TopBases )
23 15 15 22 mp2an ⊢ 𝐾 ∈ TopBases
24 eltg3 ⊢ ( 𝐾 ∈ TopBases → ( ( ◡ 𝐺 “ 𝐴 ) ∈ ( topGen ‘ 𝐾 ) ↔ ∃ 𝑡 ( 𝑡 ⊆ 𝐾 ∧ ( ◡ 𝐺 “ 𝐴 ) = ∪ 𝑡 ) ) )
25 23 24 ax-mp ⊢ ( ( ◡ 𝐺 “ 𝐴 ) ∈ ( topGen ‘ 𝐾 ) ↔ ∃ 𝑡 ( 𝑡 ⊆ 𝐾 ∧ ( ◡ 𝐺 “ 𝐴 ) = ∪ 𝑡 ) )
26 21 25 sylib ⊢ ( 𝐴 ∈ 𝐽 → ∃ 𝑡 ( 𝑡 ⊆ 𝐾 ∧ ( ◡ 𝐺 “ 𝐴 ) = ∪ 𝑡 ) )
27 26 adantl ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽 ) → ∃ 𝑡 ( 𝑡 ⊆ 𝐾 ∧ ( ◡ 𝐺 “ 𝐴 ) = ∪ 𝑡 ) )
28 2 cnref1o ⊢ 𝐺 : ( ℝ × ℝ ) –1-1-onto→ ℂ
29 f1ofo ⊢ ( 𝐺 : ( ℝ × ℝ ) –1-1-onto→ ℂ → 𝐺 : ( ℝ × ℝ ) –onto→ ℂ )
30 28 29 ax-mp ⊢ 𝐺 : ( ℝ × ℝ ) –onto→ ℂ
31 elssuni ⊢ ( 𝐴 ∈ 𝐽 → 𝐴 ⊆ ∪ 𝐽 )
32 1 cnfldtopon ⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
33 32 toponunii ⊢ ℂ = ∪ 𝐽
34 31 33 sseqtrrdi ⊢ ( 𝐴 ∈ 𝐽 → 𝐴 ⊆ ℂ )
35 34 ad2antlr ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽 ) ∧ ( 𝑡 ⊆ 𝐾 ∧ ( ◡ 𝐺 “ 𝐴 ) = ∪ 𝑡 ) ) → 𝐴 ⊆ ℂ )
36 foimacnv ⊢ ( ( 𝐺 : ( ℝ × ℝ ) –onto→ ℂ ∧ 𝐴 ⊆ ℂ ) → ( 𝐺 “ ( ◡ 𝐺 “ 𝐴 ) ) = 𝐴 )
37 30 35 36 sylancr ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽 ) ∧ ( 𝑡 ⊆ 𝐾 ∧ ( ◡ 𝐺 “ 𝐴 ) = ∪ 𝑡 ) ) → ( 𝐺 “ ( ◡ 𝐺 “ 𝐴 ) ) = 𝐴 )
38 simprr ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽 ) ∧ ( 𝑡 ⊆ 𝐾 ∧ ( ◡ 𝐺 “ 𝐴 ) = ∪ 𝑡 ) ) → ( ◡ 𝐺 “ 𝐴 ) = ∪ 𝑡 )
39 38 imaeq2d ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽 ) ∧ ( 𝑡 ⊆ 𝐾 ∧ ( ◡ 𝐺 “ 𝐴 ) = ∪ 𝑡 ) ) → ( 𝐺 “ ( ◡ 𝐺 “ 𝐴 ) ) = ( 𝐺 “ ∪ 𝑡 ) )
40 imauni ⊢ ( 𝐺 “ ∪ 𝑡 ) = ∪ 𝑤 ∈ 𝑡 ( 𝐺 “ 𝑤 )
41 39 40 eqtrdi ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽 ) ∧ ( 𝑡 ⊆ 𝐾 ∧ ( ◡ 𝐺 “ 𝐴 ) = ∪ 𝑡 ) ) → ( 𝐺 “ ( ◡ 𝐺 “ 𝐴 ) ) = ∪ 𝑤 ∈ 𝑡 ( 𝐺 “ 𝑤 ) )
42 37 41 eqtr3d ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽 ) ∧ ( 𝑡 ⊆ 𝐾 ∧ ( ◡ 𝐺 “ 𝐴 ) = ∪ 𝑡 ) ) → 𝐴 = ∪ 𝑤 ∈ 𝑡 ( 𝐺 “ 𝑤 ) )
43 42 imaeq2d ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽 ) ∧ ( 𝑡 ⊆ 𝐾 ∧ ( ◡ 𝐺 “ 𝐴 ) = ∪ 𝑡 ) ) → ( ◡ 𝐹 “ 𝐴 ) = ( ◡ 𝐹 “ ∪ 𝑤 ∈ 𝑡 ( 𝐺 “ 𝑤 ) ) )
44 imaiun ⊢ ( ◡ 𝐹 “ ∪ 𝑤 ∈ 𝑡 ( 𝐺 “ 𝑤 ) ) = ∪ 𝑤 ∈ 𝑡 ( ◡ 𝐹 “ ( 𝐺 “ 𝑤 ) )
45 43 44 eqtrdi ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽 ) ∧ ( 𝑡 ⊆ 𝐾 ∧ ( ◡ 𝐺 “ 𝐴 ) = ∪ 𝑡 ) ) → ( ◡ 𝐹 “ 𝐴 ) = ∪ 𝑤 ∈ 𝑡 ( ◡ 𝐹 “ ( 𝐺 “ 𝑤 ) ) )
46 ssdomg ⊢ ( 𝐾 ∈ TopBases → ( 𝑡 ⊆ 𝐾 → 𝑡 ≼ 𝐾 ) )
47 23 46 ax-mp ⊢ ( 𝑡 ⊆ 𝐾 → 𝑡 ≼ 𝐾 )
48 omelon ⊢ ω ∈ On
49 nnenom ⊢ ℕ ≈ ω
50 49 ensymi ⊢ ω ≈ ℕ
51 isnumi ⊢ ( ( ω ∈ On ∧ ω ≈ ℕ ) → ℕ ∈ dom card )
52 48 50 51 mp2an ⊢ ℕ ∈ dom card
53 qnnen ⊢ ℚ ≈ ℕ
54 xpen ⊢ ( ( ℚ ≈ ℕ ∧ ℚ ≈ ℕ ) → ( ℚ × ℚ ) ≈ ( ℕ × ℕ ) )
55 53 53 54 mp2an ⊢ ( ℚ × ℚ ) ≈ ( ℕ × ℕ )
56 xpnnen ⊢ ( ℕ × ℕ ) ≈ ℕ
57 55 56 entri ⊢ ( ℚ × ℚ ) ≈ ℕ
58 57 49 entr2i ⊢ ω ≈ ( ℚ × ℚ )
59 isnumi ⊢ ( ( ω ∈ On ∧ ω ≈ ( ℚ × ℚ ) ) → ( ℚ × ℚ ) ∈ dom card )
60 48 58 59 mp2an ⊢ ( ℚ × ℚ ) ∈ dom card
61 ioof ⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
62 ffun ⊢ ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → Fun (,) )
63 61 62 ax-mp ⊢ Fun (,)
64 qssre ⊢ ℚ ⊆ ℝ
65 ressxr ⊢ ℝ ⊆ ℝ*
66 64 65 sstri ⊢ ℚ ⊆ ℝ*
67 xpss12 ⊢ ( ( ℚ ⊆ ℝ* ∧ ℚ ⊆ ℝ* ) → ( ℚ × ℚ ) ⊆ ( ℝ* × ℝ* ) )
68 66 66 67 mp2an ⊢ ( ℚ × ℚ ) ⊆ ( ℝ* × ℝ* )
69 61 fdmi ⊢ dom (,) = ( ℝ* × ℝ* )
70 68 69 sseqtrri ⊢ ( ℚ × ℚ ) ⊆ dom (,)
71 fores ⊢ ( ( Fun (,) ∧ ( ℚ × ℚ ) ⊆ dom (,) ) → ( (,) ↾ ( ℚ × ℚ ) ) : ( ℚ × ℚ ) –onto→ ( (,) “ ( ℚ × ℚ ) ) )
72 63 70 71 mp2an ⊢ ( (,) ↾ ( ℚ × ℚ ) ) : ( ℚ × ℚ ) –onto→ ( (,) “ ( ℚ × ℚ ) )
73 fodomnum ⊢ ( ( ℚ × ℚ ) ∈ dom card → ( ( (,) ↾ ( ℚ × ℚ ) ) : ( ℚ × ℚ ) –onto→ ( (,) “ ( ℚ × ℚ ) ) → ( (,) “ ( ℚ × ℚ ) ) ≼ ( ℚ × ℚ ) ) )
74 60 72 73 mp2 ⊢ ( (,) “ ( ℚ × ℚ ) ) ≼ ( ℚ × ℚ )
75 3 74 eqbrtri ⊢ 𝐵 ≼ ( ℚ × ℚ )
76 domentr ⊢ ( ( 𝐵 ≼ ( ℚ × ℚ ) ∧ ( ℚ × ℚ ) ≈ ℕ ) → 𝐵 ≼ ℕ )
77 75 57 76 mp2an ⊢ 𝐵 ≼ ℕ
78 15 elexi ⊢ 𝐵 ∈ V
79 78 xpdom1 ⊢ ( 𝐵 ≼ ℕ → ( 𝐵 × 𝐵 ) ≼ ( ℕ × 𝐵 ) )
80 77 79 ax-mp ⊢ ( 𝐵 × 𝐵 ) ≼ ( ℕ × 𝐵 )
81 nnex ⊢ ℕ ∈ V
82 81 xpdom2 ⊢ ( 𝐵 ≼ ℕ → ( ℕ × 𝐵 ) ≼ ( ℕ × ℕ ) )
83 77 82 ax-mp ⊢ ( ℕ × 𝐵 ) ≼ ( ℕ × ℕ )
84 domtr ⊢ ( ( ( 𝐵 × 𝐵 ) ≼ ( ℕ × 𝐵 ) ∧ ( ℕ × 𝐵 ) ≼ ( ℕ × ℕ ) ) → ( 𝐵 × 𝐵 ) ≼ ( ℕ × ℕ ) )
85 80 83 84 mp2an ⊢ ( 𝐵 × 𝐵 ) ≼ ( ℕ × ℕ )
86 domentr ⊢ ( ( ( 𝐵 × 𝐵 ) ≼ ( ℕ × ℕ ) ∧ ( ℕ × ℕ ) ≈ ℕ ) → ( 𝐵 × 𝐵 ) ≼ ℕ )
87 85 56 86 mp2an ⊢ ( 𝐵 × 𝐵 ) ≼ ℕ
88 numdom ⊢ ( ( ℕ ∈ dom card ∧ ( 𝐵 × 𝐵 ) ≼ ℕ ) → ( 𝐵 × 𝐵 ) ∈ dom card )
89 52 87 88 mp2an ⊢ ( 𝐵 × 𝐵 ) ∈ dom card
90 eqid ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 × 𝑦 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 × 𝑦 ) )
91 vex ⊢ 𝑥 ∈ V
92 vex ⊢ 𝑦 ∈ V
93 91 92 xpex ⊢ ( 𝑥 × 𝑦 ) ∈ V
94 90 93 fnmpoi ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 × 𝑦 ) ) Fn ( 𝐵 × 𝐵 )
95 dffn4 ⊢ ( ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 × 𝑦 ) ) Fn ( 𝐵 × 𝐵 ) ↔ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 × 𝑦 ) ) : ( 𝐵 × 𝐵 ) –onto→ ran ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 × 𝑦 ) ) )
96 94 95 mpbi ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 × 𝑦 ) ) : ( 𝐵 × 𝐵 ) –onto→ ran ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 × 𝑦 ) )
97 fodomnum ⊢ ( ( 𝐵 × 𝐵 ) ∈ dom card → ( ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 × 𝑦 ) ) : ( 𝐵 × 𝐵 ) –onto→ ran ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 × 𝑦 ) ) → ran ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 × 𝑦 ) ) ≼ ( 𝐵 × 𝐵 ) ) )
98 89 96 97 mp2 ⊢ ran ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 × 𝑦 ) ) ≼ ( 𝐵 × 𝐵 )
99 domtr ⊢ ( ( ran ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 × 𝑦 ) ) ≼ ( 𝐵 × 𝐵 ) ∧ ( 𝐵 × 𝐵 ) ≼ ℕ ) → ran ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 × 𝑦 ) ) ≼ ℕ )
100 98 87 99 mp2an ⊢ ran ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 × 𝑦 ) ) ≼ ℕ
101 4 100 eqbrtri ⊢ 𝐾 ≼ ℕ
102 domtr ⊢ ( ( 𝑡 ≼ 𝐾 ∧ 𝐾 ≼ ℕ ) → 𝑡 ≼ ℕ )
103 47 101 102 sylancl ⊢ ( 𝑡 ⊆ 𝐾 → 𝑡 ≼ ℕ )
104 103 ad2antrl ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽 ) ∧ ( 𝑡 ⊆ 𝐾 ∧ ( ◡ 𝐺 “ 𝐴 ) = ∪ 𝑡 ) ) → 𝑡 ≼ ℕ )
105 4 eleq2i ⊢ ( 𝑤 ∈ 𝐾 ↔ 𝑤 ∈ ran ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 × 𝑦 ) ) )
106 90 93 elrnmpo ⊢ ( 𝑤 ∈ ran ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 × 𝑦 ) ) ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑤 = ( 𝑥 × 𝑦 ) )
107 105 106 bitri ⊢ ( 𝑤 ∈ 𝐾 ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑤 = ( 𝑥 × 𝑦 ) )
108 elin ⊢ ( 𝑧 ∈ ( ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∩ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑦 ) ) ↔ ( 𝑧 ∈ ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∧ 𝑧 ∈ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑦 ) ) )
109 mbff ⊢ ( 𝐹 ∈ MblFn → 𝐹 : dom 𝐹 ⟶ ℂ )
110 109 adantr ⊢ ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐹 : dom 𝐹 ⟶ ℂ )
111 fvco3 ⊢ ( ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ 𝑧 ∈ dom 𝐹 ) → ( ( ℜ ∘ 𝐹 ) ‘ 𝑧 ) = ( ℜ ‘ ( 𝐹 ‘ 𝑧 ) ) )
112 110 111 sylan ⊢ ( ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( ℜ ∘ 𝐹 ) ‘ 𝑧 ) = ( ℜ ‘ ( 𝐹 ‘ 𝑧 ) ) )
113 112 eleq1d ⊢ ( ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( ( ℜ ∘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑥 ↔ ( ℜ ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑥 ) )
114 fvco3 ⊢ ( ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ 𝑧 ∈ dom 𝐹 ) → ( ( ℑ ∘ 𝐹 ) ‘ 𝑧 ) = ( ℑ ‘ ( 𝐹 ‘ 𝑧 ) ) )
115 110 114 sylan ⊢ ( ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( ℑ ∘ 𝐹 ) ‘ 𝑧 ) = ( ℑ ‘ ( 𝐹 ‘ 𝑧 ) ) )
116 115 eleq1d ⊢ ( ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( ( ℑ ∘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑦 ↔ ( ℑ ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑦 ) )
117 113 116 anbi12d ⊢ ( ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( ( ( ℜ ∘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑥 ∧ ( ( ℑ ∘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑦 ) ↔ ( ( ℜ ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑥 ∧ ( ℑ ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑦 ) ) )
118 110 ffvelrnda ⊢ ( ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
119 fveq2 ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑧 ) → ( ℜ ‘ 𝑤 ) = ( ℜ ‘ ( 𝐹 ‘ 𝑧 ) ) )
120 fveq2 ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑧 ) → ( ℑ ‘ 𝑤 ) = ( ℑ ‘ ( 𝐹 ‘ 𝑧 ) ) )
121 119 120 opeq12d ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑧 ) → ⟨ ( ℜ ‘ 𝑤 ) , ( ℑ ‘ 𝑤 ) ⟩ = ⟨ ( ℜ ‘ ( 𝐹 ‘ 𝑧 ) ) , ( ℑ ‘ ( 𝐹 ‘ 𝑧 ) ) ⟩ )
122 2 cnrecnv ⊢ ◡ 𝐺 = ( 𝑤 ∈ ℂ ↦ ⟨ ( ℜ ‘ 𝑤 ) , ( ℑ ‘ 𝑤 ) ⟩ )
123 opex ⊢ ⟨ ( ℜ ‘ ( 𝐹 ‘ 𝑧 ) ) , ( ℑ ‘ ( 𝐹 ‘ 𝑧 ) ) ⟩ ∈ V
124 121 122 123 fvmpt ⊢ ( ( 𝐹 ‘ 𝑧 ) ∈ ℂ → ( ◡ 𝐺 ‘ ( 𝐹 ‘ 𝑧 ) ) = ⟨ ( ℜ ‘ ( 𝐹 ‘ 𝑧 ) ) , ( ℑ ‘ ( 𝐹 ‘ 𝑧 ) ) ⟩ )
125 118 124 syl ⊢ ( ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ◡ 𝐺 ‘ ( 𝐹 ‘ 𝑧 ) ) = ⟨ ( ℜ ‘ ( 𝐹 ‘ 𝑧 ) ) , ( ℑ ‘ ( 𝐹 ‘ 𝑧 ) ) ⟩ )
126 125 eleq1d ⊢ ( ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( ◡ 𝐺 ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ( 𝑥 × 𝑦 ) ↔ ⟨ ( ℜ ‘ ( 𝐹 ‘ 𝑧 ) ) , ( ℑ ‘ ( 𝐹 ‘ 𝑧 ) ) ⟩ ∈ ( 𝑥 × 𝑦 ) ) )
127 118 biantrurd ⊢ ( ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( ◡ 𝐺 ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ( 𝑥 × 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ ℂ ∧ ( ◡ 𝐺 ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ( 𝑥 × 𝑦 ) ) ) )
128 126 127 bitr3d ⊢ ( ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ⟨ ( ℜ ‘ ( 𝐹 ‘ 𝑧 ) ) , ( ℑ ‘ ( 𝐹 ‘ 𝑧 ) ) ⟩ ∈ ( 𝑥 × 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ ℂ ∧ ( ◡ 𝐺 ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ( 𝑥 × 𝑦 ) ) ) )
129 opelxp ⊢ ( ⟨ ( ℜ ‘ ( 𝐹 ‘ 𝑧 ) ) , ( ℑ ‘ ( 𝐹 ‘ 𝑧 ) ) ⟩ ∈ ( 𝑥 × 𝑦 ) ↔ ( ( ℜ ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑥 ∧ ( ℑ ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑦 ) )
130 f1ocnv ⊢ ( 𝐺 : ( ℝ × ℝ ) –1-1-onto→ ℂ → ◡ 𝐺 : ℂ –1-1-onto→ ( ℝ × ℝ ) )
131 f1ofn ⊢ ( ◡ 𝐺 : ℂ –1-1-onto→ ( ℝ × ℝ ) → ◡ 𝐺 Fn ℂ )
132 28 130 131 mp2b ⊢ ◡ 𝐺 Fn ℂ
133 elpreima ⊢ ( ◡ 𝐺 Fn ℂ → ( ( 𝐹 ‘ 𝑧 ) ∈ ( ◡ ◡ 𝐺 “ ( 𝑥 × 𝑦 ) ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ ℂ ∧ ( ◡ 𝐺 ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ( 𝑥 × 𝑦 ) ) ) )
134 132 133 ax-mp ⊢ ( ( 𝐹 ‘ 𝑧 ) ∈ ( ◡ ◡ 𝐺 “ ( 𝑥 × 𝑦 ) ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ ℂ ∧ ( ◡ 𝐺 ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ( 𝑥 × 𝑦 ) ) )
135 imacnvcnv ⊢ ( ◡ ◡ 𝐺 “ ( 𝑥 × 𝑦 ) ) = ( 𝐺 “ ( 𝑥 × 𝑦 ) )
136 135 eleq2i ⊢ ( ( 𝐹 ‘ 𝑧 ) ∈ ( ◡ ◡ 𝐺 “ ( 𝑥 × 𝑦 ) ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 “ ( 𝑥 × 𝑦 ) ) )
137 134 136 bitr3i ⊢ ( ( ( 𝐹 ‘ 𝑧 ) ∈ ℂ ∧ ( ◡ 𝐺 ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ( 𝑥 × 𝑦 ) ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 “ ( 𝑥 × 𝑦 ) ) )
138 128 129 137 3bitr3g ⊢ ( ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( ( ℜ ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑥 ∧ ( ℑ ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑦 ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 “ ( 𝑥 × 𝑦 ) ) ) )
139 117 138 bitrd ⊢ ( ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( ( ( ℜ ∘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑥 ∧ ( ( ℑ ∘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑦 ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 “ ( 𝑥 × 𝑦 ) ) ) )
140 139 pm5.32da ⊢ ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑧 ∈ dom 𝐹 ∧ ( ( ( ℜ ∘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑥 ∧ ( ( ℑ ∘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑦 ) ) ↔ ( 𝑧 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 “ ( 𝑥 × 𝑦 ) ) ) ) )
141 ref ⊢ ℜ : ℂ ⟶ ℝ
142 fco ⊢ ( ( ℜ : ℂ ⟶ ℝ ∧ 𝐹 : dom 𝐹 ⟶ ℂ ) → ( ℜ ∘ 𝐹 ) : dom 𝐹 ⟶ ℝ )
143 141 109 142 sylancr ⊢ ( 𝐹 ∈ MblFn → ( ℜ ∘ 𝐹 ) : dom 𝐹 ⟶ ℝ )
144 ffn ⊢ ( ( ℜ ∘ 𝐹 ) : dom 𝐹 ⟶ ℝ → ( ℜ ∘ 𝐹 ) Fn dom 𝐹 )
145 elpreima ⊢ ( ( ℜ ∘ 𝐹 ) Fn dom 𝐹 → ( 𝑧 ∈ ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ↔ ( 𝑧 ∈ dom 𝐹 ∧ ( ( ℜ ∘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑥 ) ) )
146 143 144 145 3syl ⊢ ( 𝐹 ∈ MblFn → ( 𝑧 ∈ ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ↔ ( 𝑧 ∈ dom 𝐹 ∧ ( ( ℜ ∘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑥 ) ) )
147 imf ⊢ ℑ : ℂ ⟶ ℝ
148 fco ⊢ ( ( ℑ : ℂ ⟶ ℝ ∧ 𝐹 : dom 𝐹 ⟶ ℂ ) → ( ℑ ∘ 𝐹 ) : dom 𝐹 ⟶ ℝ )
149 147 109 148 sylancr ⊢ ( 𝐹 ∈ MblFn → ( ℑ ∘ 𝐹 ) : dom 𝐹 ⟶ ℝ )
150 ffn ⊢ ( ( ℑ ∘ 𝐹 ) : dom 𝐹 ⟶ ℝ → ( ℑ ∘ 𝐹 ) Fn dom 𝐹 )
151 elpreima ⊢ ( ( ℑ ∘ 𝐹 ) Fn dom 𝐹 → ( 𝑧 ∈ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑦 ) ↔ ( 𝑧 ∈ dom 𝐹 ∧ ( ( ℑ ∘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑦 ) ) )
152 149 150 151 3syl ⊢ ( 𝐹 ∈ MblFn → ( 𝑧 ∈ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑦 ) ↔ ( 𝑧 ∈ dom 𝐹 ∧ ( ( ℑ ∘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑦 ) ) )
153 146 152 anbi12d ⊢ ( 𝐹 ∈ MblFn → ( ( 𝑧 ∈ ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∧ 𝑧 ∈ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑦 ) ) ↔ ( ( 𝑧 ∈ dom 𝐹 ∧ ( ( ℜ ∘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑥 ) ∧ ( 𝑧 ∈ dom 𝐹 ∧ ( ( ℑ ∘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑦 ) ) ) )
154 anandi ⊢ ( ( 𝑧 ∈ dom 𝐹 ∧ ( ( ( ℜ ∘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑥 ∧ ( ( ℑ ∘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑦 ) ) ↔ ( ( 𝑧 ∈ dom 𝐹 ∧ ( ( ℜ ∘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑥 ) ∧ ( 𝑧 ∈ dom 𝐹 ∧ ( ( ℑ ∘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑦 ) ) )
155 153 154 bitr4di ⊢ ( 𝐹 ∈ MblFn → ( ( 𝑧 ∈ ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∧ 𝑧 ∈ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑦 ) ) ↔ ( 𝑧 ∈ dom 𝐹 ∧ ( ( ( ℜ ∘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑥 ∧ ( ( ℑ ∘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑦 ) ) ) )
156 155 adantr ⊢ ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑧 ∈ ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∧ 𝑧 ∈ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑦 ) ) ↔ ( 𝑧 ∈ dom 𝐹 ∧ ( ( ( ℜ ∘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑥 ∧ ( ( ℑ ∘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑦 ) ) ) )
157 ffn ⊢ ( 𝐹 : dom 𝐹 ⟶ ℂ → 𝐹 Fn dom 𝐹 )
158 elpreima ⊢ ( 𝐹 Fn dom 𝐹 → ( 𝑧 ∈ ( ◡ 𝐹 “ ( 𝐺 “ ( 𝑥 × 𝑦 ) ) ) ↔ ( 𝑧 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 “ ( 𝑥 × 𝑦 ) ) ) ) )
159 109 157 158 3syl ⊢ ( 𝐹 ∈ MblFn → ( 𝑧 ∈ ( ◡ 𝐹 “ ( 𝐺 “ ( 𝑥 × 𝑦 ) ) ) ↔ ( 𝑧 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 “ ( 𝑥 × 𝑦 ) ) ) ) )
160 159 adantr ⊢ ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑧 ∈ ( ◡ 𝐹 “ ( 𝐺 “ ( 𝑥 × 𝑦 ) ) ) ↔ ( 𝑧 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 “ ( 𝑥 × 𝑦 ) ) ) ) )
161 140 156 160 3bitr4d ⊢ ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑧 ∈ ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∧ 𝑧 ∈ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑦 ) ) ↔ 𝑧 ∈ ( ◡ 𝐹 “ ( 𝐺 “ ( 𝑥 × 𝑦 ) ) ) ) )
162 108 161 syl5bb ⊢ ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑧 ∈ ( ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∩ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑦 ) ) ↔ 𝑧 ∈ ( ◡ 𝐹 “ ( 𝐺 “ ( 𝑥 × 𝑦 ) ) ) ) )
163 162 eqrdv ⊢ ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∩ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑦 ) ) = ( ◡ 𝐹 “ ( 𝐺 “ ( 𝑥 × 𝑦 ) ) ) )
164 ismbfcn ⊢ ( 𝐹 : dom 𝐹 ⟶ ℂ → ( 𝐹 ∈ MblFn ↔ ( ( ℜ ∘ 𝐹 ) ∈ MblFn ∧ ( ℑ ∘ 𝐹 ) ∈ MblFn ) ) )
165 109 164 syl ⊢ ( 𝐹 ∈ MblFn → ( 𝐹 ∈ MblFn ↔ ( ( ℜ ∘ 𝐹 ) ∈ MblFn ∧ ( ℑ ∘ 𝐹 ) ∈ MblFn ) ) )
166 165 ibi ⊢ ( 𝐹 ∈ MblFn → ( ( ℜ ∘ 𝐹 ) ∈ MblFn ∧ ( ℑ ∘ 𝐹 ) ∈ MblFn ) )
167 166 simpld ⊢ ( 𝐹 ∈ MblFn → ( ℜ ∘ 𝐹 ) ∈ MblFn )
168 ismbf ⊢ ( ( ℜ ∘ 𝐹 ) : dom 𝐹 ⟶ ℝ → ( ( ℜ ∘ 𝐹 ) ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) )
169 143 168 syl ⊢ ( 𝐹 ∈ MblFn → ( ( ℜ ∘ 𝐹 ) ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) )
170 167 169 mpbid ⊢ ( 𝐹 ∈ MblFn → ∀ 𝑥 ∈ ran (,) ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol )
171 170 adantr ⊢ ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ ran (,) ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol )
172 imassrn ⊢ ( (,) “ ( ℚ × ℚ ) ) ⊆ ran (,)
173 3 172 eqsstri ⊢ 𝐵 ⊆ ran (,)
174 simprl ⊢ ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
175 173 174 sselid ⊢ ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ ran (,) )
176 rsp ⊢ ( ∀ 𝑥 ∈ ran (,) ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol → ( 𝑥 ∈ ran (,) → ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) )
177 171 175 176 sylc ⊢ ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol )
178 166 simprd ⊢ ( 𝐹 ∈ MblFn → ( ℑ ∘ 𝐹 ) ∈ MblFn )
179 ismbf ⊢ ( ( ℑ ∘ 𝐹 ) : dom 𝐹 ⟶ ℝ → ( ( ℑ ∘ 𝐹 ) ∈ MblFn ↔ ∀ 𝑦 ∈ ran (,) ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑦 ) ∈ dom vol ) )
180 149 179 syl ⊢ ( 𝐹 ∈ MblFn → ( ( ℑ ∘ 𝐹 ) ∈ MblFn ↔ ∀ 𝑦 ∈ ran (,) ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑦 ) ∈ dom vol ) )
181 178 180 mpbid ⊢ ( 𝐹 ∈ MblFn → ∀ 𝑦 ∈ ran (,) ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑦 ) ∈ dom vol )
182 181 adantr ⊢ ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∀ 𝑦 ∈ ran (,) ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑦 ) ∈ dom vol )
183 simprr ⊢ ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
184 173 183 sselid ⊢ ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ ran (,) )
185 rsp ⊢ ( ∀ 𝑦 ∈ ran (,) ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑦 ) ∈ dom vol → ( 𝑦 ∈ ran (,) → ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑦 ) ∈ dom vol ) )
186 182 184 185 sylc ⊢ ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑦 ) ∈ dom vol )
187 inmbl ⊢ ( ( ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ∧ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑦 ) ∈ dom vol ) → ( ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∩ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑦 ) ) ∈ dom vol )
188 177 186 187 syl2anc ⊢ ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∩ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑦 ) ) ∈ dom vol )
189 163 188 eqeltrrd ⊢ ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ◡ 𝐹 “ ( 𝐺 “ ( 𝑥 × 𝑦 ) ) ) ∈ dom vol )
190 imaeq2 ⊢ ( 𝑤 = ( 𝑥 × 𝑦 ) → ( 𝐺 “ 𝑤 ) = ( 𝐺 “ ( 𝑥 × 𝑦 ) ) )
191 190 imaeq2d ⊢ ( 𝑤 = ( 𝑥 × 𝑦 ) → ( ◡ 𝐹 “ ( 𝐺 “ 𝑤 ) ) = ( ◡ 𝐹 “ ( 𝐺 “ ( 𝑥 × 𝑦 ) ) ) )
192 191 eleq1d ⊢ ( 𝑤 = ( 𝑥 × 𝑦 ) → ( ( ◡ 𝐹 “ ( 𝐺 “ 𝑤 ) ) ∈ dom vol ↔ ( ◡ 𝐹 “ ( 𝐺 “ ( 𝑥 × 𝑦 ) ) ) ∈ dom vol ) )
193 189 192 syl5ibrcom ⊢ ( ( 𝐹 ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑤 = ( 𝑥 × 𝑦 ) → ( ◡ 𝐹 “ ( 𝐺 “ 𝑤 ) ) ∈ dom vol ) )
194 193 rexlimdvva ⊢ ( 𝐹 ∈ MblFn → ( ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑤 = ( 𝑥 × 𝑦 ) → ( ◡ 𝐹 “ ( 𝐺 “ 𝑤 ) ) ∈ dom vol ) )
195 107 194 syl5bi ⊢ ( 𝐹 ∈ MblFn → ( 𝑤 ∈ 𝐾 → ( ◡ 𝐹 “ ( 𝐺 “ 𝑤 ) ) ∈ dom vol ) )
196 195 ralrimiv ⊢ ( 𝐹 ∈ MblFn → ∀ 𝑤 ∈ 𝐾 ( ◡ 𝐹 “ ( 𝐺 “ 𝑤 ) ) ∈ dom vol )
197 ssralv ⊢ ( 𝑡 ⊆ 𝐾 → ( ∀ 𝑤 ∈ 𝐾 ( ◡ 𝐹 “ ( 𝐺 “ 𝑤 ) ) ∈ dom vol → ∀ 𝑤 ∈ 𝑡 ( ◡ 𝐹 “ ( 𝐺 “ 𝑤 ) ) ∈ dom vol ) )
198 196 197 mpan9 ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝑡 ⊆ 𝐾 ) → ∀ 𝑤 ∈ 𝑡 ( ◡ 𝐹 “ ( 𝐺 “ 𝑤 ) ) ∈ dom vol )
199 198 ad2ant2r ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽 ) ∧ ( 𝑡 ⊆ 𝐾 ∧ ( ◡ 𝐺 “ 𝐴 ) = ∪ 𝑡 ) ) → ∀ 𝑤 ∈ 𝑡 ( ◡ 𝐹 “ ( 𝐺 “ 𝑤 ) ) ∈ dom vol )
200 iunmbl2 ⊢ ( ( 𝑡 ≼ ℕ ∧ ∀ 𝑤 ∈ 𝑡 ( ◡ 𝐹 “ ( 𝐺 “ 𝑤 ) ) ∈ dom vol ) → ∪ 𝑤 ∈ 𝑡 ( ◡ 𝐹 “ ( 𝐺 “ 𝑤 ) ) ∈ dom vol )
201 104 199 200 syl2anc ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽 ) ∧ ( 𝑡 ⊆ 𝐾 ∧ ( ◡ 𝐺 “ 𝐴 ) = ∪ 𝑡 ) ) → ∪ 𝑤 ∈ 𝑡 ( ◡ 𝐹 “ ( 𝐺 “ 𝑤 ) ) ∈ dom vol )
202 45 201 eqeltrd ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽 ) ∧ ( 𝑡 ⊆ 𝐾 ∧ ( ◡ 𝐺 “ 𝐴 ) = ∪ 𝑡 ) ) → ( ◡ 𝐹 “ 𝐴 ) ∈ dom vol )
203 27 202 exlimddv ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽 ) → ( ◡ 𝐹 “ 𝐴 ) ∈ dom vol )