Theorem issmflem 47333

Description: The predicate "𝐹 is a real-valued measurable function w.r.t. to the sigma-algebra 𝑆". A function is measurable iff the preimages of all open intervals unbounded below are in the subspace sigma-algebra induced by its domain. The domain of 𝐹 is required to be a subset of the underlying set of 𝑆. Definition 121C of [Fremlin1] p. 36, and Proposition 121B (i) of [Fremlin1] p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)

Hypotheses

Ref	Expression
issmflem.s	⊢ (𝜑 → 𝑆 ∈ SAlg)
issmflem.d	⊢ 𝐷 = dom 𝐹

Assertion

Ref	Expression
issmflem	⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) ↔ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))))

Distinct variable groups:   𝐷,𝑎,𝑥   𝐹,𝑎,𝑥   𝑆,𝑎,𝑥   𝜑,𝑎,𝑥

Proof of Theorem issmflem

Dummy variables 𝑓 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 489	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹 ∈ (SMblFn‘𝑆))
2		df-smblfn 47302	. . . . . . . . 9 ⊢ SMblFn = (𝑠 ∈ SAlg ↦ {𝑓 ∈ (ℝ ↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)})
3		unieq 4887	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑆 → ∪ 𝑠 = ∪ 𝑆)
4	3	oveq2d 7427	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑆 → (ℝ ↑pm ∪ 𝑠) = (ℝ ↑pm ∪ 𝑆))
5	4	rabeqdv 3438	. . . . . . . . . 10 ⊢ (𝑠 = 𝑆 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)} = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)})
6		oveq1 7418	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑆 → (𝑠 ↾t dom 𝑓) = (𝑆 ↾t dom 𝑓))
7	6	eleq2d 2855	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑆 → ((◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓) ↔ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)))
8	7	ralbidv 3194	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑆 → (∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓) ↔ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)))
9	8	rabbidv 3430	. . . . . . . . . 10 ⊢ (𝑠 = 𝑆 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)} = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
10	5, 9	eqtrd 2804	. . . . . . . . 9 ⊢ (𝑠 = 𝑆 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)} = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
11		issmflem.s	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ SAlg)
12		ovex 7444	. . . . . . . . . . 11 ⊢ (ℝ ↑pm ∪ 𝑆) ∈ V
13	12	rabex 5310	. . . . . . . . . 10 ⊢ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} ∈ V
14	13	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} ∈ V)
15	2, 10, 11, 14	fvmptd3 7014	. . . . . . . 8 ⊢ (𝜑 → (SMblFn‘𝑆) = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
16	15	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (SMblFn‘𝑆) = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
17	1, 16	eleqtrd 2871	. . . . . 6 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
18		elrabi 3655	. . . . . 6 ⊢ (𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆))
19	17, 18	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆))
20		issmflem.d	. . . . . . 7 ⊢ 𝐷 = dom 𝐹
21		elpmi2 45833	. . . . . . 7 ⊢ (𝐹 ∈ (ℝ ↑pm ∪ 𝑆) → dom 𝐹 ⊆ ∪ 𝑆)
22	20, 21	eqsstrid 3983	. . . . . 6 ⊢ (𝐹 ∈ (ℝ ↑pm ∪ 𝑆) → 𝐷 ⊆ ∪ 𝑆)
23	22	adantl 486	. . . . 5 ⊢ ((𝜑 ∧ 𝐹 ∈ (ℝ ↑pm ∪ 𝑆)) → 𝐷 ⊆ ∪ 𝑆)
24	19, 23	syldan 602	. . . 4 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐷 ⊆ ∪ 𝑆)
25		elpmi 8843	. . . . . . 7 ⊢ (𝐹 ∈ (ℝ ↑pm ∪ 𝑆) → (𝐹:dom 𝐹⟶ℝ ∧ dom 𝐹 ⊆ ∪ 𝑆))
26	19, 25	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (𝐹:dom 𝐹⟶ℝ ∧ dom 𝐹 ⊆ ∪ 𝑆))
27	26	simpld 499	. . . . 5 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹:dom 𝐹⟶ℝ)
28	20	feq2i 6698	. . . . . 6 ⊢ (𝐹:𝐷⟶ℝ ↔ 𝐹:dom 𝐹⟶ℝ)
29	28	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (𝐹:𝐷⟶ℝ ↔ 𝐹:dom 𝐹⟶ℝ))
30	27, 29	mpbird 260	. . . 4 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹:𝐷⟶ℝ)
31		cnveq 5860	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → ◡𝑓 = ◡𝐹)
32	31	imaeq1d 6062	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → (◡𝑓 “ (-∞(,)𝑎)) = (◡𝐹 “ (-∞(,)𝑎)))
33		dmeq 5894	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
34	33	oveq2d 7427	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → (𝑆 ↾t dom 𝑓) = (𝑆 ↾t dom 𝐹))
35	32, 34	eleq12d 2863	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → ((◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓) ↔ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
36	35	ralbidv 3194	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓) ↔ ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
37	36	elrab 3659	. . . . . . . . . 10 ⊢ (𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} ↔ (𝐹 ∈ (ℝ ↑pm ∪ 𝑆) ∧ ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
38	37	simprbi 502	. . . . . . . . 9 ⊢ (𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
39	17, 38	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
40	39	adantr 485	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
41		simpr 489	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ)
42		rspa 3260	. . . . . . 7 ⊢ ((∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹) ∧ 𝑎 ∈ ℝ) → (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
43	40, 41, 42	syl2anc 595	. . . . . 6 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
44	30	adantr 485	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → 𝐹:𝐷⟶ℝ)
45		simpl 487	. . . . . . . . . 10 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → 𝐹:𝐷⟶ℝ)
46		simpr 489	. . . . . . . . . . 11 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ)
47	46	rexrd 11259	. . . . . . . . . 10 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ*)
48	45, 47	preimaioomnf 47325	. . . . . . . . 9 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → (◡𝐹 “ (-∞(,)𝑎)) = {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎})
49	48	eqcomd 2775	. . . . . . . 8 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} = (◡𝐹 “ (-∞(,)𝑎)))
50	44, 41, 49	syl2anc 595	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} = (◡𝐹 “ (-∞(,)𝑎)))
51	20	oveq2i 7422	. . . . . . . 8 ⊢ (𝑆 ↾t 𝐷) = (𝑆 ↾t dom 𝐹)
52	51	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → (𝑆 ↾t 𝐷) = (𝑆 ↾t dom 𝐹))
53	50, 52	eleq12d 2863	. . . . . 6 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → ({𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
54	43, 53	mpbird 260	. . . . 5 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))
55	54	ralrimiva 3163	. . . 4 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))
56	24, 30, 55	3jca 1144	. . 3 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷)))
57	56	ex 417	. 2 ⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) → (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))))
58		reex 11191	. . . . . . . . 9 ⊢ ℝ ∈ V
59	58	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → ℝ ∈ V)
60	11	uniexd 7741	. . . . . . . . 9 ⊢ (𝜑 → ∪ 𝑆 ∈ V)
61	60	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → ∪ 𝑆 ∈ V)
62		simprr 784	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → 𝐹:𝐷⟶ℝ)
63		fssxp 6734	. . . . . . . . . . . 12 ⊢ (𝐹:𝐷⟶ℝ → 𝐹 ⊆ (𝐷 × ℝ))
64	63	adantl 486	. . . . . . . . . . 11 ⊢ ((𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ) → 𝐹 ⊆ (𝐷 × ℝ))
65		xpss1 5681	. . . . . . . . . . . 12 ⊢ (𝐷 ⊆ ∪ 𝑆 → (𝐷 × ℝ) ⊆ (∪ 𝑆 × ℝ))
66	65	adantr 485	. . . . . . . . . . 11 ⊢ ((𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ) → (𝐷 × ℝ) ⊆ (∪ 𝑆 × ℝ))
67	64, 66	sstrd 3955	. . . . . . . . . 10 ⊢ ((𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ) → 𝐹 ⊆ (∪ 𝑆 × ℝ))
68	67	adantl 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → 𝐹 ⊆ (∪ 𝑆 × ℝ))
69		dmss 5893	. . . . . . . . . . . 12 ⊢ (𝐹 ⊆ (∪ 𝑆 × ℝ) → dom 𝐹 ⊆ dom (∪ 𝑆 × ℝ))
70		dmxpss 6170	. . . . . . . . . . . . 13 ⊢ dom (∪ 𝑆 × ℝ) ⊆ ∪ 𝑆
71	70	a1i 11	. . . . . . . . . . . 12 ⊢ (𝐹 ⊆ (∪ 𝑆 × ℝ) → dom (∪ 𝑆 × ℝ) ⊆ ∪ 𝑆)
72	69, 71	sstrd 3955	. . . . . . . . . . 11 ⊢ (𝐹 ⊆ (∪ 𝑆 × ℝ) → dom 𝐹 ⊆ ∪ 𝑆)
73	72	adantl 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐹 ⊆ (∪ 𝑆 × ℝ)) → dom 𝐹 ⊆ ∪ 𝑆)
74	20, 73	eqsstrid 3983	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐹 ⊆ (∪ 𝑆 × ℝ)) → 𝐷 ⊆ ∪ 𝑆)
75	68, 74	syldan 602	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → 𝐷 ⊆ ∪ 𝑆)
76		elpm2r 8842	. . . . . . . 8 ⊢ (((ℝ ∈ V ∧ ∪ 𝑆 ∈ V) ∧ (𝐹:𝐷⟶ℝ ∧ 𝐷 ⊆ ∪ 𝑆)) → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆))
77	59, 61, 62, 75, 76	syl22anc 851	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆))
78	77	3adantr3 1188	. . . . . 6 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆))
79	20	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → 𝐷 = dom 𝐹)
80	79	oveq2d 7427	. . . . . . . . . . . 12 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → (𝑆 ↾t 𝐷) = (𝑆 ↾t dom 𝐹))
81	49, 80	eleq12d 2863	. . . . . . . . . . 11 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → ({𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
82	81	ralbidva 3192	. . . . . . . . . 10 ⊢ (𝐹:𝐷⟶ℝ → (∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷) ↔ ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
83	82	biimpd 232	. . . . . . . . 9 ⊢ (𝐹:𝐷⟶ℝ → (∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
84	83	imp 411	. . . . . . . 8 ⊢ ((𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷)) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
85	84	adantl 486	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
86	85	3adantr1 1186	. . . . . 6 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
87	78, 86	jca 520	. . . . 5 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → (𝐹 ∈ (ℝ ↑pm ∪ 𝑆) ∧ ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
88	87, 37	sylibr 237	. . . 4 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → 𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
89	15	eqcomd 2775	. . . . 5 ⊢ (𝜑 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} = (SMblFn‘𝑆))
90	89	adantr 485	. . . 4 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} = (SMblFn‘𝑆))
91	88, 90	eleqtrd 2871	. . 3 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → 𝐹 ∈ (SMblFn‘𝑆))
92	91	ex 417	. 2 ⊢ (𝜑 → ((𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷)) → 𝐹 ∈ (SMblFn‘𝑆)))
93	57, 92	impbid 215	1 ⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) ↔ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149  ∀wral 3085  {crab 3423  Vcvv 3463   ⊆ wss 3913  ∪ cuni 4876   class class class wbr 5113   × cxp 5660  ^◡ccnv 5661  dom cdm 5662   “ cima 5665  ⟶wf 6533  ‘cfv 6537  (class class class)co 7411   ↑_pm cpm 8825  ℝcr 11099  -∞cmnf 11241   < clt 11243  (,)cioo 13372   ↾_t crest 17473  SAlgcsalg 46914  SMblFncsmblfn 47301

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-cnex 11156  ax-resscn 11157  ax-pre-lttri 11174  ax-pre-lttrn 11175

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-po 5570  df-so 5571  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7986  df-2nd 7987  df-er 8694  df-pm 8827  df-en 8944  df-dom 8945  df-sdom 8946  df-pnf 11245  df-mnf 11246  df-xr 11247  df-ltxr 11248  df-le 11249  df-ioo 13376  df-ico 13378  df-smblfn 47302

This theorem is referenced by:  issmf  47334