1stmbfm

Description: The first projection map is measurable with regard to the product sigma-algebra. (Contributed by Thierry Arnoux, 3-Jun-2017)

	Ref	Expression
Hypotheses	1stmbfm.1	$⊢ φ \to S \in ⋃ ran sigAlgebra$
	1stmbfm.2	$⊢ φ \to T \in ⋃ ran sigAlgebra$
Assertion	1stmbfm	$⊢ φ \to {1^{st} ↾}_{(⋃ S \times ⋃ T)} \in ((S \times_{s} T) {MblFn}_{μ} S)$

Proof

Step	Hyp	Ref	Expression
1		1stmbfm.1	$⊢ φ \to S \in ⋃ ran sigAlgebra$
2		1stmbfm.2	$⊢ φ \to T \in ⋃ ran sigAlgebra$
3		f1stres	$⊢ ({1^{st} ↾}_{(⋃ S \times ⋃ T)}) : ⋃ S \times ⋃ T ⟶ ⋃ S$
4		sxuni	$⊢ (S \in ⋃ ran sigAlgebra \land T \in ⋃ ran sigAlgebra) \to ⋃ S \times ⋃ T = ⋃ (S \times_{s} T)$
5	1 2 4	syl2anc	$⊢ φ \to ⋃ S \times ⋃ T = ⋃ (S \times_{s} T)$
6	5	feq2d	$⊢ φ \to (({1^{st} ↾}_{(⋃ S \times ⋃ T)}) : ⋃ S \times ⋃ T ⟶ ⋃ S \leftrightarrow ({1^{st} ↾}_{(⋃ S \times ⋃ T)}) : ⋃ (S \times_{s} T) ⟶ ⋃ S)$
7	3 6	mpbii	$⊢ φ \to ({1^{st} ↾}_{(⋃ S \times ⋃ T)}) : ⋃ (S \times_{s} T) ⟶ ⋃ S$
8		unielsiga	$⊢ S \in ⋃ ran sigAlgebra \to ⋃ S \in S$
9	1 8	syl	$⊢ φ \to ⋃ S \in S$
10		sxsiga	$⊢ (S \in ⋃ ran sigAlgebra \land T \in ⋃ ran sigAlgebra) \to S \times_{s} T \in ⋃ ran sigAlgebra$
11	1 2 10	syl2anc	$⊢ φ \to S \times_{s} T \in ⋃ ran sigAlgebra$
12		unielsiga	$⊢ S \times_{s} T \in ⋃ ran sigAlgebra \to ⋃ (S \times_{s} T) \in (S \times_{s} T)$
13	11 12	syl	$⊢ φ \to ⋃ (S \times_{s} T) \in (S \times_{s} T)$
14	9 13	elmapd	$⊢ φ \to ({1^{st} ↾}_{(⋃ S \times ⋃ T)} \in ({⋃ S}^{⋃ (S \times_{s} T)}) \leftrightarrow ({1^{st} ↾}_{(⋃ S \times ⋃ T)}) : ⋃ (S \times_{s} T) ⟶ ⋃ S)$
15	7 14	mpbird	$⊢ φ \to {1^{st} ↾}_{(⋃ S \times ⋃ T)} \in ({⋃ S}^{⋃ (S \times_{s} T)})$
16		sgon	$⊢ S \in ⋃ ran sigAlgebra \to S \in sigAlgebra (⋃ S)$
17		sigasspw	$⊢ S \in sigAlgebra (⋃ S) \to S \subseteq 𝒫 ⋃ S$
18		pwssb	$⊢ S \subseteq 𝒫 ⋃ S \leftrightarrow \forall a \in S a \subseteq ⋃ S$
19	18	biimpi	$⊢ S \subseteq 𝒫 ⋃ S \to \forall a \in S a \subseteq ⋃ S$
20	1 16 17 19	4syl	$⊢ φ \to \forall a \in S a \subseteq ⋃ S$
21	20	r19.21bi	$⊢ (φ \land a \in S) \to a \subseteq ⋃ S$
22		xpss1	$⊢ a \subseteq ⋃ S \to a \times ⋃ T \subseteq ⋃ S \times ⋃ T$
23	21 22	syl	$⊢ (φ \land a \in S) \to a \times ⋃ T \subseteq ⋃ S \times ⋃ T$
24	23	sseld	$⊢ (φ \land a \in S) \to (z \in (a \times ⋃ T) \to z \in (⋃ S \times ⋃ T))$
25	24	pm4.71rd	$⊢ (φ \land a \in S) \to (z \in (a \times ⋃ T) \leftrightarrow (z \in (⋃ S \times ⋃ T) \land z \in (a \times ⋃ T)))$
26		ffn	$⊢ ({1^{st} ↾}_{(⋃ S \times ⋃ T)}) : ⋃ S \times ⋃ T ⟶ ⋃ S \to ({1^{st} ↾}_{(⋃ S \times ⋃ T)}) Fn (⋃ S \times ⋃ T)$
27		elpreima	$⊢ ({1^{st} ↾}_{(⋃ S \times ⋃ T)}) Fn (⋃ S \times ⋃ T) \to (z \in {({1^{st} ↾}_{(⋃ S \times ⋃ T)})}^{-1} [a] \leftrightarrow (z \in (⋃ S \times ⋃ T) \land ({1^{st} ↾}_{(⋃ S \times ⋃ T)}) (z) \in a))$
28	3 26 27	mp2b	$⊢ z \in {({1^{st} ↾}_{(⋃ S \times ⋃ T)})}^{-1} [a] \leftrightarrow (z \in (⋃ S \times ⋃ T) \land ({1^{st} ↾}_{(⋃ S \times ⋃ T)}) (z) \in a)$
29		fvres	$⊢ z \in (⋃ S \times ⋃ T) \to ({1^{st} ↾}_{(⋃ S \times ⋃ T)}) (z) = 1^{st} (z)$
30	29	eleq1d	$⊢ z \in (⋃ S \times ⋃ T) \to (({1^{st} ↾}_{(⋃ S \times ⋃ T)}) (z) \in a \leftrightarrow 1^{st} (z) \in a)$
31		1st2nd2	$⊢ z \in (⋃ S \times ⋃ T) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
32		xp2nd	$⊢ z \in (⋃ S \times ⋃ T) \to 2^{nd} (z) \in ⋃ T$
33		elxp6	$⊢ z \in (a \times ⋃ T) \leftrightarrow (z = ⟨1^{st} (z), 2^{nd} (z)⟩ \land (1^{st} (z) \in a \land 2^{nd} (z) \in ⋃ T))$
34		anass	$⊢ ((z = ⟨1^{st} (z), 2^{nd} (z)⟩ \land 1^{st} (z) \in a) \land 2^{nd} (z) \in ⋃ T) \leftrightarrow (z = ⟨1^{st} (z), 2^{nd} (z)⟩ \land (1^{st} (z) \in a \land 2^{nd} (z) \in ⋃ T))$
35		an32	$⊢ ((z = ⟨1^{st} (z), 2^{nd} (z)⟩ \land 1^{st} (z) \in a) \land 2^{nd} (z) \in ⋃ T) \leftrightarrow ((z = ⟨1^{st} (z), 2^{nd} (z)⟩ \land 2^{nd} (z) \in ⋃ T) \land 1^{st} (z) \in a)$
36	33 34 35	3bitr2i	$⊢ z \in (a \times ⋃ T) \leftrightarrow ((z = ⟨1^{st} (z), 2^{nd} (z)⟩ \land 2^{nd} (z) \in ⋃ T) \land 1^{st} (z) \in a)$
37	36	baib	$⊢ (z = ⟨1^{st} (z), 2^{nd} (z)⟩ \land 2^{nd} (z) \in ⋃ T) \to (z \in (a \times ⋃ T) \leftrightarrow 1^{st} (z) \in a)$
38	31 32 37	syl2anc	$⊢ z \in (⋃ S \times ⋃ T) \to (z \in (a \times ⋃ T) \leftrightarrow 1^{st} (z) \in a)$
39	30 38	bitr4d	$⊢ z \in (⋃ S \times ⋃ T) \to (({1^{st} ↾}_{(⋃ S \times ⋃ T)}) (z) \in a \leftrightarrow z \in (a \times ⋃ T))$
40	39	pm5.32i	$⊢ (z \in (⋃ S \times ⋃ T) \land ({1^{st} ↾}_{(⋃ S \times ⋃ T)}) (z) \in a) \leftrightarrow (z \in (⋃ S \times ⋃ T) \land z \in (a \times ⋃ T))$
41	28 40	bitri	$⊢ z \in {({1^{st} ↾}_{(⋃ S \times ⋃ T)})}^{-1} [a] \leftrightarrow (z \in (⋃ S \times ⋃ T) \land z \in (a \times ⋃ T))$
42	25 41	syl6rbbr	$⊢ (φ \land a \in S) \to (z \in {({1^{st} ↾}_{(⋃ S \times ⋃ T)})}^{-1} [a] \leftrightarrow z \in (a \times ⋃ T))$
43	42	eqrdv	$⊢ (φ \land a \in S) \to {({1^{st} ↾}_{(⋃ S \times ⋃ T)})}^{-1} [a] = a \times ⋃ T$
44	1	adantr	$⊢ (φ \land a \in S) \to S \in ⋃ ran sigAlgebra$
45	2	adantr	$⊢ (φ \land a \in S) \to T \in ⋃ ran sigAlgebra$
46		simpr	$⊢ (φ \land a \in S) \to a \in S$
47		eqid	$⊢ ⋃ T = ⋃ T$
48		issgon	$⊢ T \in sigAlgebra (⋃ T) \leftrightarrow (T \in ⋃ ran sigAlgebra \land ⋃ T = ⋃ T)$
49	2 47 48	sylanblrc	$⊢ φ \to T \in sigAlgebra (⋃ T)$
50		baselsiga	$⊢ T \in sigAlgebra (⋃ T) \to ⋃ T \in T$
51	49 50	syl	$⊢ φ \to ⋃ T \in T$
52	51	adantr	$⊢ (φ \land a \in S) \to ⋃ T \in T$
53		elsx	$⊢ ((S \in ⋃ ran sigAlgebra \land T \in ⋃ ran sigAlgebra) \land (a \in S \land ⋃ T \in T)) \to a \times ⋃ T \in (S \times_{s} T)$
54	44 45 46 52 53	syl22anc	$⊢ (φ \land a \in S) \to a \times ⋃ T \in (S \times_{s} T)$
55	43 54	eqeltrd	$⊢ (φ \land a \in S) \to {({1^{st} ↾}_{(⋃ S \times ⋃ T)})}^{-1} [a] \in (S \times_{s} T)$
56	55	ralrimiva	$⊢ φ \to \forall a \in S {({1^{st} ↾}_{(⋃ S \times ⋃ T)})}^{-1} [a] \in (S \times_{s} T)$
57	11 1	ismbfm	$⊢ φ \to ({1^{st} ↾}_{(⋃ S \times ⋃ T)} \in ((S \times_{s} T) {MblFn}_{μ} S) \leftrightarrow ({1^{st} ↾}_{(⋃ S \times ⋃ T)} \in ({⋃ S}^{⋃ (S \times_{s} T)}) \land \forall a \in S {({1^{st} ↾}_{(⋃ S \times ⋃ T)})}^{-1} [a] \in (S \times_{s} T)))$
58	15 56 57	mpbir2and	$⊢ φ \to {1^{st} ↾}_{(⋃ S \times ⋃ T)} \in ((S \times_{s} T) {MblFn}_{μ} S)$

Metamath Proof Explorer

Theorem 1stmbfm

Proof