# Metamath Proof Explorer

## Theorem 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 ${⊢}{\phi }\to {S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
1stmbfm.2 ${⊢}{\phi }\to {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
Assertion 2ndmbfm ${⊢}{\phi }\to {{2}^{nd}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\in \left(\left({S}{×}_{s}{T}\right){\mathrm{MblFn}}_{\mu }{T}\right)$

### Proof

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