2ndmbfm

Description: The second 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	2ndmbfm	$⊢ φ \to {2^{nd} ↾}_{(⋃ S \times ⋃ T)} \in ((S \times_{s} T) {MblFn}_{μ} T)$

Proof

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

Metamath Proof Explorer

Theorem 2ndmbfm

Proof