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	⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra )
	1stmbfm.2	⊢ ( 𝜑 → 𝑇 ∈ ∪ ran sigAlgebra )
Assertion	2ndmbfm	⊢ ( 𝜑 → ( 2^nd ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) ∈ ( ( 𝑆 ×_s 𝑇 ) MblFnM 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		1stmbfm.1	⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra )
2		1stmbfm.2	⊢ ( 𝜑 → 𝑇 ∈ ∪ ran sigAlgebra )
3		f2ndres	⊢ ( 2^nd ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) : ( ∪ 𝑆 × ∪ 𝑇 ) ⟶ ∪ 𝑇
4		sxuni	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ( ∪ 𝑆 × ∪ 𝑇 ) = ∪ ( 𝑆 ×_s 𝑇 ) )
5	1 2 4	syl2anc	⊢ ( 𝜑 → ( ∪ 𝑆 × ∪ 𝑇 ) = ∪ ( 𝑆 ×_s 𝑇 ) )
6	5	feq2d	⊢ ( 𝜑 → ( ( 2^nd ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) : ( ∪ 𝑆 × ∪ 𝑇 ) ⟶ ∪ 𝑇 ↔ ( 2^nd ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) : ∪ ( 𝑆 ×_s 𝑇 ) ⟶ ∪ 𝑇 ) )
7	3 6	mpbii	⊢ ( 𝜑 → ( 2^nd ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) : ∪ ( 𝑆 ×_s 𝑇 ) ⟶ ∪ 𝑇 )
8		unielsiga	⊢ ( 𝑇 ∈ ∪ ran sigAlgebra → ∪ 𝑇 ∈ 𝑇 )
9	2 8	syl	⊢ ( 𝜑 → ∪ 𝑇 ∈ 𝑇 )
10		sxsiga	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ( 𝑆 ×_s 𝑇 ) ∈ ∪ ran sigAlgebra )
11	1 2 10	syl2anc	⊢ ( 𝜑 → ( 𝑆 ×_s 𝑇 ) ∈ ∪ ran sigAlgebra )
12		unielsiga	⊢ ( ( 𝑆 ×_s 𝑇 ) ∈ ∪ ran sigAlgebra → ∪ ( 𝑆 ×_s 𝑇 ) ∈ ( 𝑆 ×_s 𝑇 ) )
13	11 12	syl	⊢ ( 𝜑 → ∪ ( 𝑆 ×_s 𝑇 ) ∈ ( 𝑆 ×_s 𝑇 ) )
14	9 13	elmapd	⊢ ( 𝜑 → ( ( 2^nd ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) ∈ ( ∪ 𝑇 ↑_m ∪ ( 𝑆 ×_s 𝑇 ) ) ↔ ( 2^nd ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) : ∪ ( 𝑆 ×_s 𝑇 ) ⟶ ∪ 𝑇 ) )
15	7 14	mpbird	⊢ ( 𝜑 → ( 2^nd ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) ∈ ( ∪ 𝑇 ↑_m ∪ ( 𝑆 ×_s 𝑇 ) ) )
16		ffn	⊢ ( ( 2^nd ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) : ( ∪ 𝑆 × ∪ 𝑇 ) ⟶ ∪ 𝑇 → ( 2^nd ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) Fn ( ∪ 𝑆 × ∪ 𝑇 ) )
17		elpreima	⊢ ( ( 2^nd ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) Fn ( ∪ 𝑆 × ∪ 𝑇 ) → ( 𝑧 ∈ ( ^◡ ( 2^nd ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) “ 𝑎 ) ↔ ( 𝑧 ∈ ( ∪ 𝑆 × ∪ 𝑇 ) ∧ ( ( 2^nd ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) ‘ 𝑧 ) ∈ 𝑎 ) ) )
18	3 16 17	mp2b	⊢ ( 𝑧 ∈ ( ^◡ ( 2^nd ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) “ 𝑎 ) ↔ ( 𝑧 ∈ ( ∪ 𝑆 × ∪ 𝑇 ) ∧ ( ( 2^nd ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) ‘ 𝑧 ) ∈ 𝑎 ) )
19		fvres	⊢ ( 𝑧 ∈ ( ∪ 𝑆 × ∪ 𝑇 ) → ( ( 2^nd ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) ‘ 𝑧 ) = ( 2^nd ‘ 𝑧 ) )
20	19	eleq1d	⊢ ( 𝑧 ∈ ( ∪ 𝑆 × ∪ 𝑇 ) → ( ( ( 2^nd ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) ‘ 𝑧 ) ∈ 𝑎 ↔ ( 2^nd ‘ 𝑧 ) ∈ 𝑎 ) )
21		1st2nd2	⊢ ( 𝑧 ∈ ( ∪ 𝑆 × ∪ 𝑇 ) → 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
22		xp1st	⊢ ( 𝑧 ∈ ( ∪ 𝑆 × ∪ 𝑇 ) → ( 1^st ‘ 𝑧 ) ∈ ∪ 𝑆 )
23		elxp6	⊢ ( 𝑧 ∈ ( ∪ 𝑆 × 𝑎 ) ↔ ( 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ∧ ( ( 1^st ‘ 𝑧 ) ∈ ∪ 𝑆 ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝑎 ) ) )
24		anass	⊢ ( ( ( 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ∧ ( 1^st ‘ 𝑧 ) ∈ ∪ 𝑆 ) ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝑎 ) ↔ ( 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ∧ ( ( 1^st ‘ 𝑧 ) ∈ ∪ 𝑆 ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝑎 ) ) )
25	23 24	bitr4i	⊢ ( 𝑧 ∈ ( ∪ 𝑆 × 𝑎 ) ↔ ( ( 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ∧ ( 1^st ‘ 𝑧 ) ∈ ∪ 𝑆 ) ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝑎 ) )
26	25	baib	⊢ ( ( 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ∧ ( 1^st ‘ 𝑧 ) ∈ ∪ 𝑆 ) → ( 𝑧 ∈ ( ∪ 𝑆 × 𝑎 ) ↔ ( 2^nd ‘ 𝑧 ) ∈ 𝑎 ) )
27	21 22 26	syl2anc	⊢ ( 𝑧 ∈ ( ∪ 𝑆 × ∪ 𝑇 ) → ( 𝑧 ∈ ( ∪ 𝑆 × 𝑎 ) ↔ ( 2^nd ‘ 𝑧 ) ∈ 𝑎 ) )
28	20 27	bitr4d	⊢ ( 𝑧 ∈ ( ∪ 𝑆 × ∪ 𝑇 ) → ( ( ( 2^nd ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) ‘ 𝑧 ) ∈ 𝑎 ↔ 𝑧 ∈ ( ∪ 𝑆 × 𝑎 ) ) )
29	28	pm5.32i	⊢ ( ( 𝑧 ∈ ( ∪ 𝑆 × ∪ 𝑇 ) ∧ ( ( 2^nd ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) ‘ 𝑧 ) ∈ 𝑎 ) ↔ ( 𝑧 ∈ ( ∪ 𝑆 × ∪ 𝑇 ) ∧ 𝑧 ∈ ( ∪ 𝑆 × 𝑎 ) ) )
30	18 29	bitri	⊢ ( 𝑧 ∈ ( ^◡ ( 2^nd ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) “ 𝑎 ) ↔ ( 𝑧 ∈ ( ∪ 𝑆 × ∪ 𝑇 ) ∧ 𝑧 ∈ ( ∪ 𝑆 × 𝑎 ) ) )
31		sgon	⊢ ( 𝑇 ∈ ∪ ran sigAlgebra → 𝑇 ∈ ( sigAlgebra ‘ ∪ 𝑇 ) )
32		sigasspw	⊢ ( 𝑇 ∈ ( sigAlgebra ‘ ∪ 𝑇 ) → 𝑇 ⊆ 𝒫 ∪ 𝑇 )
33		pwssb	⊢ ( 𝑇 ⊆ 𝒫 ∪ 𝑇 ↔ ∀ 𝑎 ∈ 𝑇 𝑎 ⊆ ∪ 𝑇 )
34	33	biimpi	⊢ ( 𝑇 ⊆ 𝒫 ∪ 𝑇 → ∀ 𝑎 ∈ 𝑇 𝑎 ⊆ ∪ 𝑇 )
35	2 31 32 34	4syl	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑇 𝑎 ⊆ ∪ 𝑇 )
36	35	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝑎 ⊆ ∪ 𝑇 )
37		xpss2	⊢ ( 𝑎 ⊆ ∪ 𝑇 → ( ∪ 𝑆 × 𝑎 ) ⊆ ( ∪ 𝑆 × ∪ 𝑇 ) )
38	36 37	syl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ( ∪ 𝑆 × 𝑎 ) ⊆ ( ∪ 𝑆 × ∪ 𝑇 ) )
39	38	sseld	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ( 𝑧 ∈ ( ∪ 𝑆 × 𝑎 ) → 𝑧 ∈ ( ∪ 𝑆 × ∪ 𝑇 ) ) )
40	39	pm4.71rd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ( 𝑧 ∈ ( ∪ 𝑆 × 𝑎 ) ↔ ( 𝑧 ∈ ( ∪ 𝑆 × ∪ 𝑇 ) ∧ 𝑧 ∈ ( ∪ 𝑆 × 𝑎 ) ) ) )
41	30 40	bitr4id	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ( 𝑧 ∈ ( ^◡ ( 2^nd ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) “ 𝑎 ) ↔ 𝑧 ∈ ( ∪ 𝑆 × 𝑎 ) ) )
42	41	eqrdv	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ( ^◡ ( 2^nd ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) “ 𝑎 ) = ( ∪ 𝑆 × 𝑎 ) )
43	1	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝑆 ∈ ∪ ran sigAlgebra )
44	2	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝑇 ∈ ∪ ran sigAlgebra )
45		eqid	⊢ ∪ 𝑆 = ∪ 𝑆
46		issgon	⊢ ( 𝑆 ∈ ( sigAlgebra ‘ ∪ 𝑆 ) ↔ ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∪ 𝑆 = ∪ 𝑆 ) )
47	1 45 46	sylanblrc	⊢ ( 𝜑 → 𝑆 ∈ ( sigAlgebra ‘ ∪ 𝑆 ) )
48		baselsiga	⊢ ( 𝑆 ∈ ( sigAlgebra ‘ ∪ 𝑆 ) → ∪ 𝑆 ∈ 𝑆 )
49	47 48	syl	⊢ ( 𝜑 → ∪ 𝑆 ∈ 𝑆 )
50	49	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ∪ 𝑆 ∈ 𝑆 )
51		simpr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝑎 ∈ 𝑇 )
52		elsx	⊢ ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) ∧ ( ∪ 𝑆 ∈ 𝑆 ∧ 𝑎 ∈ 𝑇 ) ) → ( ∪ 𝑆 × 𝑎 ) ∈ ( 𝑆 ×_s 𝑇 ) )
53	43 44 50 51 52	syl22anc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ( ∪ 𝑆 × 𝑎 ) ∈ ( 𝑆 ×_s 𝑇 ) )
54	42 53	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ( ^◡ ( 2^nd ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) “ 𝑎 ) ∈ ( 𝑆 ×_s 𝑇 ) )
55	54	ralrimiva	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑇 ( ^◡ ( 2^nd ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) “ 𝑎 ) ∈ ( 𝑆 ×_s 𝑇 ) )
56	11 2	ismbfm	⊢ ( 𝜑 → ( ( 2^nd ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) ∈ ( ( 𝑆 ×_s 𝑇 ) MblFnM 𝑇 ) ↔ ( ( 2^nd ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) ∈ ( ∪ 𝑇 ↑_m ∪ ( 𝑆 ×_s 𝑇 ) ) ∧ ∀ 𝑎 ∈ 𝑇 ( ^◡ ( 2^nd ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) “ 𝑎 ) ∈ ( 𝑆 ×_s 𝑇 ) ) ) )
57	15 55 56	mpbir2and	⊢ ( 𝜑 → ( 2^nd ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) ∈ ( ( 𝑆 ×_s 𝑇 ) MblFnM 𝑇 ) )

Metamath Proof Explorer

Theorem 2ndmbfm

Proof