mbfmco2

Description: The pair building of two measurable functions is measurable. ( cf. cnmpt1t ). (Contributed by Thierry Arnoux, 6-Jun-2017)

	Ref	Expression
Hypotheses	mbfmco.1	$⊢ φ \to R \in ⋃ ran sigAlgebra$
	mbfmco.2	$⊢ φ \to S \in ⋃ ran sigAlgebra$
	mbfmco.3	$⊢ φ \to T \in ⋃ ran sigAlgebra$
	mbfmco2.4	$⊢ φ \to F \in (R {MblFn}_{μ} S)$
	mbfmco2.5	$⊢ φ \to G \in (R {MblFn}_{μ} T)$
	mbfmco2.6	$⊢ H = (x \in ⋃ R ⟼ ⟨F (x), G (x)⟩)$
Assertion	mbfmco2	$⊢ φ \to H \in (R {MblFn}_{μ} (S \times_{s} T))$

Proof

Step	Hyp	Ref	Expression
1		mbfmco.1	$⊢ φ \to R \in ⋃ ran sigAlgebra$
2		mbfmco.2	$⊢ φ \to S \in ⋃ ran sigAlgebra$
3		mbfmco.3	$⊢ φ \to T \in ⋃ ran sigAlgebra$
4		mbfmco2.4	$⊢ φ \to F \in (R {MblFn}_{μ} S)$
5		mbfmco2.5	$⊢ φ \to G \in (R {MblFn}_{μ} T)$
6		mbfmco2.6	$⊢ H = (x \in ⋃ R ⟼ ⟨F (x), G (x)⟩)$
7	1 2 4	mbfmf	$⊢ φ \to F : ⋃ R ⟶ ⋃ S$
8	7	ffvelrnda	$⊢ (φ \land x \in ⋃ R) \to F (x) \in ⋃ S$
9	1 3 5	mbfmf	$⊢ φ \to G : ⋃ R ⟶ ⋃ T$
10	9	ffvelrnda	$⊢ (φ \land x \in ⋃ R) \to G (x) \in ⋃ T$
11		opelxpi	$⊢ (F (x) \in ⋃ S \land G (x) \in ⋃ T) \to ⟨F (x), G (x)⟩ \in (⋃ S \times ⋃ T)$
12	8 10 11	syl2anc	$⊢ (φ \land x \in ⋃ R) \to ⟨F (x), G (x)⟩ \in (⋃ S \times ⋃ T)$
13		sxuni	$⊢ (S \in ⋃ ran sigAlgebra \land T \in ⋃ ran sigAlgebra) \to ⋃ S \times ⋃ T = ⋃ (S \times_{s} T)$
14	2 3 13	syl2anc	$⊢ φ \to ⋃ S \times ⋃ T = ⋃ (S \times_{s} T)$
15	14	adantr	$⊢ (φ \land x \in ⋃ R) \to ⋃ S \times ⋃ T = ⋃ (S \times_{s} T)$
16	12 15	eleqtrd	$⊢ (φ \land x \in ⋃ R) \to ⟨F (x), G (x)⟩ \in ⋃ (S \times_{s} T)$
17	16 6	fmptd	$⊢ φ \to H : ⋃ R ⟶ ⋃ (S \times_{s} T)$
18		eqid	$⊢ (a \in S, b \in T ⟼ a \times b) = (a \in S, b \in T ⟼ a \times b)$
19		vex	$⊢ a \in V$
20		vex	$⊢ b \in V$
21	19 20	xpex	$⊢ a \times b \in V$
22	18 21	elrnmpo	$⊢ c \in ran (a \in S, b \in T ⟼ a \times b) \leftrightarrow \exists a \in S \exists b \in T c = a \times b$
23		simp3	$⊢ (φ \land (a \in S \land b \in T) \land c = a \times b) \to c = a \times b$
24	23	imaeq2d	$⊢ (φ \land (a \in S \land b \in T) \land c = a \times b) \to H^{-1} [c] = H^{-1} [a \times b]$
25		simp1	$⊢ (φ \land (a \in S \land b \in T) \land c = a \times b) \to φ$
26		simp2l	$⊢ (φ \land (a \in S \land b \in T) \land c = a \times b) \to a \in S$
27		simp2r	$⊢ (φ \land (a \in S \land b \in T) \land c = a \times b) \to b \in T$
28	7 9 6	xppreima2	$⊢ φ \to H^{-1} [a \times b] = F^{-1} [a] \cap G^{-1} [b]$
29	28	3ad2ant1	$⊢ (φ \land a \in S \land b \in T) \to H^{-1} [a \times b] = F^{-1} [a] \cap G^{-1} [b]$
30	1	3ad2ant1	$⊢ (φ \land a \in S \land b \in T) \to R \in ⋃ ran sigAlgebra$
31	2	3ad2ant1	$⊢ (φ \land a \in S \land b \in T) \to S \in ⋃ ran sigAlgebra$
32	4	3ad2ant1	$⊢ (φ \land a \in S \land b \in T) \to F \in (R {MblFn}_{μ} S)$
33		simp2	$⊢ (φ \land a \in S \land b \in T) \to a \in S$
34	30 31 32 33	mbfmcnvima	$⊢ (φ \land a \in S \land b \in T) \to F^{-1} [a] \in R$
35	3	3ad2ant1	$⊢ (φ \land a \in S \land b \in T) \to T \in ⋃ ran sigAlgebra$
36	5	3ad2ant1	$⊢ (φ \land a \in S \land b \in T) \to G \in (R {MblFn}_{μ} T)$
37		simp3	$⊢ (φ \land a \in S \land b \in T) \to b \in T$
38	30 35 36 37	mbfmcnvima	$⊢ (φ \land a \in S \land b \in T) \to G^{-1} [b] \in R$
39		inelsiga	$⊢ (R \in ⋃ ran sigAlgebra \land F^{-1} [a] \in R \land G^{-1} [b] \in R) \to F^{-1} [a] \cap G^{-1} [b] \in R$
40	30 34 38 39	syl3anc	$⊢ (φ \land a \in S \land b \in T) \to F^{-1} [a] \cap G^{-1} [b] \in R$
41	29 40	eqeltrd	$⊢ (φ \land a \in S \land b \in T) \to H^{-1} [a \times b] \in R$
42	25 26 27 41	syl3anc	$⊢ (φ \land (a \in S \land b \in T) \land c = a \times b) \to H^{-1} [a \times b] \in R$
43	24 42	eqeltrd	$⊢ (φ \land (a \in S \land b \in T) \land c = a \times b) \to H^{-1} [c] \in R$
44	43	3expia	$⊢ (φ \land (a \in S \land b \in T)) \to (c = a \times b \to H^{-1} [c] \in R)$
45	44	rexlimdvva	$⊢ φ \to (\exists a \in S \exists b \in T c = a \times b \to H^{-1} [c] \in R)$
46	45	imp	$⊢ (φ \land \exists a \in S \exists b \in T c = a \times b) \to H^{-1} [c] \in R$
47	22 46	sylan2b	$⊢ (φ \land c \in ran (a \in S, b \in T ⟼ a \times b)) \to H^{-1} [c] \in R$
48	47	ralrimiva	$⊢ φ \to \forall c \in ran (a \in S, b \in T ⟼ a \times b) H^{-1} [c] \in R$
49		eqid	$⊢ ran (a \in S, b \in T ⟼ a \times b) = ran (a \in S, b \in T ⟼ a \times b)$
50	49	txbasex	$⊢ (S \in ⋃ ran sigAlgebra \land T \in ⋃ ran sigAlgebra) \to ran (a \in S, b \in T ⟼ a \times b) \in V$
51	2 3 50	syl2anc	$⊢ φ \to ran (a \in S, b \in T ⟼ a \times b) \in V$
52	49	sxval	$⊢ (S \in ⋃ ran sigAlgebra \land T \in ⋃ ran sigAlgebra) \to S \times_{s} T = 𝛔 (ran (a \in S, b \in T ⟼ a \times b))$
53	2 3 52	syl2anc	$⊢ φ \to S \times_{s} T = 𝛔 (ran (a \in S, b \in T ⟼ a \times b))$
54	51 1 53	imambfm	$⊢ φ \to (H \in (R {MblFn}_{μ} (S \times_{s} T)) \leftrightarrow (H : ⋃ R ⟶ ⋃ (S \times_{s} T) \land \forall c \in ran (a \in S, b \in T ⟼ a \times b) H^{-1} [c] \in R))$
55	17 48 54	mpbir2and	$⊢ φ \to H \in (R {MblFn}_{μ} (S \times_{s} T))$

Metamath Proof Explorer

Theorem mbfmco2

Proof