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 34620

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 8013	. . . 4 ⊢ (1^st ↾ (∪ 𝑆 × ∪ 𝑇)):(∪ 𝑆 × ∪ 𝑇)⟶∪ 𝑆
2		1stmbfm.1	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)
3		1stmbfm.2	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)
4		sxuni 34553	. . . . . 6 ⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) → (∪ 𝑆 × ∪ 𝑇) = ∪ (𝑆 ×_s 𝑇))
5	2, 3, 4	syl2anc 595	. . . . 5 ⊢ (𝜑 → (∪ 𝑆 × ∪ 𝑇) = ∪ (𝑆 ×_s 𝑇))
6	5	feq2d 6693	. . . 4 ⊢ (𝜑 → ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)):(∪ 𝑆 × ∪ 𝑇)⟶∪ 𝑆 ↔ (1^st ↾ (∪ 𝑆 × ∪ 𝑇)):∪ (𝑆 ×_s 𝑇)⟶∪ 𝑆))
7	1, 6	mpbii 236	. . 3 ⊢ (𝜑 → (1^st ↾ (∪ 𝑆 × ∪ 𝑇)):∪ (𝑆 ×_s 𝑇)⟶∪ 𝑆)
8		unielsiga 34488	. . . . 5 ⊢ (𝑆 ∈ ∪ ran sigAlgebra → ∪ 𝑆 ∈ 𝑆)
9	2, 8	syl 18	. . . 4 ⊢ (𝜑 → ∪ 𝑆 ∈ 𝑆)
10		sxsiga 34551	. . . . . 6 ⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) → (𝑆 ×_s 𝑇) ∈ ∪ ran sigAlgebra)
11	2, 3, 10	syl2anc 595	. . . . 5 ⊢ (𝜑 → (𝑆 ×_s 𝑇) ∈ ∪ ran sigAlgebra)
12		unielsiga 34488	. . . . 5 ⊢ ((𝑆 ×_s 𝑇) ∈ ∪ ran sigAlgebra → ∪ (𝑆 ×_s 𝑇) ∈ (𝑆 ×_s 𝑇))
13	11, 12	syl 18	. . . 4 ⊢ (𝜑 → ∪ (𝑆 ×_s 𝑇) ∈ (𝑆 ×_s 𝑇))
14	9, 13	elmapd 8840	. . 3 ⊢ (𝜑 → ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ (∪ 𝑆 ↑_m ∪ (𝑆 ×_s 𝑇)) ↔ (1^st ↾ (∪ 𝑆 × ∪ 𝑇)):∪ (𝑆 ×_s 𝑇)⟶∪ 𝑆))
15	7, 14	mpbird 260	. 2 ⊢ (𝜑 → (1^st ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ (∪ 𝑆 ↑_m ∪ (𝑆 ×_s 𝑇)))
16		ffn 6709	. . . . . . . 8 ⊢ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)):(∪ 𝑆 × ∪ 𝑇)⟶∪ 𝑆 → (1^st ↾ (∪ 𝑆 × ∪ 𝑇)) Fn (∪ 𝑆 × ∪ 𝑇))
17		elpreima 7057	. . . . . . . 8 ⊢ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)) Fn (∪ 𝑆 × ∪ 𝑇) → (𝑧 ∈ (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) ∧ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎)))
18	1, 16, 17	mp2b 10	. . . . . . 7 ⊢ (𝑧 ∈ (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) ∧ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎))
19		fvres 6904	. . . . . . . . . 10 ⊢ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) → ((1^st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) = (1^st ‘𝑧))
20	19	eleq1d 2855	. . . . . . . . 9 ⊢ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) → (((1^st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎 ↔ (1^st ‘𝑧) ∈ 𝑎))
21		1st2nd2 8028	. . . . . . . . . 10 ⊢ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) → 𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)
22		xp2nd 8022	. . . . . . . . . 10 ⊢ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) → (2^nd ‘𝑧) ∈ ∪ 𝑇)
23		elxp6 8023	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∧ ((1^st ‘𝑧) ∈ 𝑎 ∧ (2^nd ‘𝑧) ∈ ∪ 𝑇)))
24		anass 473	. . . . . . . . . . . 12 ⊢ (((𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∧ (1^st ‘𝑧) ∈ 𝑎) ∧ (2^nd ‘𝑧) ∈ ∪ 𝑇) ↔ (𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∧ ((1^st ‘𝑧) ∈ 𝑎 ∧ (2^nd ‘𝑧) ∈ ∪ 𝑇)))
25		an32 658	. . . . . . . . . . . 12 ⊢ (((𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∧ (1^st ‘𝑧) ∈ 𝑎) ∧ (2^nd ‘𝑧) ∈ ∪ 𝑇) ↔ ((𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∧ (2^nd ‘𝑧) ∈ ∪ 𝑇) ∧ (1^st ‘𝑧) ∈ 𝑎))
26	23, 24, 25	3bitr2i 302	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ ((𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∧ (2^nd ‘𝑧) ∈ ∪ 𝑇) ∧ (1^st ‘𝑧) ∈ 𝑎))
27	26	baib 544	. . . . . . . . . 10 ⊢ ((𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∧ (2^nd ‘𝑧) ∈ ∪ 𝑇) → (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (1^st ‘𝑧) ∈ 𝑎))
28	21, 22, 27	syl2anc 595	. . . . . . . . 9 ⊢ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) → (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (1^st ‘𝑧) ∈ 𝑎))
29	20, 28	bitr4d 285	. . . . . . . 8 ⊢ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) → (((1^st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎 ↔ 𝑧 ∈ (𝑎 × ∪ 𝑇)))
30	29	pm5.32i 584	. . . . . . 7 ⊢ ((𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) ∧ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) ∧ 𝑧 ∈ (𝑎 × ∪ 𝑇)))
31	18, 30	bitri 278	. . . . . 6 ⊢ (𝑧 ∈ (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) ∧ 𝑧 ∈ (𝑎 × ∪ 𝑇)))
32		sgon 34484	. . . . . . . . . . 11 ⊢ (𝑆 ∈ ∪ ran sigAlgebra → 𝑆 ∈ (sigAlgebra‘∪ 𝑆))
33		sigasspw 34476	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (sigAlgebra‘∪ 𝑆) → 𝑆 ⊆ 𝒫 ∪ 𝑆)
34		pwssb 5072	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ 𝒫 ∪ 𝑆 ↔ ∀𝑎 ∈ 𝑆 𝑎 ⊆ ∪ 𝑆)
35	34	biimpi 219	. . . . . . . . . . 11 ⊢ (𝑆 ⊆ 𝒫 ∪ 𝑆 → ∀𝑎 ∈ 𝑆 𝑎 ⊆ ∪ 𝑆)
36	2, 32, 33, 35	4syl 20	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑎 ∈ 𝑆 𝑎 ⊆ ∪ 𝑆)
37	36	r19.21bi 3264	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ⊆ ∪ 𝑆)
38		xpss1 5684	. . . . . . . . 9 ⊢ (𝑎 ⊆ ∪ 𝑆 → (𝑎 × ∪ 𝑇) ⊆ (∪ 𝑆 × ∪ 𝑇))
39	37, 38	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 × ∪ 𝑇) ⊆ (∪ 𝑆 × ∪ 𝑇))
40	39	sseld 3944	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑧 ∈ (𝑎 × ∪ 𝑇) → 𝑧 ∈ (∪ 𝑆 × ∪ 𝑇)))
41	40	pm4.71rd 571	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) ∧ 𝑧 ∈ (𝑎 × ∪ 𝑇))))
42	31, 41	bitr4id 293	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑧 ∈ (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ↔ 𝑧 ∈ (𝑎 × ∪ 𝑇)))
43	42	eqrdv 2768	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) = (𝑎 × ∪ 𝑇))
44	2	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑆 ∈ ∪ ran sigAlgebra)
45	3	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑇 ∈ ∪ ran sigAlgebra)
46		simpr 489	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ 𝑆)
47		eqid 2770	. . . . . . . 8 ⊢ ∪ 𝑇 = ∪ 𝑇
48		issgon 34483	. . . . . . . 8 ⊢ (𝑇 ∈ (sigAlgebra‘∪ 𝑇) ↔ (𝑇 ∈ ∪ ran sigAlgebra ∧ ∪ 𝑇 = ∪ 𝑇))
49	3, 47, 48	sylanblrc 601	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ (sigAlgebra‘∪ 𝑇))
50		baselsiga 34475	. . . . . . 7 ⊢ (𝑇 ∈ (sigAlgebra‘∪ 𝑇) → ∪ 𝑇 ∈ 𝑇)
51	49, 50	syl 18	. . . . . 6 ⊢ (𝜑 → ∪ 𝑇 ∈ 𝑇)
52	51	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ∪ 𝑇 ∈ 𝑇)
53		elsx 34554	. . . . 5 ⊢ (((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) ∧ (𝑎 ∈ 𝑆 ∧ ∪ 𝑇 ∈ 𝑇)) → (𝑎 × ∪ 𝑇) ∈ (𝑆 ×_s 𝑇))
54	44, 45, 46, 52, 53	syl22anc 851	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 × ∪ 𝑇) ∈ (𝑆 ×_s 𝑇))
55	43, 54	eqeltrd 2870	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ∈ (𝑆 ×_s 𝑇))
56	55	ralrimiva 3164	. 2 ⊢ (𝜑 → ∀𝑎 ∈ 𝑆 (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ∈ (𝑆 ×_s 𝑇))
57	11, 2	ismbfm 34611	. 2 ⊢ (𝜑 → ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ ((𝑆 ×_s 𝑇)MblFnM𝑆) ↔ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ (∪ 𝑆 ↑_m ∪ (𝑆 ×_s 𝑇)) ∧ ∀𝑎 ∈ 𝑆 (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ∈ (𝑆 ×_s 𝑇))))
58	15, 56, 57	mpbir2and 725	1 ⊢ (𝜑 → (1^st ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ ((𝑆 ×_s 𝑇)MblFnM𝑆))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1568 ∈ wcel 2150 ∀wral 3086 ⊆ wss 3913 𝒫 cpw 4567 ⟨cop 4600 ∪ cuni 4877 × cxp 5663 ^◡ccnv 5664 ran crn 5666 ↾ cres 5667 “ cima 5668 Fn wfn 6535 ⟶wf 6536 ‘cfv 6540 (class class class)co 7414 1^st c1st 7987 2^nd c2nd 7988 ↑_m cmap 8827 sigAlgebracsiga 34468 ×_s csx 34548 MblFnMcmbfm 34609

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1823 ax-4 1837 ax-5 1938 ax-6 1995 ax-7 2036 ax-8 2152 ax-9 2160 ax-10 2183 ax-11 2199 ax-12 2220 ax-ext 2742 ax-rep 5243 ax-sep 5262 ax-nul 5274 ax-pow 5340 ax-pr 5408 ax-un 7736

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1571 df-fal 1581 df-ex 1808 df-nf 1812 df-sb 2099 df-mo 2574 df-eu 2604 df-clab 2749 df-cleq 2762 df-clel 2845 df-nfc 2919 df-ne 2966 df-ral 3087 df-rex 3097 df-reu 3377 df-rab 3424 df-v 3464 df-sbc 3753 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-int 4918 df-iun 4963 df-br 5115 df-opab 5179 df-mpt 5198 df-id 5560 df-xp 5671 df-rel 5672 df-cnv 5673 df-co 5674 df-dm 5675 df-rn 5676 df-res 5677 df-ima 5678 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-ov 7417 df-oprab 7418 df-mpo 7419 df-1st 7989 df-2nd 7990 df-map 8829 df-siga 34469 df-sigagen 34499 df-sx 34549 df-mbfm 34610

This theorem is referenced by: (None)

W3C validator