Theorem opnmblALT

Description: All open sets are measurable. This alternative proof of opnmbl is significantly shorter, at the expense of invoking countable choice ax-cc . (This was also the original proof before the current opnmbl was discovered.) (Contributed by Mario Carneiro, 17-Jun-2014) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	opnmblALT	$$⊢A\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\to A\in \mathrm{dom}vol$$

Proof

Step	Hyp	Ref	Expression
1		qtopbas	$$⊢\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\in \mathrm{TopBases}$$
2		eltg3	$$⊢\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\in \mathrm{TopBases}\to \left(A\in \mathrm{topGen}\left(\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\right)\leftrightarrow \exists x\left(x\subseteq \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\wedge A=\bigcup x\right)\right)$$
3	1 2	ax-mp	$$⊢A\in \mathrm{topGen}\left(\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\right)\leftrightarrow \exists x\left(x\subseteq \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\wedge A=\bigcup x\right)$$
4		uniiun	$$⊢\bigcup x=\bigcup _{y\in x}y$$
5		ssdomg	$$⊢\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\in \mathrm{TopBases}\to \left(x\subseteq \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\to x\preccurlyeq \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\right)$$
6	1 5	ax-mp	$$⊢x\subseteq \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\to x\preccurlyeq \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]$$
7		omelon	$$⊢\mathrm{\omega }\in \mathrm{On}$$
8		qnnen	$$⊢\mathbb{Q}\approx \mathbb{N}$$
9		xpen	$$⊢\left(\mathbb{Q}\approx \mathbb{N}\wedge \mathbb{Q}\approx \mathbb{N}\right)\to \left(\mathbb{Q}\times \mathbb{Q}\right)\approx \left(\mathbb{N}\times \mathbb{N}\right)$$
10	8 8 9	mp2an	$$⊢\left(\mathbb{Q}\times \mathbb{Q}\right)\approx \left(\mathbb{N}\times \mathbb{N}\right)$$
11		xpnnen	$$⊢\left(\mathbb{N}\times \mathbb{N}\right)\approx \mathbb{N}$$
12	10 11	entri	$$⊢\left(\mathbb{Q}\times \mathbb{Q}\right)\approx \mathbb{N}$$
13		nnenom	$$⊢\mathbb{N}\approx \mathrm{\omega }$$
14	12 13	entr2i	$$⊢\mathrm{\omega }\approx \left(\mathbb{Q}\times \mathbb{Q}\right)$$
15		isnumi	$$⊢\left(\mathrm{\omega }\in \mathrm{On}\wedge \mathrm{\omega }\approx \left(\mathbb{Q}\times \mathbb{Q}\right)\right)\to \mathbb{Q}\times \mathbb{Q}\in \mathrm{dom}\mathrm{card}$$
16	7 14 15	mp2an	$$⊢\mathbb{Q}\times \mathbb{Q}\in \mathrm{dom}\mathrm{card}$$
17		ioof	$$⊢\left(.\right):{ℝ}^{*}\times {ℝ}^{*}⟶𝒫ℝ$$
18		ffun	$$⊢\left(.\right):{ℝ}^{*}\times {ℝ}^{*}⟶𝒫ℝ\to \mathrm{Fun}\left(.\right)$$
19	17 18	ax-mp	$$⊢\mathrm{Fun}\left(.\right)$$
20		qssre	$$⊢\mathbb{Q}\subseteq ℝ$$
21		ressxr	$$⊢ℝ\subseteq {ℝ}^{*}$$
22	20 21	sstri	$$⊢\mathbb{Q}\subseteq {ℝ}^{*}$$
23		xpss12	$$⊢\left(\mathbb{Q}\subseteq {ℝ}^{*}\wedge \mathbb{Q}\subseteq {ℝ}^{*}\right)\to \mathbb{Q}\times \mathbb{Q}\subseteq {ℝ}^{*}\times {ℝ}^{*}$$
24	22 22 23	mp2an	$$⊢\mathbb{Q}\times \mathbb{Q}\subseteq {ℝ}^{*}\times {ℝ}^{*}$$
25	17	fdmi	$$⊢\mathrm{dom}\left(.\right)={ℝ}^{*}\times {ℝ}^{*}$$
26	24 25	sseqtrri	$$⊢\mathbb{Q}\times \mathbb{Q}\subseteq \mathrm{dom}\left(.\right)$$
27		fores	$$⊢\left(\mathrm{Fun}\left(.\right)\wedge \mathbb{Q}\times \mathbb{Q}\subseteq \mathrm{dom}\left(.\right)\right)\to \left({\left(.\right)\upharpoonright }_{\left(\mathbb{Q}\times \mathbb{Q}\right)}\right):\mathbb{Q}\times \mathbb{Q}\underset{onto}{⟶}\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]$$
28	19 26 27	mp2an	$$⊢\left({\left(.\right)\upharpoonright }_{\left(\mathbb{Q}\times \mathbb{Q}\right)}\right):\mathbb{Q}\times \mathbb{Q}\underset{onto}{⟶}\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]$$
29		fodomnum	$$⊢\mathbb{Q}\times \mathbb{Q}\in \mathrm{dom}\mathrm{card}\to \left(\left({\left(.\right)\upharpoonright }_{\left(\mathbb{Q}\times \mathbb{Q}\right)}\right):\mathbb{Q}\times \mathbb{Q}\underset{onto}{⟶}\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\to \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\preccurlyeq \left(\mathbb{Q}\times \mathbb{Q}\right)\right)$$
30	16 28 29	mp2	$$⊢\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\preccurlyeq \left(\mathbb{Q}\times \mathbb{Q}\right)$$
31		domentr	$$⊢\left(\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\preccurlyeq \left(\mathbb{Q}\times \mathbb{Q}\right)\wedge \left(\mathbb{Q}\times \mathbb{Q}\right)\approx \mathbb{N}\right)\to \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\preccurlyeq \mathbb{N}$$
32	30 12 31	mp2an	$$⊢\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\preccurlyeq \mathbb{N}$$
33		domtr	$$⊢\left(x\preccurlyeq \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\wedge \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\preccurlyeq \mathbb{N}\right)\to x\preccurlyeq \mathbb{N}$$
34	6 32 33	sylancl	$$⊢x\subseteq \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\to x\preccurlyeq \mathbb{N}$$
35		imassrn	$$⊢\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\subseteq \mathrm{ran}\left(.\right)$$
36		ffn	$$⊢\left(.\right):{ℝ}^{*}\times {ℝ}^{*}⟶𝒫ℝ\to \left(.\right)Fn\left({ℝ}^{*}\times {ℝ}^{*}\right)$$
37	17 36	ax-mp	$$⊢\left(.\right)Fn\left({ℝ}^{*}\times {ℝ}^{*}\right)$$
38		ioombl	$$⊢\left(x,y\right)\in \mathrm{dom}vol$$
39	38	rgen2w	$$⊢\forall x\in {ℝ}^{*}\forall y\in {ℝ}^{*}\left(x,y\right)\in \mathrm{dom}vol$$
40		ffnov	$$⊢\left(.\right):{ℝ}^{*}\times {ℝ}^{*}⟶\mathrm{dom}vol\leftrightarrow \left(\left(.\right)Fn\left({ℝ}^{*}\times {ℝ}^{*}\right)\wedge \forall x\in {ℝ}^{*}\forall y\in {ℝ}^{*}\left(x,y\right)\in \mathrm{dom}vol\right)$$
41	37 39 40	mpbir2an	$$⊢\left(.\right):{ℝ}^{*}\times {ℝ}^{*}⟶\mathrm{dom}vol$$
42		frn	$$⊢\left(.\right):{ℝ}^{*}\times {ℝ}^{*}⟶\mathrm{dom}vol\to \mathrm{ran}\left(.\right)\subseteq \mathrm{dom}vol$$
43	41 42	ax-mp	$$⊢\mathrm{ran}\left(.\right)\subseteq \mathrm{dom}vol$$
44	35 43	sstri	$$⊢\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\subseteq \mathrm{dom}vol$$
45		sstr	$$⊢\left(x\subseteq \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\wedge \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\subseteq \mathrm{dom}vol\right)\to x\subseteq \mathrm{dom}vol$$
46	44 45	mpan2	$$⊢x\subseteq \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\to x\subseteq \mathrm{dom}vol$$
47		dfss3	$$⊢x\subseteq \mathrm{dom}vol\leftrightarrow \forall y\in xy\in \mathrm{dom}vol$$
48	46 47	sylib	$$⊢x\subseteq \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\to \forall y\in xy\in \mathrm{dom}vol$$
49		iunmbl2	$$⊢\left(x\preccurlyeq \mathbb{N}\wedge \forall y\in xy\in \mathrm{dom}vol\right)\to \bigcup _{y\in x}y\in \mathrm{dom}vol$$
50	34 48 49	syl2anc	$$⊢x\subseteq \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\to \bigcup _{y\in x}y\in \mathrm{dom}vol$$
51	4 50	eqeltrid	$$⊢x\subseteq \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\to \bigcup x\in \mathrm{dom}vol$$
52		eleq1	$$⊢A=\bigcup x\to \left(A\in \mathrm{dom}vol\leftrightarrow \bigcup x\in \mathrm{dom}vol\right)$$
53	51 52	syl5ibrcom	$$⊢x\subseteq \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\to \left(A=\bigcup x\to A\in \mathrm{dom}vol\right)$$
54	53	imp	$$⊢\left(x\subseteq \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\wedge A=\bigcup x\right)\to A\in \mathrm{dom}vol$$
55	54	exlimiv	$$⊢\exists x\left(x\subseteq \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\wedge A=\bigcup x\right)\to A\in \mathrm{dom}vol$$
56	3 55	sylbi	$$⊢A\in \mathrm{topGen}\left(\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\right)\to A\in \mathrm{dom}vol$$
57		eqid	$$⊢\mathrm{topGen}\left(\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\right)=\mathrm{topGen}\left(\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\right)$$
58	57	tgqioo	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{topGen}\left(\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\right)$$
59	56 58	eleq2s	$$⊢A\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\to A\in \mathrm{dom}vol$$