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		ffn	$⊢ ({1^{st} ↾}_{(⋃ S \times ⋃ T)}) : ⋃ S \times ⋃ T ⟶ ⋃ S \to ({1^{st} ↾}_{(⋃ S \times ⋃ T)}) Fn (⋃ S \times ⋃ T)$
17		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))$
18	3 16 17	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)$
19		fvres	$⊢ z \in (⋃ S \times ⋃ T) \to ({1^{st} ↾}_{(⋃ S \times ⋃ T)}) (z) = 1^{st} (z)$
20	19	eleq1d	$⊢ z \in (⋃ S \times ⋃ T) \to (({1^{st} ↾}_{(⋃ S \times ⋃ T)}) (z) \in a \leftrightarrow 1^{st} (z) \in a)$
21		1st2nd2	$⊢ z \in (⋃ S \times ⋃ T) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
22		xp2nd	$⊢ z \in (⋃ S \times ⋃ T) \to 2^{nd} (z) \in ⋃ T$
23		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))$
24		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))$
25		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)$
26	23 24 25	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)$
27	26	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)$
28	21 22 27	syl2anc	$⊢ z \in (⋃ S \times ⋃ T) \to (z \in (a \times ⋃ T) \leftrightarrow 1^{st} (z) \in a)$
29	20 28	bitr4d	$⊢ z \in (⋃ S \times ⋃ T) \to (({1^{st} ↾}_{(⋃ S \times ⋃ T)}) (z) \in a \leftrightarrow z \in (a \times ⋃ T))$
30	29	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))$
31	18 30	bitri	$⊢ z \in {({1^{st} ↾}_{(⋃ S \times ⋃ T)})}^{-1} [a] \leftrightarrow (z \in (⋃ S \times ⋃ T) \land z \in (a \times ⋃ T))$
32		sgon	$⊢ S \in ⋃ ran sigAlgebra \to S \in sigAlgebra (⋃ S)$
33		sigasspw	$⊢ S \in sigAlgebra (⋃ S) \to S \subseteq 𝒫 ⋃ S$
34		pwssb	$⊢ S \subseteq 𝒫 ⋃ S \leftrightarrow \forall a \in S a \subseteq ⋃ S$
35	34	biimpi	$⊢ S \subseteq 𝒫 ⋃ S \to \forall a \in S a \subseteq ⋃ S$
36	1 32 33 35	4syl	$⊢ φ \to \forall a \in S a \subseteq ⋃ S$
37	36	r19.21bi	$⊢ (φ \land a \in S) \to a \subseteq ⋃ S$
38		xpss1	$⊢ a \subseteq ⋃ S \to a \times ⋃ T \subseteq ⋃ S \times ⋃ T$
39	37 38	syl	$⊢ (φ \land a \in S) \to a \times ⋃ T \subseteq ⋃ S \times ⋃ T$
40	39	sseld	$⊢ (φ \land a \in S) \to (z \in (a \times ⋃ T) \to z \in (⋃ S \times ⋃ T))$
41	40	pm4.71rd	$⊢ (φ \land a \in S) \to (z \in (a \times ⋃ T) \leftrightarrow (z \in (⋃ S \times ⋃ T) \land z \in (a \times ⋃ T)))$
42	31 41	bitr4id	$⊢ (φ \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