cnambfre

Description: A real-valued, a.e. continuous function is measurable. (Contributed by Brendan Leahy, 4-Apr-2018)

		Ref	Expression
	Assertion	cnambfre	$⊢ (F : A ⟶ ℝ \land A \in dom vol \land {vol}^{*} (A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}]) = 0) \to F \in MblFn$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ F : A ⟶ ℝ \to F : A ⟶ ℝ$
2	1	feqmptd	$⊢ F : A ⟶ ℝ \to F = (x \in A ⟼ F (x))$
3	2	cnveqd	$⊢ F : A ⟶ ℝ \to F^{-1} = {(x \in A ⟼ F (x))}^{-1}$
4	3	imaeq1d	$⊢ F : A ⟶ ℝ \to F^{-1} [b] = {(x \in A ⟼ F (x))}^{-1} [b]$
5	4	ad2antrr	$⊢ ((F : A ⟶ ℝ \land A \in dom vol) \land b \in ran (.)) \to F^{-1} [b] = {(x \in A ⟼ F (x))}^{-1} [b]$
6		exmid	$⊢ (F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \lor \neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x))$
7	6	biantrur	$⊢ F (x) \in b \leftrightarrow ((F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \lor \neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)) \land F (x) \in b)$
8		andir	$⊢ ((F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \lor \neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)) \land F (x) \in b) \leftrightarrow ((F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b) \lor (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b))$
9	7 8	bitri	$⊢ F (x) \in b \leftrightarrow ((F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b) \lor (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b))$
10		retopbas	$⊢ ran (.) \in TopBases$
11		bastg	$⊢ ran (.) \in TopBases \to ran (.) \subseteq topGen (ran (.))$
12	10 11	ax-mp	$⊢ ran (.) \subseteq topGen (ran (.))$
13	12	sseli	$⊢ b \in ran (.) \to b \in topGen (ran (.))$
14	13	ad2antlr	$⊢ (((F : A ⟶ ℝ \land A \in dom vol) \land b \in ran (.)) \land x \in A) \to b \in topGen (ran (.))$
15		cnpimaex	$⊢ (F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land b \in topGen (ran (.)) \land F (x) \in b) \to \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (x \in y \land F [y] \subseteq b)$
16	15	3com12	$⊢ (b \in topGen (ran (.)) \land F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b) \to \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (x \in y \land F [y] \subseteq b)$
17	16	3expa	$⊢ ((b \in topGen (ran (.)) \land F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)) \land F (x) \in b) \to \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (x \in y \land F [y] \subseteq b)$
18	14 17	sylanl1	$⊢ (((((F : A ⟶ ℝ \land A \in dom vol) \land b \in ran (.)) \land x \in A) \land F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)) \land F (x) \in b) \to \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (x \in y \land F [y] \subseteq b)$
19	18	ex	$⊢ ((((F : A ⟶ ℝ \land A \in dom vol) \land b \in ran (.)) \land x \in A) \land F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)) \to (F (x) \in b \to \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (x \in y \land F [y] \subseteq b))$
20		simprrr	$⊢ ((F : A ⟶ ℝ \land A \in dom vol) \land (y \in (topGen (ran (.)) ↾_{𝑡} A) \land (x \in y \land F [y] \subseteq b))) \to F [y] \subseteq b$
21		ffn	$⊢ F : A ⟶ ℝ \to F Fn A$
22	21	adantr	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to F Fn A$
23		restsspw	$⊢ topGen (ran (.)) ↾_{𝑡} A \subseteq 𝒫 A$
24	23	sseli	$⊢ y \in (topGen (ran (.)) ↾_{𝑡} A) \to y \in 𝒫 A$
25	24	elpwid	$⊢ y \in (topGen (ran (.)) ↾_{𝑡} A) \to y \subseteq A$
26		simpl	$⊢ (x \in y \land F [y] \subseteq b) \to x \in y$
27		fnfvima	$⊢ (F Fn A \land y \subseteq A \land x \in y) \to F (x) \in F [y]$
28	22 25 26 27	syl3an	$⊢ ((F : A ⟶ ℝ \land A \in dom vol) \land y \in (topGen (ran (.)) ↾_{𝑡} A) \land (x \in y \land F [y] \subseteq b)) \to F (x) \in F [y]$
29	28	3expb	$⊢ ((F : A ⟶ ℝ \land A \in dom vol) \land (y \in (topGen (ran (.)) ↾_{𝑡} A) \land (x \in y \land F [y] \subseteq b))) \to F (x) \in F [y]$
30	20 29	sseldd	$⊢ ((F : A ⟶ ℝ \land A \in dom vol) \land (y \in (topGen (ran (.)) ↾_{𝑡} A) \land (x \in y \land F [y] \subseteq b))) \to F (x) \in b$
31	30	rexlimdvaa	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to (\exists y \in (topGen (ran (.)) ↾_{𝑡} A) (x \in y \land F [y] \subseteq b) \to F (x) \in b)$
32	31	ad3antrrr	$⊢ ((((F : A ⟶ ℝ \land A \in dom vol) \land b \in ran (.)) \land x \in A) \land F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)) \to (\exists y \in (topGen (ran (.)) ↾_{𝑡} A) (x \in y \land F [y] \subseteq b) \to F (x) \in b)$
33	19 32	impbid	$⊢ ((((F : A ⟶ ℝ \land A \in dom vol) \land b \in ran (.)) \land x \in A) \land F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)) \to (F (x) \in b \leftrightarrow \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (x \in y \land F [y] \subseteq b))$
34	33	pm5.32da	$⊢ (((F : A ⟶ ℝ \land A \in dom vol) \land b \in ran (.)) \land x \in A) \to ((F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b) \leftrightarrow (F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (x \in y \land F [y] \subseteq b)))$
35		r19.42v	$⊢ \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land (x \in y \land F [y] \subseteq b)) \leftrightarrow (F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (x \in y \land F [y] \subseteq b))$
36	34 35	bitr4di	$⊢ (((F : A ⟶ ℝ \land A \in dom vol) \land b \in ran (.)) \land x \in A) \to ((F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b) \leftrightarrow \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land (x \in y \land F [y] \subseteq b)))$
37	36	orbi1d	$⊢ (((F : A ⟶ ℝ \land A \in dom vol) \land b \in ran (.)) \land x \in A) \to (((F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b) \lor (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b)) \leftrightarrow (\exists y \in (topGen (ran (.)) ↾_{𝑡} A) (F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land (x \in y \land F [y] \subseteq b)) \lor (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b)))$
38	9 37	syl5bb	$⊢ (((F : A ⟶ ℝ \land A \in dom vol) \land b \in ran (.)) \land x \in A) \to (F (x) \in b \leftrightarrow (\exists y \in (topGen (ran (.)) ↾_{𝑡} A) (F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land (x \in y \land F [y] \subseteq b)) \lor (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b)))$
39	38	rabbidva	$⊢ ((F : A ⟶ ℝ \land A \in dom vol) \land b \in ran (.)) \to \{x \in A \| F (x) \in b\} = \{x \in A \| (\exists y \in (topGen (ran (.)) ↾_{𝑡} A) (F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land (x \in y \land F [y] \subseteq b)) \lor (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b))\}$
40		eqid	$⊢ (x \in A ⟼ F (x)) = (x \in A ⟼ F (x))$
41	40	mptpreima	$⊢ {(x \in A ⟼ F (x))}^{-1} [b] = \{x \in A \| F (x) \in b\}$
42		unrab	$⊢ \{x \in A \| \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land (x \in y \land F [y] \subseteq b))\} \cup \{x \in A \| (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b)\} = \{x \in A \| (\exists y \in (topGen (ran (.)) ↾_{𝑡} A) (F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land (x \in y \land F [y] \subseteq b)) \lor (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b))\}$
43	39 41 42	3eqtr4g	$⊢ ((F : A ⟶ ℝ \land A \in dom vol) \land b \in ran (.)) \to {(x \in A ⟼ F (x))}^{-1} [b] = \{x \in A \| \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land (x \in y \land F [y] \subseteq b))\} \cup \{x \in A \| (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b)\}$
44	5 43	eqtrd	$⊢ ((F : A ⟶ ℝ \land A \in dom vol) \land b \in ran (.)) \to F^{-1} [b] = \{x \in A \| \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land (x \in y \land F [y] \subseteq b))\} \cup \{x \in A \| (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b)\}$
45	44	3adantl3	$⊢ ((F : A ⟶ ℝ \land A \in dom vol \land {vol}^{*} (A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}]) = 0) \land b \in ran (.)) \to F^{-1} [b] = \{x \in A \| \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land (x \in y \land F [y] \subseteq b))\} \cup \{x \in A \| (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b)\}$
46		incom	$⊢ ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} \cap \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\} = \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\} \cap ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\}$
47		dfin4	$⊢ ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} \cap \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\} = ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} ∖ (⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} ∖ \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\})$
48		inrab	$⊢ \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\} \cap \{x \in A \| (x \in y \land F [y] \subseteq b)\} = \{x \in A \| (F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land (x \in y \land F [y] \subseteq b))\}$
49	48	a1i	$⊢ y \in (topGen (ran (.)) ↾_{𝑡} A) \to \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\} \cap \{x \in A \| (x \in y \land F [y] \subseteq b)\} = \{x \in A \| (F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land (x \in y \land F [y] \subseteq b))\}$
50	49	iuneq2i	$⊢ ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} (\{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\} \cap \{x \in A \| (x \in y \land F [y] \subseteq b)\}) = ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land (x \in y \land F [y] \subseteq b))\}$
51		iunin2	$⊢ ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} (\{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\} \cap \{x \in A \| (x \in y \land F [y] \subseteq b)\}) = \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\} \cap ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\}$
52		iunrab	$⊢ ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land (x \in y \land F [y] \subseteq b))\} = \{x \in A \| \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land (x \in y \land F [y] \subseteq b))\}$
53	50 51 52	3eqtr3i	$⊢ \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\} \cap ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} = \{x \in A \| \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land (x \in y \land F [y] \subseteq b))\}$
54	46 47 53	3eqtr3i	$⊢ ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} ∖ (⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} ∖ \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\}) = \{x \in A \| \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land (x \in y \land F [y] \subseteq b))\}$
55		eqeq2	$⊢ y = if (F [y] \subseteq b, y, \emptyset) \to (\{x \in A \| (x \in y \land F [y] \subseteq b)\} = y \leftrightarrow \{x \in A \| (x \in y \land F [y] \subseteq b)\} = if (F [y] \subseteq b, y, \emptyset))$
56		eqeq2	$⊢ \emptyset = if (F [y] \subseteq b, y, \emptyset) \to (\{x \in A \| (x \in y \land F [y] \subseteq b)\} = \emptyset \leftrightarrow \{x \in A \| (x \in y \land F [y] \subseteq b)\} = if (F [y] \subseteq b, y, \emptyset))$
57		simprrl	$⊢ ((y \in (topGen (ran (.)) ↾_{𝑡} A) \land F [y] \subseteq b) \land (x \in A \land (x \in y \land F [y] \subseteq b))) \to x \in y$
58	25	adantr	$⊢ (y \in (topGen (ran (.)) ↾_{𝑡} A) \land F [y] \subseteq b) \to y \subseteq A$
59	58	sselda	$⊢ ((y \in (topGen (ran (.)) ↾_{𝑡} A) \land F [y] \subseteq b) \land x \in y) \to x \in A$
60		pm3.22	$⊢ (F [y] \subseteq b \land x \in y) \to (x \in y \land F [y] \subseteq b)$
61	60	adantll	$⊢ ((y \in (topGen (ran (.)) ↾_{𝑡} A) \land F [y] \subseteq b) \land x \in y) \to (x \in y \land F [y] \subseteq b)$
62	59 61	jca	$⊢ ((y \in (topGen (ran (.)) ↾_{𝑡} A) \land F [y] \subseteq b) \land x \in y) \to (x \in A \land (x \in y \land F [y] \subseteq b))$
63	57 62	impbida	$⊢ (y \in (topGen (ran (.)) ↾_{𝑡} A) \land F [y] \subseteq b) \to ((x \in A \land (x \in y \land F [y] \subseteq b)) \leftrightarrow x \in y)$
64	63	abbidv	$⊢ (y \in (topGen (ran (.)) ↾_{𝑡} A) \land F [y] \subseteq b) \to \{x \| (x \in A \land (x \in y \land F [y] \subseteq b))\} = \{x \| x \in y\}$
65		df-rab	$⊢ \{x \in A \| (x \in y \land F [y] \subseteq b)\} = \{x \| (x \in A \land (x \in y \land F [y] \subseteq b))\}$
66		cvjust	$⊢ y = \{x \| x \in y\}$
67	64 65 66	3eqtr4g	$⊢ (y \in (topGen (ran (.)) ↾_{𝑡} A) \land F [y] \subseteq b) \to \{x \in A \| (x \in y \land F [y] \subseteq b)\} = y$
68		simpr	$⊢ (x \in y \land F [y] \subseteq b) \to F [y] \subseteq b$
69	68	con3i	$⊢ \neg F [y] \subseteq b \to \neg (x \in y \land F [y] \subseteq b)$
70	69	ralrimivw	$⊢ \neg F [y] \subseteq b \to \forall x \in A \neg (x \in y \land F [y] \subseteq b)$
71		rabeq0	$⊢ \{x \in A \| (x \in y \land F [y] \subseteq b)\} = \emptyset \leftrightarrow \forall x \in A \neg (x \in y \land F [y] \subseteq b)$
72	70 71	sylibr	$⊢ \neg F [y] \subseteq b \to \{x \in A \| (x \in y \land F [y] \subseteq b)\} = \emptyset$
73	72	adantl	$⊢ (y \in (topGen (ran (.)) ↾_{𝑡} A) \land \neg F [y] \subseteq b) \to \{x \in A \| (x \in y \land F [y] \subseteq b)\} = \emptyset$
74	55 56 67 73	ifbothda	$⊢ y \in (topGen (ran (.)) ↾_{𝑡} A) \to \{x \in A \| (x \in y \land F [y] \subseteq b)\} = if (F [y] \subseteq b, y, \emptyset)$
75	74	iuneq2i	$⊢ ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} = ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} if (F [y] \subseteq b, y, \emptyset)$
76		retop	$⊢ topGen (ran (.)) \in Top$
77		resttop	$⊢ (topGen (ran (.)) \in Top \land A \in dom vol) \to topGen (ran (.)) ↾_{𝑡} A \in Top$
78	76 77	mpan	$⊢ A \in dom vol \to topGen (ran (.)) ↾_{𝑡} A \in Top$
79		0opn	$⊢ topGen (ran (.)) ↾_{𝑡} A \in Top \to \emptyset \in (topGen (ran (.)) ↾_{𝑡} A)$
80	78 79	syl	$⊢ A \in dom vol \to \emptyset \in (topGen (ran (.)) ↾_{𝑡} A)$
81		ifcl	$⊢ (y \in (topGen (ran (.)) ↾_{𝑡} A) \land \emptyset \in (topGen (ran (.)) ↾_{𝑡} A)) \to if (F [y] \subseteq b, y, \emptyset) \in (topGen (ran (.)) ↾_{𝑡} A)$
82	81	ancoms	$⊢ (\emptyset \in (topGen (ran (.)) ↾_{𝑡} A) \land y \in (topGen (ran (.)) ↾_{𝑡} A)) \to if (F [y] \subseteq b, y, \emptyset) \in (topGen (ran (.)) ↾_{𝑡} A)$
83	80 82	sylan	$⊢ (A \in dom vol \land y \in (topGen (ran (.)) ↾_{𝑡} A)) \to if (F [y] \subseteq b, y, \emptyset) \in (topGen (ran (.)) ↾_{𝑡} A)$
84	83	ralrimiva	$⊢ A \in dom vol \to \forall y \in (topGen (ran (.)) ↾_{𝑡} A) if (F [y] \subseteq b, y, \emptyset) \in (topGen (ran (.)) ↾_{𝑡} A)$
85		iunopn	$⊢ (topGen (ran (.)) ↾_{𝑡} A \in Top \land \forall y \in (topGen (ran (.)) ↾_{𝑡} A) if (F [y] \subseteq b, y, \emptyset) \in (topGen (ran (.)) ↾_{𝑡} A)) \to ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} if (F [y] \subseteq b, y, \emptyset) \in (topGen (ran (.)) ↾_{𝑡} A)$
86	78 84 85	syl2anc	$⊢ A \in dom vol \to ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} if (F [y] \subseteq b, y, \emptyset) \in (topGen (ran (.)) ↾_{𝑡} A)$
87		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} A = topGen (ran (.)) ↾_{𝑡} A$
88	87	subopnmbl	$⊢ (A \in dom vol \land ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} if (F [y] \subseteq b, y, \emptyset) \in (topGen (ran (.)) ↾_{𝑡} A)) \to ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} if (F [y] \subseteq b, y, \emptyset) \in dom vol$
89	86 88	mpdan	$⊢ A \in dom vol \to ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} if (F [y] \subseteq b, y, \emptyset) \in dom vol$
90	75 89	eqeltrid	$⊢ A \in dom vol \to ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} \in dom vol$
91		difss	$⊢ ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} ∖ \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\} \subseteq ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\}$
92		ssrab2	$⊢ \{x \in A \| (x \in y \land F [y] \subseteq b)\} \subseteq A$
93	92	rgenw	$⊢ \forall y \in (topGen (ran (.)) ↾_{𝑡} A) \{x \in A \| (x \in y \land F [y] \subseteq b)\} \subseteq A$
94		iunss	$⊢ ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} \subseteq A \leftrightarrow \forall y \in (topGen (ran (.)) ↾_{𝑡} A) \{x \in A \| (x \in y \land F [y] \subseteq b)\} \subseteq A$
95	93 94	mpbir	$⊢ ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} \subseteq A$
96	91 95	sstri	$⊢ ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} ∖ \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\} \subseteq A$
97		mblss	$⊢ A \in dom vol \to A \subseteq ℝ$
98	96 97	sstrid	$⊢ A \in dom vol \to ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} ∖ \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\} \subseteq ℝ$
99		ssdif	$⊢ ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} \subseteq A \to ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} ∖ \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\} \subseteq A ∖ \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\}$
100	95 99	ax-mp	$⊢ ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} ∖ \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\} \subseteq A ∖ \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\}$
101		rele	$⊢ Rel E$
102		elrelimasn	$⊢ Rel E \to (((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \in E [\{F\}] \leftrightarrow F E ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x))$
103	101 102	ax-mp	$⊢ ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \in E [\{F\}] \leftrightarrow F E ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)$
104		fvex	$⊢ ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \in V$
105	104	epeli	$⊢ F E ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \leftrightarrow F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)$
106	103 105	bitr2i	$⊢ F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \leftrightarrow ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \in E [\{F\}]$
107	106	anbi2i	$⊢ (x \in A \land F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)) \leftrightarrow (x \in A \land ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \in E [\{F\}])$
108		ovex	$⊢ ℝ^{A} \in V$
109	108	rabex	$⊢ \{f \in (ℝ^{A}) \| \forall b \in topGen (ran (.)) (f (x) \in b \to \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (x \in y \land f [y] \subseteq b))\} \in V$
110		eqid	$⊢ (x \in A ⟼ \{f \in (ℝ^{A}) \| \forall b \in topGen (ran (.)) (f (x) \in b \to \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (x \in y \land f [y] \subseteq b))\}) = (x \in A ⟼ \{f \in (ℝ^{A}) \| \forall b \in topGen (ran (.)) (f (x) \in b \to \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (x \in y \land f [y] \subseteq b))\})$
111	109 110	fnmpti	$⊢ (x \in A ⟼ \{f \in (ℝ^{A}) \| \forall b \in topGen (ran (.)) (f (x) \in b \to \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (x \in y \land f [y] \subseteq b))\}) Fn A$
112		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
113		resttopon	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land A \subseteq ℝ) \to topGen (ran (.)) ↾_{𝑡} A \in TopOn (A)$
114	112 97 113	sylancr	$⊢ A \in dom vol \to topGen (ran (.)) ↾_{𝑡} A \in TopOn (A)$
115		cnpfval	$⊢ (topGen (ran (.)) ↾_{𝑡} A \in TopOn (A) \land topGen (ran (.)) \in TopOn (ℝ)) \to (topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)) = (x \in A ⟼ \{f \in (ℝ^{A}) \| \forall b \in topGen (ran (.)) (f (x) \in b \to \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (x \in y \land f [y] \subseteq b))\})$
116	114 112 115	sylancl	$⊢ A \in dom vol \to (topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)) = (x \in A ⟼ \{f \in (ℝ^{A}) \| \forall b \in topGen (ran (.)) (f (x) \in b \to \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (x \in y \land f [y] \subseteq b))\})$
117	116	fneq1d	$⊢ A \in dom vol \to (((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) Fn A \leftrightarrow (x \in A ⟼ \{f \in (ℝ^{A}) \| \forall b \in topGen (ran (.)) (f (x) \in b \to \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (x \in y \land f [y] \subseteq b))\}) Fn A)$
118	111 117	mpbiri	$⊢ A \in dom vol \to ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) Fn A$
119		elpreima	$⊢ ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) Fn A \to (x \in {((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} [E [\{F\}]] \leftrightarrow (x \in A \land ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \in E [\{F\}]))$
120	118 119	syl	$⊢ A \in dom vol \to (x \in {((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} [E [\{F\}]] \leftrightarrow (x \in A \land ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \in E [\{F\}]))$
121	107 120	bitr4id	$⊢ A \in dom vol \to ((x \in A \land F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)) \leftrightarrow x \in {((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} [E [\{F\}]])$
122	121	abbidv	$⊢ A \in dom vol \to \{x \| (x \in A \land F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x))\} = \{x \| x \in {((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} [E [\{F\}]]\}$
123		df-rab	$⊢ \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\} = \{x \| (x \in A \land F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x))\}$
124		imaco	$⊢ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}] = {((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} [E [\{F\}]]$
125		abid2	$⊢ \{x \| x \in {((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} [E [\{F\}]]\} = {((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} [E [\{F\}]]$
126	124 125	eqtr4i	$⊢ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}] = \{x \| x \in {((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} [E [\{F\}]]\}$
127	122 123 126	3eqtr4g	$⊢ A \in dom vol \to \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\} = ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}]$
128	127	difeq2d	$⊢ A \in dom vol \to A ∖ \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\} = A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}]$
129	100 128	sseqtrid	$⊢ A \in dom vol \to ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} ∖ \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\} \subseteq A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}]$
130		difss	$⊢ A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}] \subseteq A$
131	130 97	sstrid	$⊢ A \in dom vol \to A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}] \subseteq ℝ$
132	129 131	jca	$⊢ A \in dom vol \to (⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} ∖ \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\} \subseteq A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}] \land A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}] \subseteq ℝ)$
133		ovolssnul	$⊢ (⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} ∖ \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\} \subseteq A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}] \land A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}] \subseteq ℝ \land {vol}^{} (A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}]) = 0) \to {vol}^{} (⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} ∖ \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\}) = 0$
134	133	3expa	$⊢ ((⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} ∖ \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\} \subseteq A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}] \land A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}] \subseteq ℝ) \land {vol}^{} (A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}]) = 0) \to {vol}^{} (⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} ∖ \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\}) = 0$
135	132 134	sylan	$⊢ (A \in dom vol \land {vol}^{} (A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}]) = 0) \to {vol}^{} (⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} ∖ \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\}) = 0$
136		nulmbl	$⊢ (⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} ∖ \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\} \subseteq ℝ \land {vol}^{*} (⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} ∖ \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\}) = 0) \to ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} ∖ \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\} \in dom vol$
137	98 135 136	syl2an2r	$⊢ (A \in dom vol \land {vol}^{*} (A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}]) = 0) \to ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} ∖ \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\} \in dom vol$
138		difmbl	$⊢ (⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} \in dom vol \land ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} ∖ \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\} \in dom vol) \to ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} ∖ (⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} ∖ \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\}) \in dom vol$
139	90 137 138	syl2an2r	$⊢ (A \in dom vol \land {vol}^{*} (A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}]) = 0) \to ⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} ∖ (⋃_{y \in topGen (ran (.)) ↾_{𝑡} A} \{x \in A \| (x \in y \land F [y] \subseteq b)\} ∖ \{x \in A \| F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x)\}) \in dom vol$
140	54 139	eqeltrrid	$⊢ (A \in dom vol \land {vol}^{*} (A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}]) = 0) \to \{x \in A \| \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land (x \in y \land F [y] \subseteq b))\} \in dom vol$
141		ssrab2	$⊢ \{x \in A \| (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b)\} \subseteq A$
142	141 97	sstrid	$⊢ A \in dom vol \to \{x \in A \| (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b)\} \subseteq ℝ$
143	124	eleq2i	$⊢ x \in ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}] \leftrightarrow x \in {((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} [E [\{F\}]]$
144		ibar	$⊢ x \in A \to (((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \in E [\{F\}] \leftrightarrow (x \in A \land ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \in E [\{F\}]))$
145	106 144	bitr2id	$⊢ x \in A \to ((x \in A \land ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \in E [\{F\}]) \leftrightarrow F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x))$
146	120 145	sylan9bb	$⊢ (A \in dom vol \land x \in A) \to (x \in {((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} [E [\{F\}]] \leftrightarrow F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x))$
147	143 146	bitr2id	$⊢ (A \in dom vol \land x \in A) \to (F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \leftrightarrow x \in ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}])$
148	147	notbid	$⊢ (A \in dom vol \land x \in A) \to (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \leftrightarrow \neg x \in ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}])$
149	148	biimpd	$⊢ (A \in dom vol \land x \in A) \to (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \to \neg x \in ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}])$
150	149	adantrd	$⊢ (A \in dom vol \land x \in A) \to ((\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b) \to \neg x \in ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}])$
151	150	ss2rabdv	$⊢ A \in dom vol \to \{x \in A \| (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b)\} \subseteq \{x \in A \| \neg x \in ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}]\}$
152		dfdif2	$⊢ A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}] = \{x \in A \| \neg x \in ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}]\}$
153	151 152	sseqtrrdi	$⊢ A \in dom vol \to \{x \in A \| (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b)\} \subseteq A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}]$
154	153 131	jca	$⊢ A \in dom vol \to (\{x \in A \| (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b)\} \subseteq A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}] \land A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}] \subseteq ℝ)$
155		ovolssnul	$⊢ (\{x \in A \| (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b)\} \subseteq A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}] \land A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}] \subseteq ℝ \land {vol}^{} (A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}]) = 0) \to {vol}^{} (\{x \in A \| (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b)\}) = 0$
156	155	3expa	$⊢ ((\{x \in A \| (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b)\} \subseteq A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}] \land A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}] \subseteq ℝ) \land {vol}^{} (A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}]) = 0) \to {vol}^{} (\{x \in A \| (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b)\}) = 0$
157	154 156	sylan	$⊢ (A \in dom vol \land {vol}^{} (A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}]) = 0) \to {vol}^{} (\{x \in A \| (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b)\}) = 0$
158		nulmbl	$⊢ (\{x \in A \| (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b)\} \subseteq ℝ \land {vol}^{*} (\{x \in A \| (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b)\}) = 0) \to \{x \in A \| (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b)\} \in dom vol$
159	142 157 158	syl2an2r	$⊢ (A \in dom vol \land {vol}^{*} (A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}]) = 0) \to \{x \in A \| (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b)\} \in dom vol$
160		unmbl	$⊢ (\{x \in A \| \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land (x \in y \land F [y] \subseteq b))\} \in dom vol \land \{x \in A \| (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b)\} \in dom vol) \to \{x \in A \| \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land (x \in y \land F [y] \subseteq b))\} \cup \{x \in A \| (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b)\} \in dom vol$
161	140 159 160	syl2anc	$⊢ (A \in dom vol \land {vol}^{*} (A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}]) = 0) \to \{x \in A \| \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land (x \in y \land F [y] \subseteq b))\} \cup \{x \in A \| (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b)\} \in dom vol$
162	161	3adant1	$⊢ (F : A ⟶ ℝ \land A \in dom vol \land {vol}^{*} (A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}]) = 0) \to \{x \in A \| \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land (x \in y \land F [y] \subseteq b))\} \cup \{x \in A \| (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b)\} \in dom vol$
163	162	adantr	$⊢ ((F : A ⟶ ℝ \land A \in dom vol \land {vol}^{*} (A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}]) = 0) \land b \in ran (.)) \to \{x \in A \| \exists y \in (topGen (ran (.)) ↾_{𝑡} A) (F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land (x \in y \land F [y] \subseteq b))\} \cup \{x \in A \| (\neg F \in ((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.))) (x) \land F (x) \in b)\} \in dom vol$
164	45 163	eqeltrd	$⊢ ((F : A ⟶ ℝ \land A \in dom vol \land {vol}^{*} (A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}]) = 0) \land b \in ran (.)) \to F^{-1} [b] \in dom vol$
165	164	ralrimiva	$⊢ (F : A ⟶ ℝ \land A \in dom vol \land {vol}^{*} (A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}]) = 0) \to \forall b \in ran (.) F^{-1} [b] \in dom vol$
166		ismbf	$⊢ F : A ⟶ ℝ \to (F \in MblFn \leftrightarrow \forall b \in ran (.) F^{-1} [b] \in dom vol)$
167	166	3ad2ant1	$⊢ (F : A ⟶ ℝ \land A \in dom vol \land {vol}^{*} (A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}]) = 0) \to (F \in MblFn \leftrightarrow \forall b \in ran (.) F^{-1} [b] \in dom vol)$
168	165 167	mpbird	$⊢ (F : A ⟶ ℝ \land A \in dom vol \land {vol}^{*} (A ∖ ({((topGen (ran (.)) ↾_{𝑡} A) CnP topGen (ran (.)))}^{-1} \circ E) [\{F\}]) = 0) \to F \in MblFn$

Metamath Proof Explorer

Theorem cnambfre

Proof