Theorem issmflem 45429

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 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹 ∈ (SMblFn‘𝑆))
2		df-smblfn 45398	. . . . . . . . 9 ⊢ SMblFn = (𝑠 ∈ SAlg ↦ {𝑓 ∈ (ℝ ↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)})
3		unieq 4918	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑆 → ∪ 𝑠 = ∪ 𝑆)
4	3	oveq2d 7421	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑆 → (ℝ ↑pm ∪ 𝑠) = (ℝ ↑pm ∪ 𝑆))
5	4	rabeqdv 3447	. . . . . . . . . 10 ⊢ (𝑠 = 𝑆 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)} = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)})
6		oveq1 7412	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑆 → (𝑠 ↾t dom 𝑓) = (𝑆 ↾t dom 𝑓))
7	6	eleq2d 2819	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑆 → ((◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓) ↔ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)))
8	7	ralbidv 3177	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑆 → (∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓) ↔ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)))
9	8	rabbidv 3440	. . . . . . . . . 10 ⊢ (𝑠 = 𝑆 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)} = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
10	5, 9	eqtrd 2772	. . . . . . . . 9 ⊢ (𝑠 = 𝑆 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)} = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
11		issmflem.s	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ SAlg)
12		ovex 7438	. . . . . . . . . . 11 ⊢ (ℝ ↑pm ∪ 𝑆) ∈ V
13	12	rabex 5331	. . . . . . . . . 10 ⊢ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} ∈ V
14	13	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} ∈ V)
15	2, 10, 11, 14	fvmptd3 7018	. . . . . . . 8 ⊢ (𝜑 → (SMblFn‘𝑆) = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
16	15	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (SMblFn‘𝑆) = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
17	1, 16	eleqtrd 2835	. . . . . 6 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
18		elrabi 3676	. . . . . 6 ⊢ (𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆))
19	17, 18	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆))
20		issmflem.d	. . . . . . 7 ⊢ 𝐷 = dom 𝐹
21		elpmi2 43909	. . . . . . 7 ⊢ (𝐹 ∈ (ℝ ↑pm ∪ 𝑆) → dom 𝐹 ⊆ ∪ 𝑆)
22	20, 21	eqsstrid 4029	. . . . . 6 ⊢ (𝐹 ∈ (ℝ ↑pm ∪ 𝑆) → 𝐷 ⊆ ∪ 𝑆)
23	22	adantl 482	. . . . 5 ⊢ ((𝜑 ∧ 𝐹 ∈ (ℝ ↑pm ∪ 𝑆)) → 𝐷 ⊆ ∪ 𝑆)
24	19, 23	syldan 591	. . . 4 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐷 ⊆ ∪ 𝑆)
25		elpmi 8836	. . . . . . 7 ⊢ (𝐹 ∈ (ℝ ↑pm ∪ 𝑆) → (𝐹:dom 𝐹⟶ℝ ∧ dom 𝐹 ⊆ ∪ 𝑆))
26	19, 25	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (𝐹:dom 𝐹⟶ℝ ∧ dom 𝐹 ⊆ ∪ 𝑆))
27	26	simpld 495	. . . . 5 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹:dom 𝐹⟶ℝ)
28	20	feq2i 6706	. . . . . 6 ⊢ (𝐹:𝐷⟶ℝ ↔ 𝐹:dom 𝐹⟶ℝ)
29	28	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (𝐹:𝐷⟶ℝ ↔ 𝐹:dom 𝐹⟶ℝ))
30	27, 29	mpbird 256	. . . 4 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹:𝐷⟶ℝ)
31		cnveq 5871	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → ◡𝑓 = ◡𝐹)
32	31	imaeq1d 6056	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → (◡𝑓 “ (-∞(,)𝑎)) = (◡𝐹 “ (-∞(,)𝑎)))
33		dmeq 5901	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
34	33	oveq2d 7421	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → (𝑆 ↾t dom 𝑓) = (𝑆 ↾t dom 𝐹))
35	32, 34	eleq12d 2827	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → ((◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓) ↔ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
36	35	ralbidv 3177	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓) ↔ ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
37	36	elrab 3682	. . . . . . . . . 10 ⊢ (𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} ↔ (𝐹 ∈ (ℝ ↑pm ∪ 𝑆) ∧ ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
38	37	simprbi 497	. . . . . . . . 9 ⊢ (𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
39	17, 38	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
40	39	adantr 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
41		simpr 485	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ)
42		rspa 3245	. . . . . . 7 ⊢ ((∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹) ∧ 𝑎 ∈ ℝ) → (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
43	40, 41, 42	syl2anc 584	. . . . . 6 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
44	30	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → 𝐹:𝐷⟶ℝ)
45		simpl 483	. . . . . . . . . 10 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → 𝐹:𝐷⟶ℝ)
46		simpr 485	. . . . . . . . . . 11 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ)
47	46	rexrd 11260	. . . . . . . . . 10 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ*)
48	45, 47	preimaioomnf 45421	. . . . . . . . 9 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → (◡𝐹 “ (-∞(,)𝑎)) = {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎})
49	48	eqcomd 2738	. . . . . . . 8 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} = (◡𝐹 “ (-∞(,)𝑎)))
50	44, 41, 49	syl2anc 584	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} = (◡𝐹 “ (-∞(,)𝑎)))
51	20	oveq2i 7416	. . . . . . . 8 ⊢ (𝑆 ↾t 𝐷) = (𝑆 ↾t dom 𝐹)
52	51	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → (𝑆 ↾t 𝐷) = (𝑆 ↾t dom 𝐹))
53	50, 52	eleq12d 2827	. . . . . 6 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → ({𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
54	43, 53	mpbird 256	. . . . 5 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))
55	54	ralrimiva 3146	. . . 4 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))
56	24, 30, 55	3jca 1128	. . 3 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷)))
57	56	ex 413	. 2 ⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) → (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))))
58		reex 11197	. . . . . . . . 9 ⊢ ℝ ∈ V
59	58	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → ℝ ∈ V)
60	11	uniexd 7728	. . . . . . . . 9 ⊢ (𝜑 → ∪ 𝑆 ∈ V)
61	60	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → ∪ 𝑆 ∈ V)
62		simprr 771	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → 𝐹:𝐷⟶ℝ)
63		fssxp 6742	. . . . . . . . . . . 12 ⊢ (𝐹:𝐷⟶ℝ → 𝐹 ⊆ (𝐷 × ℝ))
64	63	adantl 482	. . . . . . . . . . 11 ⊢ ((𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ) → 𝐹 ⊆ (𝐷 × ℝ))
65		xpss1 5694	. . . . . . . . . . . 12 ⊢ (𝐷 ⊆ ∪ 𝑆 → (𝐷 × ℝ) ⊆ (∪ 𝑆 × ℝ))
66	65	adantr 481	. . . . . . . . . . 11 ⊢ ((𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ) → (𝐷 × ℝ) ⊆ (∪ 𝑆 × ℝ))
67	64, 66	sstrd 3991	. . . . . . . . . 10 ⊢ ((𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ) → 𝐹 ⊆ (∪ 𝑆 × ℝ))
68	67	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → 𝐹 ⊆ (∪ 𝑆 × ℝ))
69		dmss 5900	. . . . . . . . . . . 12 ⊢ (𝐹 ⊆ (∪ 𝑆 × ℝ) → dom 𝐹 ⊆ dom (∪ 𝑆 × ℝ))
70		dmxpss 6167	. . . . . . . . . . . . 13 ⊢ dom (∪ 𝑆 × ℝ) ⊆ ∪ 𝑆
71	70	a1i 11	. . . . . . . . . . . 12 ⊢ (𝐹 ⊆ (∪ 𝑆 × ℝ) → dom (∪ 𝑆 × ℝ) ⊆ ∪ 𝑆)
72	69, 71	sstrd 3991	. . . . . . . . . . 11 ⊢ (𝐹 ⊆ (∪ 𝑆 × ℝ) → dom 𝐹 ⊆ ∪ 𝑆)
73	72	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐹 ⊆ (∪ 𝑆 × ℝ)) → dom 𝐹 ⊆ ∪ 𝑆)
74	20, 73	eqsstrid 4029	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐹 ⊆ (∪ 𝑆 × ℝ)) → 𝐷 ⊆ ∪ 𝑆)
75	68, 74	syldan 591	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → 𝐷 ⊆ ∪ 𝑆)
76		elpm2r 8835	. . . . . . . 8 ⊢ (((ℝ ∈ V ∧ ∪ 𝑆 ∈ V) ∧ (𝐹:𝐷⟶ℝ ∧ 𝐷 ⊆ ∪ 𝑆)) → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆))
77	59, 61, 62, 75, 76	syl22anc 837	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆))
78	77	3adantr3 1171	. . . . . 6 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆))
79	20	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → 𝐷 = dom 𝐹)
80	79	oveq2d 7421	. . . . . . . . . . . 12 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → (𝑆 ↾t 𝐷) = (𝑆 ↾t dom 𝐹))
81	49, 80	eleq12d 2827	. . . . . . . . . . 11 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → ({𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
82	81	ralbidva 3175	. . . . . . . . . 10 ⊢ (𝐹:𝐷⟶ℝ → (∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷) ↔ ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
83	82	biimpd 228	. . . . . . . . 9 ⊢ (𝐹:𝐷⟶ℝ → (∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
84	83	imp 407	. . . . . . . 8 ⊢ ((𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷)) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
85	84	adantl 482	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
86	85	3adantr1 1169	. . . . . 6 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
87	78, 86	jca 512	. . . . 5 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → (𝐹 ∈ (ℝ ↑pm ∪ 𝑆) ∧ ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
88	87, 37	sylibr 233	. . . 4 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → 𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
89	15	eqcomd 2738	. . . . 5 ⊢ (𝜑 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} = (SMblFn‘𝑆))
90	89	adantr 481	. . . 4 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} = (SMblFn‘𝑆))
91	88, 90	eleqtrd 2835	. . 3 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → 𝐹 ∈ (SMblFn‘𝑆))
92	91	ex 413	. 2 ⊢ (𝜑 → ((𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷)) → 𝐹 ∈ (SMblFn‘𝑆)))
93	57, 92	impbid 211	1 ⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) ↔ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  ∀wral 3061  {crab 3432  Vcvv 3474   ⊆ wss 3947  ∪ cuni 4907   class class class wbr 5147   × cxp 5673  ^◡ccnv 5674  dom cdm 5675   “ cima 5678  ⟶wf 6536  ‘cfv 6540  (class class class)co 7405   ↑_pm cpm 8817  ℝcr 11105  -∞cmnf 11242   < clt 11244  (,)cioo 13320   ↾_t crest 17362  SAlgcsalg 45010  SMblFncsmblfn 45397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-pre-lttri 11180  ax-pre-lttrn 11181

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410  df-1st 7971  df-2nd 7972  df-er 8699  df-pm 8819  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-ioo 13324  df-ico 13326  df-smblfn 45398

This theorem is referenced by:  issmf  45430