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

Proof

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

Metamath Proof Explorer

Theorem 1stmbfm

Proof