Theorem smfrec 41517

Description: The reciprocal of a sigma-measurable functions is sigma-measurable. First part of Proposition 121E (e) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)

Hypotheses

Ref	Expression
smfrec.x	⊢ Ⅎ𝑥𝜑
smfrec.s	⊢ (𝜑 → 𝑆 ∈ SAlg)
smfrec.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
smfrec.b	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)
smfrec.m	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))
smfrec.e	⊢ 𝐶 = {𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 0}

Assertion

Ref	Expression
smfrec	⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (1 / 𝐵)) ∈ (SMblFn‘𝑆))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶

Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)   𝑆(𝑥)   𝑉(𝑥)

Proof of Theorem smfrec

Dummy variable 𝑎 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		smfrec.x	. 2 ⊢ Ⅎ𝑥𝜑
2		nfv 1995	. 2 ⊢ Ⅎ𝑎𝜑
3		smfrec.s	. 2 ⊢ (𝜑 → 𝑆 ∈ SAlg)
4		smfrec.e	. . . 4 ⊢ 𝐶 = {𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 0}
5		ssrab2 3837	. . . 4 ⊢ {𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 0} ⊆ 𝐴
6	4, 5	eqsstri 3785	. . 3 ⊢ 𝐶 ⊆ 𝐴
7		eqid 2771	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
8		smfrec.b	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)
9	1, 7, 8	dmmptdf 39936	. . . . 5 ⊢ (𝜑 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)
10	9	eqcomd 2777	. . . 4 ⊢ (𝜑 → 𝐴 = dom (𝑥 ∈ 𝐴 ↦ 𝐵))
11		smfrec.m	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))
12		eqid 2771	. . . . 5 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) = dom (𝑥 ∈ 𝐴 ↦ 𝐵)
13	3, 11, 12	smfdmss 41463	. . . 4 ⊢ (𝜑 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ ∪ 𝑆)
14	10, 13	eqsstrd 3789	. . 3 ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑆)
15	6, 14	syl5ss 3764	. 2 ⊢ (𝜑 → 𝐶 ⊆ ∪ 𝑆)
16		1red 10258	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 1 ∈ ℝ)
17	6	sseli 3749	. . . . 5 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐴)
18	17	adantl 467	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ 𝐴)
19	18, 8	syldan 573	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐵 ∈ ℝ)
20	4	eleq2i 2842	. . . . . 6 ⊢ (𝑥 ∈ 𝐶 ↔ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 0})
21	20	biimpi 206	. . . . 5 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 0})
22		rabidim2 39806	. . . . 5 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 0} → 𝐵 ≠ 0)
23	21, 22	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐶 → 𝐵 ≠ 0)
24	23	adantl 467	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐵 ≠ 0)
25	16, 19, 24	redivcld 11056	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (1 / 𝐵) ∈ ℝ)
26		nfv 1995	. . . . . . 7 ⊢ Ⅎ𝑥 𝑎 ∈ ℝ
27	1, 26	nfan 1980	. . . . . 6 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑎 ∈ ℝ)
28		nfv 1995	. . . . . 6 ⊢ Ⅎ𝑥0 < 𝑎
29	27, 28	nfan 1980	. . . . 5 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 0 < 𝑎)
30	19	ad4ant14 1208	. . . . 5 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 0 < 𝑎) ∧ 𝑥 ∈ 𝐶) → 𝐵 ∈ ℝ)
31	23	adantl 467	. . . . 5 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 0 < 𝑎) ∧ 𝑥 ∈ 𝐶) → 𝐵 ≠ 0)
32		simpl 468	. . . . . . 7 ⊢ ((𝑎 ∈ ℝ ∧ 0 < 𝑎) → 𝑎 ∈ ℝ)
33		simpr 471	. . . . . . 7 ⊢ ((𝑎 ∈ ℝ ∧ 0 < 𝑎) → 0 < 𝑎)
34	32, 33	elrpd 12073	. . . . . 6 ⊢ ((𝑎 ∈ ℝ ∧ 0 < 𝑎) → 𝑎 ∈ ℝ+)
35	34	adantll 687	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 0 < 𝑎) → 𝑎 ∈ ℝ+)
36	29, 30, 31, 35	pimrecltpos 41440	. . . 4 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 0 < 𝑎) → {𝑥 ∈ 𝐶 ∣ (1 / 𝐵) < 𝑎} = ({𝑥 ∈ 𝐶 ∣ (1 / 𝑎) < 𝐵} ∪ {𝑥 ∈ 𝐶 ∣ 𝐵 < 0}))
37		smfrec.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
38	4, 37	rabexd 4948	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ V)
39		eqid 2771	. . . . . . 7 ⊢ (𝑆 ↾t 𝐶) = (𝑆 ↾t 𝐶)
40	3, 38, 39	subsalsal 41095	. . . . . 6 ⊢ (𝜑 → (𝑆 ↾t 𝐶) ∈ SAlg)
41	40	ad2antrr 699	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 0 < 𝑎) → (𝑆 ↾t 𝐶) ∈ SAlg)
42	3	adantr 466	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝑆 ∈ SAlg)
43	42	adantr 466	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 0 < 𝑎) → 𝑆 ∈ SAlg)
44	6	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ⊆ 𝐴)
45	3, 11, 44	sssmfmpt 41480	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ 𝐵) ∈ (SMblFn‘𝑆))
46	45	adantr 466	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (𝑥 ∈ 𝐶 ↦ 𝐵) ∈ (SMblFn‘𝑆))
47	46	adantr 466	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 0 < 𝑎) → (𝑥 ∈ 𝐶 ↦ 𝐵) ∈ (SMblFn‘𝑆))
48	34	rprecred 12087	. . . . . . 7 ⊢ ((𝑎 ∈ ℝ ∧ 0 < 𝑎) → (1 / 𝑎) ∈ ℝ)
49	48	adantll 687	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 0 < 𝑎) → (1 / 𝑎) ∈ ℝ)
50	29, 43, 30, 47, 49	smfpimgtmpt 41510	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 0 < 𝑎) → {𝑥 ∈ 𝐶 ∣ (1 / 𝑎) < 𝐵} ∈ (𝑆 ↾t 𝐶))
51		0red 10244	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℝ)
52	1, 3, 19, 45, 51	smfpimltmpt 41476	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ 𝐶 ∣ 𝐵 < 0} ∈ (𝑆 ↾t 𝐶))
53	52	ad2antrr 699	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 0 < 𝑎) → {𝑥 ∈ 𝐶 ∣ 𝐵 < 0} ∈ (𝑆 ↾t 𝐶))
54	41, 50, 53	saluncld 41084	. . . 4 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 0 < 𝑎) → ({𝑥 ∈ 𝐶 ∣ (1 / 𝑎) < 𝐵} ∪ {𝑥 ∈ 𝐶 ∣ 𝐵 < 0}) ∈ (𝑆 ↾t 𝐶))
55	36, 54	eqeltrd 2850	. . 3 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 0 < 𝑎) → {𝑥 ∈ 𝐶 ∣ (1 / 𝐵) < 𝑎} ∈ (𝑆 ↾t 𝐶))
56		nfv 1995	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑎 = 0
57	1, 56	nfan 1980	. . . . . . 7 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑎 = 0)
58		breq2 4791	. . . . . . . . 9 ⊢ (𝑎 = 0 → ((1 / 𝐵) < 𝑎 ↔ (1 / 𝐵) < 0))
59	58	ad2antlr 700	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 = 0) ∧ 𝑥 ∈ 𝐶) → ((1 / 𝐵) < 𝑎 ↔ (1 / 𝐵) < 0))
60	19, 24	reclt0 40131	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐵 < 0 ↔ (1 / 𝐵) < 0))
61	60	bicomd 213	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((1 / 𝐵) < 0 ↔ 𝐵 < 0))
62	61	adantlr 688	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 = 0) ∧ 𝑥 ∈ 𝐶) → ((1 / 𝐵) < 0 ↔ 𝐵 < 0))
63	59, 62	bitrd 268	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 = 0) ∧ 𝑥 ∈ 𝐶) → ((1 / 𝐵) < 𝑎 ↔ 𝐵 < 0))
64	57, 63	rabbida 39796	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 = 0) → {𝑥 ∈ 𝐶 ∣ (1 / 𝐵) < 𝑎} = {𝑥 ∈ 𝐶 ∣ 𝐵 < 0})
65	52	adantr 466	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 = 0) → {𝑥 ∈ 𝐶 ∣ 𝐵 < 0} ∈ (𝑆 ↾t 𝐶))
66	64, 65	eqeltrd 2850	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 = 0) → {𝑥 ∈ 𝐶 ∣ (1 / 𝐵) < 𝑎} ∈ (𝑆 ↾t 𝐶))
67	66	ad4ant14 1208	. . . 4 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ¬ 0 < 𝑎) ∧ 𝑎 = 0) → {𝑥 ∈ 𝐶 ∣ (1 / 𝐵) < 𝑎} ∈ (𝑆 ↾t 𝐶))
68		simpll 744	. . . . 5 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ¬ 0 < 𝑎) ∧ ¬ 𝑎 = 0) → (𝜑 ∧ 𝑎 ∈ ℝ))
69		simpll 744	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ ¬ 0 < 𝑎) ∧ ¬ 𝑎 = 0) → 𝑎 ∈ ℝ)
70		0red 10244	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ ¬ 0 < 𝑎) ∧ ¬ 𝑎 = 0) → 0 ∈ ℝ)
71		neqne 2951	. . . . . . . 8 ⊢ (¬ 𝑎 = 0 → 𝑎 ≠ 0)
72	71	adantl 467	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ ¬ 0 < 𝑎) ∧ ¬ 𝑎 = 0) → 𝑎 ≠ 0)
73		simplr 746	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ ¬ 0 < 𝑎) ∧ ¬ 𝑎 = 0) → ¬ 0 < 𝑎)
74	69, 70, 72, 73	lttri5d 40031	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ ¬ 0 < 𝑎) ∧ ¬ 𝑎 = 0) → 𝑎 < 0)
75	74	adantlll 691	. . . . 5 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ¬ 0 < 𝑎) ∧ ¬ 𝑎 = 0) → 𝑎 < 0)
76		nfv 1995	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑎 < 0
77	27, 76	nfan 1980	. . . . . . 7 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0)
78	8	adantlr 688	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)
79	17, 78	sylan2 574	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑥 ∈ 𝐶) → 𝐵 ∈ ℝ)
80	79	adantlr 688	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) ∧ 𝑥 ∈ 𝐶) → 𝐵 ∈ ℝ)
81	23	adantl 467	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) ∧ 𝑥 ∈ 𝐶) → 𝐵 ≠ 0)
82		simpr 471	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ)
83	82	adantr 466	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) → 𝑎 ∈ ℝ)
84		simpr 471	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) → 𝑎 < 0)
85	77, 80, 81, 83, 84	pimrecltneg 41454	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) → {𝑥 ∈ 𝐶 ∣ (1 / 𝐵) < 𝑎} = {𝑥 ∈ 𝐶 ∣ 𝐵 ∈ ((1 / 𝑎)(,)0)})
86	42	adantr 466	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) → 𝑆 ∈ SAlg)
87	38	ad2antrr 699	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) → 𝐶 ∈ V)
88	46	adantr 466	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) → (𝑥 ∈ 𝐶 ↦ 𝐵) ∈ (SMblFn‘𝑆))
89		1red 10258	. . . . . . . . . 10 ⊢ ((𝑎 ∈ ℝ ∧ 𝑎 < 0) → 1 ∈ ℝ)
90		simpl 468	. . . . . . . . . 10 ⊢ ((𝑎 ∈ ℝ ∧ 𝑎 < 0) → 𝑎 ∈ ℝ)
91		lt0ne0 10697	. . . . . . . . . 10 ⊢ ((𝑎 ∈ ℝ ∧ 𝑎 < 0) → 𝑎 ≠ 0)
92	89, 90, 91	redivcld 11056	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑎 < 0) → (1 / 𝑎) ∈ ℝ)
93	92	adantll 687	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) → (1 / 𝑎) ∈ ℝ)
94	93	rexrd 10292	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) → (1 / 𝑎) ∈ ℝ*)
95	51	ad2antrr 699	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) → 0 ∈ ℝ)
96	95	rexrd 10292	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) → 0 ∈ ℝ*)
97	77, 86, 87, 80, 88, 94, 96	smfpimioompt 41514	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) → {𝑥 ∈ 𝐶 ∣ 𝐵 ∈ ((1 / 𝑎)(,)0)} ∈ (𝑆 ↾t 𝐶))
98	85, 97	eqeltrd 2850	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) → {𝑥 ∈ 𝐶 ∣ (1 / 𝐵) < 𝑎} ∈ (𝑆 ↾t 𝐶))
99	68, 75, 98	syl2anc 567	. . . 4 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ¬ 0 < 𝑎) ∧ ¬ 𝑎 = 0) → {𝑥 ∈ 𝐶 ∣ (1 / 𝐵) < 𝑎} ∈ (𝑆 ↾t 𝐶))
100	67, 99	pm2.61dan 807	. . 3 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ¬ 0 < 𝑎) → {𝑥 ∈ 𝐶 ∣ (1 / 𝐵) < 𝑎} ∈ (𝑆 ↾t 𝐶))
101	55, 100	pm2.61dan 807	. 2 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐶 ∣ (1 / 𝐵) < 𝑎} ∈ (𝑆 ↾t 𝐶))
102	1, 2, 3, 15, 25, 101	issmfdmpt 41478	1 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (1 / 𝐵)) ∈ (SMblFn‘𝑆))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 382   = wceq 1631  Ⅎwnf 1856   ∈ wcel 2145   ≠ wne 2943  {crab 3065  Vcvv 3351   ∪ cun 3722   ⊆ wss 3724  ∪ cuni 4575   class class class wbr 4787   ↦ cmpt 4864  dom cdm 5250  ‘cfv 6032  (class class class)co 6794  ℝcr 10138  0cc0 10139  1c1 10140   < clt 10277   / cdiv 10887  ℝ⁺crp 12036  (,)cioo 12381   ↾_t crest 16290  SAlgcsalg 41046  SMblFncsmblfn 41430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7097  ax-inf2 8703  ax-cc 9460  ax-ac2 9488  ax-cnex 10195  ax-resscn 10196  ax-1cn 10197  ax-icn 10198  ax-addcl 10199  ax-addrcl 10200  ax-mulcl 10201  ax-mulrcl 10202  ax-mulcom 10203  ax-addass 10204  ax-mulass 10205  ax-distr 10206  ax-i2m1 10207  ax-1ne0 10208  ax-1rid 10209  ax-rnegex 10210  ax-rrecex 10211  ax-cnre 10212  ax-pre-lttri 10213  ax-pre-lttrn 10214  ax-pre-ltadd 10215  ax-pre-mulgt0 10216  ax-pre-sup 10217

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3589  df-csb 3684  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-pss 3740  df-nul 4065  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-iin 4658  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-se 5210  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5824  df-ord 5870  df-on 5871  df-lim 5872  df-suc 5873  df-iota 5995  df-fun 6034  df-fn 6035  df-f 6036  df-f1 6037  df-fo 6038  df-f1o 6039  df-fv 6040  df-isom 6041  df-riota 6755  df-ov 6797  df-oprab 6798  df-mpt2 6799  df-om 7214  df-1st 7316  df-2nd 7317  df-wrecs 7560  df-recs 7622  df-rdg 7660  df-1o 7714  df-oadd 7718  df-er 7897  df-map 8012  df-pm 8013  df-en 8111  df-dom 8112  df-sdom 8113  df-fin 8114  df-sup 8505  df-inf 8506  df-card 8966  df-acn 8969  df-ac 9140  df-pnf 10279  df-mnf 10280  df-xr 10281  df-ltxr 10282  df-le 10283  df-sub 10471  df-neg 10472  df-div 10888  df-nn 11224  df-n0 11496  df-z 11581  df-uz 11890  df-q 11993  df-rp 12037  df-ioo 12385  df-ico 12387  df-fl 12802  df-rest 16292  df-salg 41047  df-smblfn 41431

This theorem is referenced by:  smfdiv  41525