cnambfre - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cnambfre		Structured version Visualization version GIF version

Theorem cnambfre 33789

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

**Assertion**
Ref	Expression
cnambfre	⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → 𝐹 ∈ MblFn)

Proof of Theorem cnambfre Dummy variables 𝑓 𝑏 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		id 22	. . . . . . . . . 10 ⊢ (𝐹:𝐴⟶ℝ → 𝐹:𝐴⟶ℝ)
2	1	feqmptd 6480	. . . . . . . . 9 ⊢ (𝐹:𝐴⟶ℝ → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
3	2	cnveqd 5513	. . . . . . . 8 ⊢ (𝐹:𝐴⟶ℝ → ^◡𝐹 = ^◡(𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
4	3	imaeq1d 5689	. . . . . . 7 ⊢ (𝐹:𝐴⟶ℝ → (^◡𝐹 “ 𝑏) = (^◡(𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) “ 𝑏))
5	4	ad2antrr 708	. . . . . 6 ⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) → (^◡𝐹 “ 𝑏) = (^◡(𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) “ 𝑏))
6		exmid 909	. . . . . . . . . . 11 ⊢ (𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∨ ¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥))
7	6	biantrur 522	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ∈ 𝑏 ↔ ((𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∨ ¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)) ∧ (𝐹‘𝑥) ∈ 𝑏))
8		andir 1022	. . . . . . . . . 10 ⊢ (((𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∨ ¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)) ∧ (𝐹‘𝑥) ∈ 𝑏) ↔ ((𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏) ∨ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)))
9	7, 8	bitri 266	. . . . . . . . 9 ⊢ ((𝐹‘𝑥) ∈ 𝑏 ↔ ((𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏) ∨ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)))
10		retopbas 22798	. . . . . . . . . . . . . . . . . 18 ⊢ ran (,) ∈ TopBases
11		bastg 21005	. . . . . . . . . . . . . . . . . 18 ⊢ (ran (,) ∈ TopBases → ran (,) ⊆ (topGen‘ran (,)))
12	10, 11	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ran (,) ⊆ (topGen‘ran (,))
13	12	sseli 3805	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ ran (,) → 𝑏 ∈ (topGen‘ran (,)))
14	13	ad2antlr 709	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) ∧ 𝑥 ∈ 𝐴) → 𝑏 ∈ (topGen‘ran (,)))
15		cnpimaex 21295	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ 𝑏 ∈ (topGen‘ran (,)) ∧ (𝐹‘𝑥) ∈ 𝑏) → ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))
16	15	3com12 1146	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 ∈ (topGen‘ran (,)) ∧ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏) → ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))
17	16	3expa 1140	. . . . . . . . . . . . . . 15 ⊢ (((𝑏 ∈ (topGen‘ran (,)) ∧ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)) ∧ (𝐹‘𝑥) ∈ 𝑏) → ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))
18	14, 17	sylanl1 662	. . . . . . . . . . . . . 14 ⊢ ((((((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) ∧ 𝑥 ∈ 𝐴) ∧ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)) ∧ (𝐹‘𝑥) ∈ 𝑏) → ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))
19	18	ex 399	. . . . . . . . . . . . 13 ⊢ (((((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) ∧ 𝑥 ∈ 𝐴) ∧ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)) → ((𝐹‘𝑥) ∈ 𝑏 → ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)))
20		simprrr 791	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ (𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))) → (𝐹 “ 𝑦) ⊆ 𝑏)
21		ffn 6266	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹:𝐴⟶ℝ → 𝐹 Fn 𝐴)
22	21	adantr 468	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → 𝐹 Fn 𝐴)
23		restsspw 16317	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((topGen‘ran (,)) ↾_t 𝐴) ⊆ 𝒫 𝐴
24	23	sseli 3805	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴) → 𝑦 ∈ 𝒫 𝐴)
25	24	elpwid 4374	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴) → 𝑦 ⊆ 𝐴)
26		simpl 470	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏) → 𝑥 ∈ 𝑦)
27		fnfvima 6731	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ 𝑥 ∈ 𝑦) → (𝐹‘𝑥) ∈ (𝐹 “ 𝑦))
28	22, 25, 26, 27	syl3an 1192	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) → (𝐹‘𝑥) ∈ (𝐹 “ 𝑦))
29	28	3expb 1142	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ (𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))) → (𝐹‘𝑥) ∈ (𝐹 “ 𝑦))
30	20, 29	sseldd 3810	. . . . . . . . . . . . . . 15 ⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ (𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))) → (𝐹‘𝑥) ∈ 𝑏)
31	30	rexlimdvaa 3231	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏) → (𝐹‘𝑥) ∈ 𝑏))
32	31	ad3antrrr 712	. . . . . . . . . . . . 13 ⊢ (((((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) ∧ 𝑥 ∈ 𝐴) ∧ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)) → (∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏) → (𝐹‘𝑥) ∈ 𝑏))
33	19, 32	impbid 203	. . . . . . . . . . . 12 ⊢ (((((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) ∧ 𝑥 ∈ 𝐴) ∧ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)) → ((𝐹‘𝑥) ∈ 𝑏 ↔ ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)))
34	33	pm5.32da 570	. . . . . . . . . . 11 ⊢ ((((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) ∧ 𝑥 ∈ 𝐴) → ((𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏) ↔ (𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))))
35		r19.42v 3291	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) ↔ (𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)))
36	34, 35	syl6bbr 280	. . . . . . . . . 10 ⊢ ((((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) ∧ 𝑥 ∈ 𝐴) → ((𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏) ↔ ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))))
37	36	orbi1d 931	. . . . . . . . 9 ⊢ ((((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) ∧ 𝑥 ∈ 𝐴) → (((𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏) ∨ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)) ↔ (∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) ∨ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏))))
38	9, 37	syl5bb 274	. . . . . . . 8 ⊢ ((((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) ∈ 𝑏 ↔ (∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) ∨ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏))))
39	38	rabbidva 3389	. . . . . . 7 ⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) → {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ∈ 𝑏} = {𝑥 ∈ 𝐴 ∣ (∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) ∨ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏))})
40		eqid 2817	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))
41	40	mptpreima 5856	. . . . . . 7 ⊢ (^◡(𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) “ 𝑏) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ∈ 𝑏}
42		unrab 4110	. . . . . . 7 ⊢ ({𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} ∪ {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)}) = {𝑥 ∈ 𝐴 ∣ (∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) ∨ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏))}
43	39, 41, 42	3eqtr4g 2876	. . . . . 6 ⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) → (^◡(𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) “ 𝑏) = ({𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} ∪ {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)}))
44	5, 43	eqtrd 2851	. . . . 5 ⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) → (^◡𝐹 “ 𝑏) = ({𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} ∪ {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)}))
45	44	3adantl3 1202	. . . 4 ⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) ∧ 𝑏 ∈ ran (,)) → (^◡𝐹 “ 𝑏) = ({𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} ∪ {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)}))
46		incom 4015	. . . . . . . . 9 ⊢ (∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∩ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)}) = ({𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)} ∩ ∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)})
47		dfin4 4080	. . . . . . . . 9 ⊢ (∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∩ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)}) = (∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ (∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)}))
48		inrab 4111	. . . . . . . . . . . 12 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)} ∩ {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)}) = {𝑥 ∈ 𝐴 ∣ (𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))}
49	48	a1i 11	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴) → ({𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)} ∩ {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)}) = {𝑥 ∈ 𝐴 ∣ (𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))})
50	49	iuneq2i 4742	. . . . . . . . . 10 ⊢ ∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)({𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)} ∩ {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)}) = ∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))}
51		iunin2 4787	. . . . . . . . . 10 ⊢ ∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)({𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)} ∩ {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)}) = ({𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)} ∩ ∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)})
52		iunrab 4770	. . . . . . . . . 10 ⊢ ∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} = {𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))}
53	50, 51, 52	3eqtr3i 2847	. . . . . . . . 9 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)} ∩ ∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)}) = {𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))}
54	46, 47, 53	3eqtr3i 2847	. . . . . . . 8 ⊢ (∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ (∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)})) = {𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))}
55		eqeq2 2828	. . . . . . . . . . . . 13 ⊢ (𝑦 = if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) → ({𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = 𝑦 ↔ {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅)))
56		eqeq2 2828	. . . . . . . . . . . . 13 ⊢ (∅ = if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) → ({𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = ∅ ↔ {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅)))
57		simprrl 790	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴) ∧ (𝐹 “ 𝑦) ⊆ 𝑏) ∧ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))) → 𝑥 ∈ 𝑦)
58	25	adantr 468	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴) ∧ (𝐹 “ 𝑦) ⊆ 𝑏) → 𝑦 ⊆ 𝐴)
59	58	sselda 3809	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴) ∧ (𝐹 “ 𝑦) ⊆ 𝑏) ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴)
60		pm3.22 449	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 “ 𝑦) ⊆ 𝑏 ∧ 𝑥 ∈ 𝑦) → (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))
61	60	adantll 696	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴) ∧ (𝐹 “ 𝑦) ⊆ 𝑏) ∧ 𝑥 ∈ 𝑦) → (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))
62	59, 61	jca 503	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴) ∧ (𝐹 “ 𝑦) ⊆ 𝑏) ∧ 𝑥 ∈ 𝑦) → (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)))
63	57, 62	impbida 826	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴) ∧ (𝐹 “ 𝑦) ⊆ 𝑏) → ((𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) ↔ 𝑥 ∈ 𝑦))
64	63	abbidv 2936	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴) ∧ (𝐹 “ 𝑦) ⊆ 𝑏) → {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} = {𝑥 ∣ 𝑥 ∈ 𝑦})
65		df-rab 3116	. . . . . . . . . . . . . 14 ⊢ {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))}
66		cvjust 2812	. . . . . . . . . . . . . 14 ⊢ 𝑦 = {𝑥 ∣ 𝑥 ∈ 𝑦}
67	64, 65, 66	3eqtr4g 2876	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴) ∧ (𝐹 “ 𝑦) ⊆ 𝑏) → {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = 𝑦)
68		simpr 473	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏) → (𝐹 “ 𝑦) ⊆ 𝑏)
69	68	con3i 151	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝐹 “ 𝑦) ⊆ 𝑏 → ¬ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))
70	69	ralrimivw 3166	. . . . . . . . . . . . . . 15 ⊢ (¬ (𝐹 “ 𝑦) ⊆ 𝑏 → ∀𝑥 ∈ 𝐴 ¬ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))
71		rabeq0 4168	. . . . . . . . . . . . . . 15 ⊢ ({𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))
72	70, 71	sylibr 225	. . . . . . . . . . . . . 14 ⊢ (¬ (𝐹 “ 𝑦) ⊆ 𝑏 → {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = ∅)
73	72	adantl 469	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴) ∧ ¬ (𝐹 “ 𝑦) ⊆ 𝑏) → {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = ∅)
74	55, 56, 67, 73	ifbothda 4327	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴) → {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅))
75	74	iuneq2i 4742	. . . . . . . . . . 11 ⊢ ∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = ∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅)
76		retop 22799	. . . . . . . . . . . . . 14 ⊢ (topGen‘ran (,)) ∈ Top
77		resttop 21199	. . . . . . . . . . . . . 14 ⊢ (((topGen‘ran (,)) ∈ Top ∧ 𝐴 ∈ dom vol) → ((topGen‘ran (,)) ↾_t 𝐴) ∈ Top)
78	76, 77	mpan 673	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ dom vol → ((topGen‘ran (,)) ↾_t 𝐴) ∈ Top)
79		0opn 20943	. . . . . . . . . . . . . . . 16 ⊢ (((topGen‘ran (,)) ↾_t 𝐴) ∈ Top → ∅ ∈ ((topGen‘ran (,)) ↾_t 𝐴))
80	78, 79	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ dom vol → ∅ ∈ ((topGen‘ran (,)) ↾_t 𝐴))
81		ifcl 4334	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴) ∧ ∅ ∈ ((topGen‘ran (,)) ↾_t 𝐴)) → if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ ((topGen‘ran (,)) ↾_t 𝐴))
82	81	ancoms 448	. . . . . . . . . . . . . . 15 ⊢ ((∅ ∈ ((topGen‘ran (,)) ↾_t 𝐴) ∧ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)) → if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ ((topGen‘ran (,)) ↾_t 𝐴))
83	80, 82	sylan 571	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ dom vol ∧ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)) → if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ ((topGen‘ran (,)) ↾_t 𝐴))
84	83	ralrimiva 3165	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ dom vol → ∀𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ ((topGen‘ran (,)) ↾_t 𝐴))
85		iunopn 20937	. . . . . . . . . . . . 13 ⊢ ((((topGen‘ran (,)) ↾_t 𝐴) ∈ Top ∧ ∀𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ ((topGen‘ran (,)) ↾_t 𝐴)) → ∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ ((topGen‘ran (,)) ↾_t 𝐴))
86	78, 84, 85	syl2anc 575	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ dom vol → ∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ ((topGen‘ran (,)) ↾_t 𝐴))
87		eqid 2817	. . . . . . . . . . . . 13 ⊢ ((topGen‘ran (,)) ↾_t 𝐴) = ((topGen‘ran (,)) ↾_t 𝐴)
88	87	subopnmbl 23608	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ dom vol ∧ ∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ ((topGen‘ran (,)) ↾_t 𝐴)) → ∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ dom vol)
89	86, 88	mpdan 670	. . . . . . . . . . 11 ⊢ (𝐴 ∈ dom vol → ∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ dom vol)
90	75, 89	syl5eqel 2900	. . . . . . . . . 10 ⊢ (𝐴 ∈ dom vol → ∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∈ dom vol)
91	90	adantr 468	. . . . . . . . 9 ⊢ ((𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → ∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∈ dom vol)
92		difss 3947	. . . . . . . . . . . . 13 ⊢ (∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)}) ⊆ ∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)}
93		ssrab2 3895	. . . . . . . . . . . . . . 15 ⊢ {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ⊆ 𝐴
94	93	rgenw 3123	. . . . . . . . . . . . . 14 ⊢ ∀𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ⊆ 𝐴
95		iunss 4764	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ⊆ 𝐴 ↔ ∀𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ⊆ 𝐴)
96	94, 95	mpbir 222	. . . . . . . . . . . . 13 ⊢ ∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ⊆ 𝐴
97	92, 96	sstri 3818	. . . . . . . . . . . 12 ⊢ (∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)}) ⊆ 𝐴
98		mblss 23535	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ dom vol → 𝐴 ⊆ ℝ)
99	97, 98	syl5ss 3820	. . . . . . . . . . 11 ⊢ (𝐴 ∈ dom vol → (∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)}) ⊆ ℝ)
100	99	adantr 468	. . . . . . . . . 10 ⊢ ((𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → (∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)}) ⊆ ℝ)
101		ssdif 3955	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ⊆ 𝐴 → (∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)}) ⊆ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)}))
102	96, 101	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)}) ⊆ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)})
103		ovex 6916	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℝ ↑_𝑚 𝐴) ∈ V
104	103	rabex 5020	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑓 ∈ (ℝ ↑_𝑚 𝐴) ∣ ∀𝑏 ∈ (topGen‘ran (,))((𝑓‘𝑥) ∈ 𝑏 → ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝑓 “ 𝑦) ⊆ 𝑏))} ∈ V
105		eqid 2817	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝐴 ↦ {𝑓 ∈ (ℝ ↑_𝑚 𝐴) ∣ ∀𝑏 ∈ (topGen‘ran (,))((𝑓‘𝑥) ∈ 𝑏 → ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝑓 “ 𝑦) ⊆ 𝑏))}) = (𝑥 ∈ 𝐴 ↦ {𝑓 ∈ (ℝ ↑_𝑚 𝐴) ∣ ∀𝑏 ∈ (topGen‘ran (,))((𝑓‘𝑥) ∈ 𝑏 → ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝑓 “ 𝑦) ⊆ 𝑏))})
106	104, 105	fnmpti 6243	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝐴 ↦ {𝑓 ∈ (ℝ ↑_𝑚 𝐴) ∣ ∀𝑏 ∈ (topGen‘ran (,))((𝑓‘𝑥) ∈ 𝑏 → ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝑓 “ 𝑦) ⊆ 𝑏))}) Fn 𝐴
107		retopon 22801	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ)
108		resttopon 21200	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ 𝐴 ⊆ ℝ) → ((topGen‘ran (,)) ↾_t 𝐴) ∈ (TopOn‘𝐴))
109	107, 98, 108	sylancr 577	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 ∈ dom vol → ((topGen‘ran (,)) ↾_t 𝐴) ∈ (TopOn‘𝐴))
110		cnpfval 21273	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((topGen‘ran (,)) ↾_t 𝐴) ∈ (TopOn‘𝐴) ∧ (topGen‘ran (,)) ∈ (TopOn‘ℝ)) → (((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) = (𝑥 ∈ 𝐴 ↦ {𝑓 ∈ (ℝ ↑_𝑚 𝐴) ∣ ∀𝑏 ∈ (topGen‘ran (,))((𝑓‘𝑥) ∈ 𝑏 → ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝑓 “ 𝑦) ⊆ 𝑏))}))
111	109, 107, 110	sylancl 576	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ dom vol → (((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) = (𝑥 ∈ 𝐴 ↦ {𝑓 ∈ (ℝ ↑_𝑚 𝐴) ∣ ∀𝑏 ∈ (topGen‘ran (,))((𝑓‘𝑥) ∈ 𝑏 → ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝑓 “ 𝑦) ⊆ 𝑏))}))
112	111	fneq1d 6202	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ dom vol → ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) Fn 𝐴 ↔ (𝑥 ∈ 𝐴 ↦ {𝑓 ∈ (ℝ ↑_𝑚 𝐴) ∣ ∀𝑏 ∈ (topGen‘ran (,))((𝑓‘𝑥) ∈ 𝑏 → ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝑓 “ 𝑦) ⊆ 𝑏))}) Fn 𝐴))
113	106, 112	mpbiri 249	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ dom vol → (((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) Fn 𝐴)
114		elpreima 6569	. . . . . . . . . . . . . . . . . 18 ⊢ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) Fn 𝐴 → (𝑥 ∈ (^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) “ ( E “ {𝐹})) ↔ (𝑥 ∈ 𝐴 ∧ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∈ ( E “ {𝐹}))))
115	113, 114	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ dom vol → (𝑥 ∈ (^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) “ ( E “ {𝐹})) ↔ (𝑥 ∈ 𝐴 ∧ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∈ ( E “ {𝐹}))))
116		rele 5466	. . . . . . . . . . . . . . . . . . . 20 ⊢ Rel E
117		elrelimasn 5713	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Rel E → (((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∈ ( E “ {𝐹}) ↔ 𝐹 E ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)))
118	116, 117	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∈ ( E “ {𝐹}) ↔ 𝐹 E ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥))
119		fvex 6431	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∈ V
120	119	epeli 5239	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 E ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ↔ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥))
121	118, 120	bitr2i 267	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ↔ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∈ ( E “ {𝐹}))
122	121	anbi2i 611	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∈ ( E “ {𝐹})))
123	115, 122	syl6rbbr 281	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ dom vol → ((𝑥 ∈ 𝐴 ∧ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)) ↔ 𝑥 ∈ (^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) “ ( E “ {𝐹}))))
124	123	abbidv 2936	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ dom vol → {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥))} = {𝑥 ∣ 𝑥 ∈ (^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) “ ( E “ {𝐹}))})
125		df-rab 3116	. . . . . . . . . . . . . . 15 ⊢ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥))}
126		imaco 5868	. . . . . . . . . . . . . . . 16 ⊢ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}) = (^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) “ ( E “ {𝐹}))
127		abid2 2940	. . . . . . . . . . . . . . . 16 ⊢ {𝑥 ∣ 𝑥 ∈ (^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) “ ( E “ {𝐹}))} = (^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) “ ( E “ {𝐹}))
128	126, 127	eqtr4i 2842	. . . . . . . . . . . . . . 15 ⊢ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}) = {𝑥 ∣ 𝑥 ∈ (^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) “ ( E “ {𝐹}))}
129	124, 125, 128	3eqtr4g 2876	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ dom vol → {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)} = ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}))
130	129	difeq2d 3938	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ dom vol → (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)}) = (𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹})))
131	102, 130	syl5sseq 3861	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ dom vol → (∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)}) ⊆ (𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹})))
132		difss 3947	. . . . . . . . . . . . 13 ⊢ (𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹})) ⊆ 𝐴
133	132, 98	syl5ss 3820	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ dom vol → (𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹})) ⊆ ℝ)
134	131, 133	jca 503	. . . . . . . . . . 11 ⊢ (𝐴 ∈ dom vol → ((∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)}) ⊆ (𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹})) ∧ (𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹})) ⊆ ℝ))
135		ovolssnul 23491	. . . . . . . . . . . 12 ⊢ (((∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)}) ⊆ (𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹})) ∧ (𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹})) ⊆ ℝ ∧ (vol‘(𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → (vol‘(∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)})) = 0)
136	135	3expa 1140	. . . . . . . . . . 11 ⊢ ((((∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)}) ⊆ (𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹})) ∧ (𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹})) ⊆ ℝ) ∧ (vol‘(𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → (vol‘(∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)})) = 0)
137	134, 136	sylan 571	. . . . . . . . . 10 ⊢ ((𝐴 ∈ dom vol ∧ (vol‘(𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → (vol‘(∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)})) = 0)
138		nulmbl 23539	. . . . . . . . . 10 ⊢ (((∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)}) ⊆ ℝ ∧ (vol*‘(∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)})) = 0) → (∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)}) ∈ dom vol)
139	100, 137, 138	syl2anc 575	. . . . . . . . 9 ⊢ ((𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → (∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)}) ∈ dom vol)
140		difmbl 23547	. . . . . . . . 9 ⊢ ((∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∈ dom vol ∧ (∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)}) ∈ dom vol) → (∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ (∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)})) ∈ dom vol)
141	91, 139, 140	syl2anc 575	. . . . . . . 8 ⊢ ((𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → (∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ (∪ 𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)})) ∈ dom vol)
142	54, 141	syl5eqelr 2901	. . . . . . 7 ⊢ ((𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → {𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} ∈ dom vol)
143		ssrab2 3895	. . . . . . . . . 10 ⊢ {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ⊆ 𝐴
144	143, 98	syl5ss 3820	. . . . . . . . 9 ⊢ (𝐴 ∈ dom vol → {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ⊆ ℝ)
145	144	adantr 468	. . . . . . . 8 ⊢ ((𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ⊆ ℝ)
146	126	eleq2i 2888	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}) ↔ 𝑥 ∈ (^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) “ ( E “ {𝐹})))
147		ibar 520	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐴 → (((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∈ ( E “ {𝐹}) ↔ (𝑥 ∈ 𝐴 ∧ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∈ ( E “ {𝐹}))))
148	121, 147	syl5rbb 275	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐴 ∧ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∈ ( E “ {𝐹})) ↔ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)))
149	115, 148	sylan9bb 501	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ (^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) “ ( E “ {𝐹})) ↔ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥)))
150	146, 149	syl5rbb 275	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ∈ 𝐴) → (𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ↔ 𝑥 ∈ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹})))
151	150	notbid 309	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ∈ 𝐴) → (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ↔ ¬ 𝑥 ∈ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹})))
152	151	biimpd 220	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ∈ 𝐴) → (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) → ¬ 𝑥 ∈ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹})))
153	152	adantrd 481	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ∈ 𝐴) → ((¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏) → ¬ 𝑥 ∈ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹})))
154	153	ss2rabdv 3891	. . . . . . . . . . 11 ⊢ (𝐴 ∈ dom vol → {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ⊆ {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹})})
155		dfdif2 3789	. . . . . . . . . . 11 ⊢ (𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹})) = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹})}
156	154, 155	syl6sseqr 3860	. . . . . . . . . 10 ⊢ (𝐴 ∈ dom vol → {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ⊆ (𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹})))
157	156, 133	jca 503	. . . . . . . . 9 ⊢ (𝐴 ∈ dom vol → ({𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ⊆ (𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹})) ∧ (𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹})) ⊆ ℝ))
158		ovolssnul 23491	. . . . . . . . . 10 ⊢ (({𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ⊆ (𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹})) ∧ (𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹})) ⊆ ℝ ∧ (vol‘(𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → (vol‘{𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)}) = 0)
159	158	3expa 1140	. . . . . . . . 9 ⊢ ((({𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ⊆ (𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹})) ∧ (𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹})) ⊆ ℝ) ∧ (vol‘(𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → (vol‘{𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)}) = 0)
160	157, 159	sylan 571	. . . . . . . 8 ⊢ ((𝐴 ∈ dom vol ∧ (vol‘(𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → (vol‘{𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)}) = 0)
161		nulmbl 23539	. . . . . . . 8 ⊢ (({𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ⊆ ℝ ∧ (vol*‘{𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)}) = 0) → {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ∈ dom vol)
162	145, 160, 161	syl2anc 575	. . . . . . 7 ⊢ ((𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ∈ dom vol)
163		unmbl 23541	. . . . . . 7 ⊢ (({𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} ∈ dom vol ∧ {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ∈ dom vol) → ({𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} ∪ {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)}) ∈ dom vol)
164	142, 162, 163	syl2anc 575	. . . . . 6 ⊢ ((𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → ({𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} ∪ {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)}) ∈ dom vol)
165	164	3adant1 1153	. . . . 5 ⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → ({𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} ∪ {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)}) ∈ dom vol)
166	165	adantr 468	. . . 4 ⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) ∧ 𝑏 ∈ ran (,)) → ({𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,)) ↾_t 𝐴)(𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} ∪ {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)}) ∈ dom vol)
167	45, 166	eqeltrd 2896	. . 3 ⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) ∧ 𝑏 ∈ ran (,)) → (^◡𝐹 “ 𝑏) ∈ dom vol)
168	167	ralrimiva 3165	. 2 ⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → ∀𝑏 ∈ ran (,)(^◡𝐹 “ 𝑏) ∈ dom vol)
169		ismbf 23632	. . 3 ⊢ (𝐹:𝐴⟶ℝ → (𝐹 ∈ MblFn ↔ ∀𝑏 ∈ ran (,)(^◡𝐹 “ 𝑏) ∈ dom vol))
170	169	3ad2ant1 1156	. 2 ⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → (𝐹 ∈ MblFn ↔ ∀𝑏 ∈ ran (,)(^◡𝐹 “ 𝑏) ∈ dom vol))
171	168, 170	mpbird 248	1 ⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((^◡(((topGen‘ran (,)) ↾_t 𝐴) CnP (topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → 𝐹 ∈ MblFn)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 197 ∧ wa 384 ∨ wo 865 ∧ w3a 1100 = wceq 1637 ∈ wcel 2157 {cab 2803 ∀wral 3107 ∃wrex 3108 {crab 3111 ∖ cdif 3777 ∪ cun 3778 ∩ cin 3779 ⊆ wss 3780 ∅c0 4127 ifcif 4290 𝒫 cpw 4362 {csn 4381 ∪ ciun 4723 class class class wbr 4855 ↦ cmpt 4934 E cep 5236 ^◡ccnv 5323 dom cdm 5324 ran crn 5325 “ cima 5327 ∘ ccom 5328 Rel wrel 5329 Fn wfn 6106 ⟶wf 6107 ‘cfv 6111 (class class class)co 6884 ↑_𝑚 cmap 8102 ℝcr 10230 0cc0 10231 (,)cioo 12413 ↾_t crest 16306 topGenctg 16323 Topctop 20932 TopOnctopon 20949 TopBasesctb 20984 CnP ccnp 21264 vol*covol 23466 volcvol 23467 MblFncmbf 23618

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1877 ax-4 1894 ax-5 2001 ax-6 2069 ax-7 2105 ax-8 2159 ax-9 2166 ax-10 2186 ax-11 2202 ax-12 2215 ax-13 2422 ax-ext 2795 ax-rep 4977 ax-sep 4988 ax-nul 4996 ax-pow 5048 ax-pr 5109 ax-un 7189 ax-inf2 8795 ax-cnex 10287 ax-resscn 10288 ax-1cn 10289 ax-icn 10290 ax-addcl 10291 ax-addrcl 10292 ax-mulcl 10293 ax-mulrcl 10294 ax-mulcom 10295 ax-addass 10296 ax-mulass 10297 ax-distr 10298 ax-i2m1 10299 ax-1ne0 10300 ax-1rid 10301 ax-rnegex 10302 ax-rrecex 10303 ax-cnre 10304 ax-pre-lttri 10305 ax-pre-lttrn 10306 ax-pre-ltadd 10307 ax-pre-mulgt0 10308 ax-pre-sup 10309

This theorem depends on definitions: df-bi 198 df-an 385 df-or 866 df-3or 1101 df-3an 1102 df-tru 1641 df-fal 1651 df-ex 1860 df-nf 1864 df-sb 2062 df-mo 2635 df-eu 2642 df-clab 2804 df-cleq 2810 df-clel 2813 df-nfc 2948 df-ne 2990 df-nel 3093 df-ral 3112 df-rex 3113 df-reu 3114 df-rmo 3115 df-rab 3116 df-v 3404 df-sbc 3645 df-csb 3740 df-dif 3783 df-un 3785 df-in 3787 df-ss 3794 df-pss 3796 df-nul 4128 df-if 4291 df-pw 4364 df-sn 4382 df-pr 4384 df-tp 4386 df-op 4388 df-uni 4642 df-int 4681 df-iun 4725 df-disj 4824 df-br 4856 df-opab 4918 df-mpt 4935 df-tr 4958 df-id 5232 df-eprel 5237 df-po 5245 df-so 5246 df-fr 5283 df-se 5284 df-we 5285 df-xp 5330 df-rel 5331 df-cnv 5332 df-co 5333 df-dm 5334 df-rn 5335 df-res 5336 df-ima 5337 df-pred 5907 df-ord 5953 df-on 5954 df-lim 5955 df-suc 5956 df-iota 6074 df-fun 6113 df-fn 6114 df-f 6115 df-f1 6116 df-fo 6117 df-f1o 6118 df-fv 6119 df-isom 6120 df-riota 6845 df-ov 6887 df-oprab 6888 df-mpt2 6889 df-of 7137 df-om 7306 df-1st 7408 df-2nd 7409 df-wrecs 7652 df-recs 7714 df-rdg 7752 df-1o 7806 df-2o 7807 df-oadd 7810 df-omul 7811 df-er 7989 df-map 8104 df-pm 8105 df-en 8203 df-dom 8204 df-sdom 8205 df-fin 8206 df-fi 8566 df-sup 8597 df-inf 8598 df-oi 8664 df-card 9058 df-acn 9061 df-cda 9285 df-pnf 10371 df-mnf 10372 df-xr 10373 df-ltxr 10374 df-le 10375 df-sub 10563 df-neg 10564 df-div 10980 df-nn 11316 df-2 11376 df-3 11377 df-4 11378 df-n0 11580 df-z 11664 df-uz 11925 df-q 12028 df-rp 12067 df-xneg 12182 df-xadd 12183 df-xmul 12184 df-ioo 12417 df-ico 12419 df-icc 12420 df-fz 12570 df-fzo 12710 df-fl 12837 df-seq 13045 df-exp 13104 df-hash 13358 df-cj 14082 df-re 14083 df-im 14084 df-sqrt 14218 df-abs 14219 df-clim 14462 df-rlim 14463 df-sum 14660 df-rest 16308 df-topgen 16329 df-psmet 19966 df-xmet 19967 df-met 19968 df-bl 19969 df-mopn 19970 df-top 20933 df-topon 20950 df-bases 20985 df-cnp 21267 df-cmp 21425 df-ovol 23468 df-vol 23469 df-mbf 23623

This theorem is referenced by: (None)

W3C validator