1stmbfm - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > 1stmbfm		Structured version Visualization version GIF version

Theorem 1stmbfm 34225

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

**Hypotheses**
Ref	Expression
1stmbfm.1	⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)
1stmbfm.2	⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)

**Assertion**
Ref	Expression
1stmbfm	⊢ (𝜑 → (1^st ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ ((𝑆 ×_s 𝑇)MblFnM𝑆))

Proof of Theorem 1stmbfm Dummy variables 𝑧 𝑎 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		f1stres 8054	. . . 4 ⊢ (1^st ↾ (∪ 𝑆 × ∪ 𝑇)):(∪ 𝑆 × ∪ 𝑇)⟶∪ 𝑆
2		1stmbfm.1	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)
3		1stmbfm.2	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)
4		sxuni 34157	. . . . . 6 ⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) → (∪ 𝑆 × ∪ 𝑇) = ∪ (𝑆 ×_s 𝑇))
5	2, 3, 4	syl2anc 583	. . . . 5 ⊢ (𝜑 → (∪ 𝑆 × ∪ 𝑇) = ∪ (𝑆 ×_s 𝑇))
6	5	feq2d 6733	. . . 4 ⊢ (𝜑 → ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)):(∪ 𝑆 × ∪ 𝑇)⟶∪ 𝑆 ↔ (1^st ↾ (∪ 𝑆 × ∪ 𝑇)):∪ (𝑆 ×_s 𝑇)⟶∪ 𝑆))
7	1, 6	mpbii 233	. . 3 ⊢ (𝜑 → (1^st ↾ (∪ 𝑆 × ∪ 𝑇)):∪ (𝑆 ×_s 𝑇)⟶∪ 𝑆)
8		unielsiga 34092	. . . . 5 ⊢ (𝑆 ∈ ∪ ran sigAlgebra → ∪ 𝑆 ∈ 𝑆)
9	2, 8	syl 17	. . . 4 ⊢ (𝜑 → ∪ 𝑆 ∈ 𝑆)
10		sxsiga 34155	. . . . . 6 ⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) → (𝑆 ×_s 𝑇) ∈ ∪ ran sigAlgebra)
11	2, 3, 10	syl2anc 583	. . . . 5 ⊢ (𝜑 → (𝑆 ×_s 𝑇) ∈ ∪ ran sigAlgebra)
12		unielsiga 34092	. . . . 5 ⊢ ((𝑆 ×_s 𝑇) ∈ ∪ ran sigAlgebra → ∪ (𝑆 ×_s 𝑇) ∈ (𝑆 ×_s 𝑇))
13	11, 12	syl 17	. . . 4 ⊢ (𝜑 → ∪ (𝑆 ×_s 𝑇) ∈ (𝑆 ×_s 𝑇))
14	9, 13	elmapd 8898	. . 3 ⊢ (𝜑 → ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ (∪ 𝑆 ↑_m ∪ (𝑆 ×_s 𝑇)) ↔ (1^st ↾ (∪ 𝑆 × ∪ 𝑇)):∪ (𝑆 ×_s 𝑇)⟶∪ 𝑆))
15	7, 14	mpbird 257	. 2 ⊢ (𝜑 → (1^st ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ (∪ 𝑆 ↑_m ∪ (𝑆 ×_s 𝑇)))
16		ffn 6747	. . . . . . . 8 ⊢ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)):(∪ 𝑆 × ∪ 𝑇)⟶∪ 𝑆 → (1^st ↾ (∪ 𝑆 × ∪ 𝑇)) Fn (∪ 𝑆 × ∪ 𝑇))
17		elpreima 7091	. . . . . . . 8 ⊢ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)) Fn (∪ 𝑆 × ∪ 𝑇) → (𝑧 ∈ (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) ∧ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎)))
18	1, 16, 17	mp2b 10	. . . . . . 7 ⊢ (𝑧 ∈ (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) ∧ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎))
19		fvres 6939	. . . . . . . . . 10 ⊢ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) → ((1^st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) = (1^st ‘𝑧))
20	19	eleq1d 2829	. . . . . . . . 9 ⊢ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) → (((1^st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎 ↔ (1^st ‘𝑧) ∈ 𝑎))
21		1st2nd2 8069	. . . . . . . . . 10 ⊢ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) → 𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)
22		xp2nd 8063	. . . . . . . . . 10 ⊢ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) → (2^nd ‘𝑧) ∈ ∪ 𝑇)
23		elxp6 8064	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∧ ((1^st ‘𝑧) ∈ 𝑎 ∧ (2^nd ‘𝑧) ∈ ∪ 𝑇)))
24		anass 468	. . . . . . . . . . . 12 ⊢ (((𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∧ (1^st ‘𝑧) ∈ 𝑎) ∧ (2^nd ‘𝑧) ∈ ∪ 𝑇) ↔ (𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∧ ((1^st ‘𝑧) ∈ 𝑎 ∧ (2^nd ‘𝑧) ∈ ∪ 𝑇)))
25		an32 645	. . . . . . . . . . . 12 ⊢ (((𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∧ (1^st ‘𝑧) ∈ 𝑎) ∧ (2^nd ‘𝑧) ∈ ∪ 𝑇) ↔ ((𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∧ (2^nd ‘𝑧) ∈ ∪ 𝑇) ∧ (1^st ‘𝑧) ∈ 𝑎))
26	23, 24, 25	3bitr2i 299	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ ((𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∧ (2^nd ‘𝑧) ∈ ∪ 𝑇) ∧ (1^st ‘𝑧) ∈ 𝑎))
27	26	baib 535	. . . . . . . . . 10 ⊢ ((𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∧ (2^nd ‘𝑧) ∈ ∪ 𝑇) → (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (1^st ‘𝑧) ∈ 𝑎))
28	21, 22, 27	syl2anc 583	. . . . . . . . 9 ⊢ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) → (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (1^st ‘𝑧) ∈ 𝑎))
29	20, 28	bitr4d 282	. . . . . . . 8 ⊢ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) → (((1^st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎 ↔ 𝑧 ∈ (𝑎 × ∪ 𝑇)))
30	29	pm5.32i 574	. . . . . . 7 ⊢ ((𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) ∧ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) ∧ 𝑧 ∈ (𝑎 × ∪ 𝑇)))
31	18, 30	bitri 275	. . . . . 6 ⊢ (𝑧 ∈ (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) ∧ 𝑧 ∈ (𝑎 × ∪ 𝑇)))
32		sgon 34088	. . . . . . . . . . 11 ⊢ (𝑆 ∈ ∪ ran sigAlgebra → 𝑆 ∈ (sigAlgebra‘∪ 𝑆))
33		sigasspw 34080	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (sigAlgebra‘∪ 𝑆) → 𝑆 ⊆ 𝒫 ∪ 𝑆)
34		pwssb 5124	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ 𝒫 ∪ 𝑆 ↔ ∀𝑎 ∈ 𝑆 𝑎 ⊆ ∪ 𝑆)
35	34	biimpi 216	. . . . . . . . . . 11 ⊢ (𝑆 ⊆ 𝒫 ∪ 𝑆 → ∀𝑎 ∈ 𝑆 𝑎 ⊆ ∪ 𝑆)
36	2, 32, 33, 35	4syl 19	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑎 ∈ 𝑆 𝑎 ⊆ ∪ 𝑆)
37	36	r19.21bi 3257	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ⊆ ∪ 𝑆)
38		xpss1 5719	. . . . . . . . 9 ⊢ (𝑎 ⊆ ∪ 𝑆 → (𝑎 × ∪ 𝑇) ⊆ (∪ 𝑆 × ∪ 𝑇))
39	37, 38	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 × ∪ 𝑇) ⊆ (∪ 𝑆 × ∪ 𝑇))
40	39	sseld 4007	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑧 ∈ (𝑎 × ∪ 𝑇) → 𝑧 ∈ (∪ 𝑆 × ∪ 𝑇)))
41	40	pm4.71rd 562	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) ∧ 𝑧 ∈ (𝑎 × ∪ 𝑇))))
42	31, 41	bitr4id 290	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑧 ∈ (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ↔ 𝑧 ∈ (𝑎 × ∪ 𝑇)))
43	42	eqrdv 2738	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) = (𝑎 × ∪ 𝑇))
44	2	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑆 ∈ ∪ ran sigAlgebra)
45	3	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑇 ∈ ∪ ran sigAlgebra)
46		simpr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ 𝑆)
47		eqid 2740	. . . . . . . 8 ⊢ ∪ 𝑇 = ∪ 𝑇
48		issgon 34087	. . . . . . . 8 ⊢ (𝑇 ∈ (sigAlgebra‘∪ 𝑇) ↔ (𝑇 ∈ ∪ ran sigAlgebra ∧ ∪ 𝑇 = ∪ 𝑇))
49	3, 47, 48	sylanblrc 589	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ (sigAlgebra‘∪ 𝑇))
50		baselsiga 34079	. . . . . . 7 ⊢ (𝑇 ∈ (sigAlgebra‘∪ 𝑇) → ∪ 𝑇 ∈ 𝑇)
51	49, 50	syl 17	. . . . . 6 ⊢ (𝜑 → ∪ 𝑇 ∈ 𝑇)
52	51	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ∪ 𝑇 ∈ 𝑇)
53		elsx 34158	. . . . 5 ⊢ (((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) ∧ (𝑎 ∈ 𝑆 ∧ ∪ 𝑇 ∈ 𝑇)) → (𝑎 × ∪ 𝑇) ∈ (𝑆 ×_s 𝑇))
54	44, 45, 46, 52, 53	syl22anc 838	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 × ∪ 𝑇) ∈ (𝑆 ×_s 𝑇))
55	43, 54	eqeltrd 2844	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ∈ (𝑆 ×_s 𝑇))
56	55	ralrimiva 3152	. 2 ⊢ (𝜑 → ∀𝑎 ∈ 𝑆 (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ∈ (𝑆 ×_s 𝑇))
57	11, 2	ismbfm 34215	. 2 ⊢ (𝜑 → ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ ((𝑆 ×_s 𝑇)MblFnM𝑆) ↔ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ (∪ 𝑆 ↑_m ∪ (𝑆 ×_s 𝑇)) ∧ ∀𝑎 ∈ 𝑆 (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ∈ (𝑆 ×_s 𝑇))))
58	15, 56, 57	mpbir2and 712	1 ⊢ (𝜑 → (1^st ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ ((𝑆 ×_s 𝑇)MblFnM𝑆))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1537 ∈ wcel 2108 ∀wral 3067 ⊆ wss 3976 𝒫 cpw 4622 ⟨cop 4654 ∪ cuni 4931 × cxp 5698 ^◡ccnv 5699 ran crn 5701 ↾ cres 5702 “ cima 5703 Fn wfn 6568 ⟶wf 6569 ‘cfv 6573 (class class class)co 7448 1^st c1st 8028 2^nd c2nd 8029 ↑_m cmap 8884 sigAlgebracsiga 34072 ×_s csx 34152 MblFnMcmbfm 34213

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-ral 3068 df-rex 3077 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-int 4971 df-iun 5017 df-br 5167 df-opab 5229 df-mpt 5250 df-id 5593 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-ov 7451 df-oprab 7452 df-mpo 7453 df-1st 8030 df-2nd 8031 df-map 8886 df-siga 34073 df-sigagen 34103 df-sx 34153 df-mbfm 34214

This theorem is referenced by: (None)

W3C validator