mbfsup - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > mbfsup		Structured version Visualization version GIF version

Theorem mbfsup 25874

Description: The supremum of a sequence of measurable, real-valued functions is measurable. Note that in this and related theorems, 𝐵(𝑛, 𝑥) is a function of both 𝑛 and 𝑥, since it is an 𝑛-indexed sequence of functions on 𝑥. (Contributed by Mario Carneiro, 14-Aug-2014.) (Revised by Mario Carneiro, 7-Sep-2014.)

**Hypotheses**
Ref	Expression
mbfsup.1	⊢ 𝑍 = (ℤ_≥‘𝑀)
mbfsup.2	⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ))
mbfsup.3	⊢ (𝜑 → 𝑀 ∈ ℤ)
mbfsup.4	⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
mbfsup.5	⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ ℝ)
mbfsup.6	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝐵 ≤ 𝑦)

**Assertion**
Ref	Expression
mbfsup	⊢ (𝜑 → 𝐺 ∈ MblFn)

Distinct variable groups: 𝑥,𝑛,𝑦,𝐴 𝑦,𝐵 𝜑,𝑛,𝑥,𝑦 𝑛,𝑍,𝑥,𝑦 Allowed substitution hints: 𝐵(𝑥, 𝑛) 𝐺(𝑥, 𝑦, 𝑛) 𝑀(𝑥, 𝑦, 𝑛)

