mbfimaopnlem

	Ref	Expression
Hypotheses	mbfimaopn.1	$⊢ J = TopOpen (ℂ_{fld})$
	mbfimaopn.2	$⊢ G = (x \in ℝ, y \in ℝ ⟼ x + i y)$
	mbfimaopn.3	$⊢ B = (.) [ℚ \times ℚ]$
	mbfimaopn.4	$⊢ K = ran (x \in B, y \in B ⟼ x \times y)$
Assertion	mbfimaopnlem	$⊢ (F \in MblFn \land A \in J) \to F^{-1} [A] \in dom vol$

Proof

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

Metamath Proof Explorer

Theorem mbfimaopnlem

Proof