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	ffvelcdmda	⊢ ( ( ( 𝐹 ∈ 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	bitrid	⊢ ( ( 𝐹 ∈ 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	biimtrid	⊢ ( 𝐹 ∈ 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 )