Proof of Theorem mbfsup Dummy variables 𝑚 𝑧 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mbfsup.5	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ ℝ)
2	1	anassrs 473	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)
3	2	an32s 665	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → 𝐵 ∈ ℝ)
4	3	fmpttd 7114	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵):𝑍⟶ℝ)
5	4	frnd 6718	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝑛 ∈ 𝑍 ↦ 𝐵) ⊆ ℝ)
6		mbfsup.3	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℤ)
7		uzid 12893	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ_≥‘𝑀))
8	6, 7	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘𝑀))
9		mbfsup.1	. . . . . . . . 9 ⊢ 𝑍 = (ℤ_≥‘𝑀)
10	8, 9	eleqtrrdi 2876	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ 𝑍)
11	10	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑀 ∈ 𝑍)
12		eqid 2765	. . . . . . . 8 ⊢ (𝑛 ∈ 𝑍 ↦ 𝐵) = (𝑛 ∈ 𝑍 ↦ 𝐵)
13	12, 3	dmmptd 6684	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom (𝑛 ∈ 𝑍 ↦ 𝐵) = 𝑍)
14	11, 13	eleqtrrd 2868	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑀 ∈ dom (𝑛 ∈ 𝑍 ↦ 𝐵))
15	14	ne0d 4295	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom (𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅)
16		dm0rn0 5916	. . . . . 6 ⊢ (dom (𝑛 ∈ 𝑍 ↦ 𝐵) = ∅ ↔ ran (𝑛 ∈ 𝑍 ↦ 𝐵) = ∅)
17	16	necon3bii 3012	. . . . 5 ⊢ (dom (𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅ ↔ ran (𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅)
18	15, 17	sylib 221	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅)
19		mbfsup.6	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝐵 ≤ 𝑦)
20	4	ffnd 6710	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵) Fn 𝑍)
21		breq1 5114	. . . . . . . . 9 ⊢ (𝑧 = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) → (𝑧 ≤ 𝑦 ↔ ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ≤ 𝑦))
22	21	ralrn 7087	. . . . . . . 8 ⊢ ((𝑛 ∈ 𝑍 ↦ 𝐵) Fn 𝑍 → (∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∀𝑚 ∈ 𝑍 ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ≤ 𝑦))
23	20, 22	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∀𝑚 ∈ 𝑍 ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ≤ 𝑦))
24		nffvmpt1 6896	. . . . . . . . . 10 ⊢ Ⅎ𝑛((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚)
25		nfcv 2927	. . . . . . . . . 10 ⊢ Ⅎ𝑛 ≤
26		nfcv 2927	. . . . . . . . . 10 ⊢ Ⅎ𝑛𝑦
27	24, 25, 26	nfbr 5160	. . . . . . . . 9 ⊢ Ⅎ𝑛((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ≤ 𝑦
28		nfv 1947	. . . . . . . . 9 ⊢ Ⅎ𝑚((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ≤ 𝑦
29		fveq2 6885	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛))
30	29	breq1d 5121	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ≤ 𝑦 ↔ ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ≤ 𝑦))
31	27, 28, 30	cbvralw 3309	. . . . . . . 8 ⊢ (∀𝑚 ∈ 𝑍 ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ≤ 𝑦 ↔ ∀𝑛 ∈ 𝑍 ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ≤ 𝑦)
32		simpr 490	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝑍)
33	12	fvmpt2 7005	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ 𝑍 ∧ 𝐵 ∈ ℝ) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) = 𝐵)
34	32, 3, 33	syl2anc 596	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) = 𝐵)
35	34	breq1d 5121	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → (((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ≤ 𝑦 ↔ 𝐵 ≤ 𝑦))
36	35	ralbidva 3188	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑛 ∈ 𝑍 ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ≤ 𝑦 ↔ ∀𝑛 ∈ 𝑍 𝐵 ≤ 𝑦))
37	31, 36	bitrid 286	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑚 ∈ 𝑍 ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ≤ 𝑦 ↔ ∀𝑛 ∈ 𝑍 𝐵 ≤ 𝑦))
38	23, 37	bitrd 282	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∀𝑛 ∈ 𝑍 𝐵 ≤ 𝑦))
39	38	rexbidv 3191	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝐵 ≤ 𝑦))
40	19, 39	mpbird 260	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦)
41	5, 18, 40	suprcld 12193	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ) ∈ ℝ)
42		mbfsup.2	. . 3 ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ))
43	41, 42	fmptd 7113	. 2 ⊢ (𝜑 → 𝐺:𝐴⟶ℝ)
44		simpr 490	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
45		ltso 11305	. . . . . . . . . . . . . 14 ⊢ < Or ℝ
46	45	supex 9431	. . . . . . . . . . . . 13 ⊢ sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ) ∈ V
47	42	fvmpt2 7005	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐴 ∧ sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ) ∈ V) → (𝐺‘𝑥) = sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ))
48	44, 46, 47	sylancl 598	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ))
49	48	breq2d 5123	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝑡 < (𝐺‘𝑥) ↔ 𝑡 < sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < )))
50	5, 18, 40	3jca 1146	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ran (𝑛 ∈ 𝑍 ↦ 𝐵) ⊆ ℝ ∧ ran (𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦))
51	50	adantlr 728	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (ran (𝑛 ∈ 𝑍 ↦ 𝐵) ⊆ ℝ ∧ ran (𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦))
52		simplr 781	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑡 ∈ ℝ)
53		suprlub 12194	. . . . . . . . . . . 12 ⊢ (((ran (𝑛 ∈ 𝑍 ↦ 𝐵) ⊆ ℝ ∧ ran (𝑛 ∈ 𝑍 ↦ 𝐵) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑧 ≤ 𝑦) ∧ 𝑡 ∈ ℝ) → (𝑡 < sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ) ↔ ∃𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑡 < 𝑧))
54	51, 52, 53	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝑡 < sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ) ↔ ∃𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑡 < 𝑧))
55	20	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵) Fn 𝑍)
56		breq2 5115	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) → (𝑡 < 𝑧 ↔ 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚)))
57	56	rexrn 7086	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ 𝑍 ↦ 𝐵) Fn 𝑍 → (∃𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑡 < 𝑧 ↔ ∃𝑚 ∈ 𝑍 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚)))
58	55, 57	syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (∃𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑡 < 𝑧 ↔ ∃𝑚 ∈ 𝑍 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚)))
59		nfcv 2927	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛𝑡
60		nfcv 2927	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛 <
61	59, 60, 24	nfbr 5160	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚)
62		nfv 1947	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑚 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛)
63	29	breq2d 5123	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑛 → (𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ↔ 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛)))
64	61, 62, 63	cbvrexw 3310	. . . . . . . . . . . . 13 ⊢ (∃𝑚 ∈ 𝑍 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛))
65	12	fvmpt2i 7004	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ 𝑍 → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) = ( I ‘𝐵))
66		eqid 2765	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
67	66	fvmpt2i 7004	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = ( I ‘𝐵))
68	67	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = ( I ‘𝐵))
69	68	eqcomd 2771	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ( I ‘𝐵) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))
70	65, 69	sylan9eqr 2822	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))
71	70	breq2d 5123	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → (𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ↔ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)))
72	71	rexbidva 3189	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑛 ∈ 𝑍 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)))
73	72	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (∃𝑛 ∈ 𝑍 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑛) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)))
74	64, 73	bitrid 286	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (∃𝑚 ∈ 𝑍 𝑡 < ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑚) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)))
75	58, 74	bitrd 282	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (∃𝑧 ∈ ran (𝑛 ∈ 𝑍 ↦ 𝐵)𝑡 < 𝑧 ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)))
76	49, 54, 75	3bitrd 308	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝑡 < (𝐺‘𝑥) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)))
77	76	ralrimiva 3159	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ∀𝑥 ∈ 𝐴 (𝑡 < (𝐺‘𝑥) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)))
78		nfv 1947	. . . . . . . . . 10 ⊢ Ⅎ𝑧(𝑡 < (𝐺‘𝑥) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))
79		nfcv 2927	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥𝑡
80		nfcv 2927	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 <
81		nfmpt1 5212	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ))
82	42, 81	nfcxfr 2925	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥𝐺
83		nfcv 2927	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥𝑧
84	82, 83	nffv 6895	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(𝐺‘𝑧)
85	79, 80, 84	nfbr 5160	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑡 < (𝐺‘𝑧)
86		nfcv 2927	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥𝑍
87		nffvmpt1 6896	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)
88	79, 80, 87	nfbr 5160	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)
89	86, 88	nfrexw 3315	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)
90	85, 89	nfbi 1936	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑡 < (𝐺‘𝑧) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))
91		fveq2 6885	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (𝐺‘𝑥) = (𝐺‘𝑧))
92	91	breq2d 5123	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (𝑡 < (𝐺‘𝑥) ↔ 𝑡 < (𝐺‘𝑧)))
93		fveq2 6885	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))
94	93	breq2d 5123	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ↔ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)))
95	94	rexbidv 3191	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)))
96	92, 95	bibi12d 348	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → ((𝑡 < (𝐺‘𝑥) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ↔ (𝑡 < (𝐺‘𝑧) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))))
97	78, 90, 96	cbvralw 3309	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 (𝑡 < (𝐺‘𝑥) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ↔ ∀𝑧 ∈ 𝐴 (𝑡 < (𝐺‘𝑧) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)))
98	77, 97	sylib 221	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ∀𝑧 ∈ 𝐴 (𝑡 < (𝐺‘𝑧) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)))
99	98	r19.21bi 3259	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → (𝑡 < (𝐺‘𝑧) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)))
100	43	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 𝐺:𝐴⟶ℝ)
101	100	ffvelcdmda 7083	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) ∈ ℝ)
102		rexr 11270	. . . . . . . . . 10 ⊢ (𝑡 ∈ ℝ → 𝑡 ∈ ℝ^*)
103	102	ad2antlr 740	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → 𝑡 ∈ ℝ^*)
104		elioopnf 13486	. . . . . . . . 9 ⊢ (𝑡 ∈ ℝ^* → ((𝐺‘𝑧) ∈ (𝑡(,)+∞) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ 𝑡 < (𝐺‘𝑧))))
105	103, 104	syl 18	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑡(,)+∞) ↔ ((𝐺‘𝑧) ∈ ℝ ∧ 𝑡 < (𝐺‘𝑧))))
106	101, 105	mpbirand 720	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑡(,)+∞) ↔ 𝑡 < (𝐺‘𝑧)))
107	103	adantr 486	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → 𝑡 ∈ ℝ^*)
108		elioopnf 13486	. . . . . . . . . 10 ⊢ (𝑡 ∈ ℝ^* → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞) ↔ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ ℝ ∧ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))))
109	107, 108	syl 18	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞) ↔ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ ℝ ∧ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))))
110	2	fmpttd 7114	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ)
111	110	ffvelcdmda 7083	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑧 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ ℝ)
112	111	biantrurd 542	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑧 ∈ 𝐴) → (𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ↔ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ ℝ ∧ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))))
113	112	an32s 665	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → (𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ↔ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ ℝ ∧ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))))
114	113	adantllr 732	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → (𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ↔ (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ ℝ ∧ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧))))
115	109, 114	bitr4d 285	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) ∧ 𝑛 ∈ 𝑍) → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞) ↔ 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)))
116	115	rexbidva 3189	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → (∃𝑛 ∈ 𝑍 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞) ↔ ∃𝑛 ∈ 𝑍 𝑡 < ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧)))
117	99, 106, 116	3bitr4d 314	. . . . . 6 ⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) ∈ (𝑡(,)+∞) ↔ ∃𝑛 ∈ 𝑍 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞)))
118	117	pm5.32da 590	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ((𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ∃𝑛 ∈ 𝑍 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞))))
119	43	ffnd 6710	. . . . . . 7 ⊢ (𝜑 → 𝐺 Fn 𝐴)
120	119	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 𝐺 Fn 𝐴)
121		elpreima 7057	. . . . . 6 ⊢ (𝐺 Fn 𝐴 → (𝑧 ∈ (^◡𝐺 “ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑡(,)+∞))))
122	120, 121	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (𝑧 ∈ (^◡𝐺 “ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (𝐺‘𝑧) ∈ (𝑡(,)+∞))))
123		eliun 4962	. . . . . 6 ⊢ (𝑧 ∈ ∪ 𝑛 ∈ 𝑍 (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ↔ ∃𝑛 ∈ 𝑍 𝑧 ∈ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)))
124	110	ffnd 6710	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴)
125		elpreima 7057	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴 → (𝑧 ∈ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞))))
126	124, 125	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑧 ∈ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞))))
127	126	rexbidva 3189	. . . . . . . 8 ⊢ (𝜑 → (∃𝑛 ∈ 𝑍 𝑧 ∈ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ↔ ∃𝑛 ∈ 𝑍 (𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞))))
128	127	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (∃𝑛 ∈ 𝑍 𝑧 ∈ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ↔ ∃𝑛 ∈ 𝑍 (𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞))))
129		r19.42v 3199	. . . . . . 7 ⊢ (∃𝑛 ∈ 𝑍 (𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ∃𝑛 ∈ 𝑍 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞)))
130	128, 129	bitrdi 290	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (∃𝑛 ∈ 𝑍 𝑧 ∈ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ∃𝑛 ∈ 𝑍 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞))))
131	123, 130	bitrid 286	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (𝑧 ∈ ∪ 𝑛 ∈ 𝑍 (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ ∃𝑛 ∈ 𝑍 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑧) ∈ (𝑡(,)+∞))))
132	118, 122, 131	3bitr4d 314	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (𝑧 ∈ (^◡𝐺 “ (𝑡(,)+∞)) ↔ 𝑧 ∈ ∪ 𝑛 ∈ 𝑍 (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞))))
133	132	eqrdv 2763	. . 3 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (^◡𝐺 “ (𝑡(,)+∞)) = ∪ 𝑛 ∈ 𝑍 (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)))
134		zex 12615	. . . . . . 7 ⊢ ℤ ∈ V
135		uzssz 12899	. . . . . . 7 ⊢ (ℤ_≥‘𝑀) ⊆ ℤ
136		ssdomg 9003	. . . . . . 7 ⊢ (ℤ ∈ V → ((ℤ_≥‘𝑀) ⊆ ℤ → (ℤ_≥‘𝑀) ≼ ℤ))
137	134, 135, 136	mp2 9	. . . . . 6 ⊢ (ℤ_≥‘𝑀) ≼ ℤ
138	9, 137	eqbrtri 5134	. . . . 5 ⊢ 𝑍 ≼ ℤ
139		znnen 16290	. . . . 5 ⊢ ℤ ≈ ℕ
140		domentr 9016	. . . . 5 ⊢ ((𝑍 ≼ ℤ ∧ ℤ ≈ ℕ) → 𝑍 ≼ ℕ)
141	138, 139, 140	mp2an 705	. . . 4 ⊢ 𝑍 ≼ ℕ
142		mbfsup.4	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
143		mbfima 25840	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ) → (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ∈ dom vol)
144	142, 110, 143	syl2anc 596	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ∈ dom vol)
145	144	ralrimiva 3159	. . . . 5 ⊢ (𝜑 → ∀𝑛 ∈ 𝑍 (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ∈ dom vol)
146	145	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ∀𝑛 ∈ 𝑍 (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ∈ dom vol)
147		iunmbl2 25767	. . . 4 ⊢ ((𝑍 ≼ ℕ ∧ ∀𝑛 ∈ 𝑍 (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ∈ dom vol) → ∪ 𝑛 ∈ 𝑍 (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ∈ dom vol)
148	141, 146, 147	sylancr 599	. . 3 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ∪ 𝑛 ∈ 𝑍 (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (𝑡(,)+∞)) ∈ dom vol)
149	133, 148	eqeltrd 2865	. 2 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (^◡𝐺 “ (𝑡(,)+∞)) ∈ dom vol)
150	43, 149	ismbf3d 25864	1 ⊢ (𝜑 → 𝐺 ∈ MblFn)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2146 ≠ wne 2960 ∀wral 3081 ∃wrex 3091 Vcvv 3457 ⊆ wss 3906 ∅c0 4286 ∪ ciun 4958 class class class wbr 5111 ↦ cmpt 5194 I cid 5557 ^◡ccnv 5662 dom cdm 5663 ran crn 5664 “ cima 5666 Fn wfn 6535 ⟶wf 6536 ‘cfv 6540 (class class class)co 7419 ≈ cen 8946 ≼ cdom 8947 supcsup 9407 ℝcr 11114 +∞cpnf 11255 ℝ^*cxr 11257 < clt 11258 ≤ cle 11259 ℕcn 12248 ℤcz 12606 ℤ_≥cuz 12878 (,)cioo 13388 volcvol 25673 MblFncmbf 25824

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-inf2 9617 ax-cc 10434 ax-cnex 11171 ax-resscn 11172 ax-1cn 11173 ax-icn 11174 ax-addcl 11175 ax-addrcl 11176 ax-mulcl 11177 ax-mulrcl 11178 ax-mulcom 11179 ax-addass 11180 ax-mulass 11181 ax-distr 11182 ax-i2m1 11183 ax-1ne0 11184 ax-1rid 11185 ax-rnegex 11186 ax-rrecex 11187 ax-cnre 11188 ax-pre-lttri 11189 ax-pre-lttrn 11190 ax-pre-ltadd 11191 ax-pre-mulgt0 11192 ax-pre-sup 11193

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-disj 5079 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 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-isom 6549 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-of 7684 df-om 7869 df-1st 7992 df-2nd 7993 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-oadd 8463 df-omul 8464 df-er 8700 df-map 8832 df-pm 8833 df-en 8950 df-dom 8951 df-sdom 8952 df-fin 8953 df-sup 9409 df-inf 9410 df-oi 9479 df-dju 9903 df-card 9941 df-acn 9944 df-pnf 11260 df-mnf 11261 df-xr 11262 df-ltxr 11263 df-le 11264 df-sub 11458 df-neg 11459 df-div 11887 df-nn 12249 df-2 12318 df-3 12319 df-n0 12520 df-z 12607 df-uz 12879 df-q 12989 df-rp 13033 df-xadd 13154 df-ioo 13392 df-ioc 13393 df-ico 13394 df-icc 13395 df-fz 13552 df-fzo 13700 df-fl 13843 df-seq 14056 df-exp 14116 df-hash 14385 df-cj 15174 df-re 15175 df-im 15176 df-sqrt 15310 df-abs 15311 df-clim 15563 df-rlim 15564 df-sum 15762 df-xmet 21565 df-met 21566 df-ovol 25674 df-vol 25675 df-mbf 25829

This theorem is used by: mbfinf 25875 mbflimsup 25876

W3C validator