Theorem issmflem 46683

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 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹 ∈ (SMblFn‘𝑆))
2		df-smblfn 46652	. . . . . . . . 9 ⊢ SMblFn = (𝑠 ∈ SAlg ↦ {𝑓 ∈ (ℝ ↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)})
3		unieq 4923	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑆 → ∪ 𝑠 = ∪ 𝑆)
4	3	oveq2d 7447	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑆 → (ℝ ↑pm ∪ 𝑠) = (ℝ ↑pm ∪ 𝑆))
5	4	rabeqdv 3449	. . . . . . . . . 10 ⊢ (𝑠 = 𝑆 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)} = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)})
6		oveq1 7438	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑆 → (𝑠 ↾t dom 𝑓) = (𝑆 ↾t dom 𝑓))
7	6	eleq2d 2825	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑆 → ((◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓) ↔ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)))
8	7	ralbidv 3176	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑆 → (∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓) ↔ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)))
9	8	rabbidv 3441	. . . . . . . . . 10 ⊢ (𝑠 = 𝑆 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)} = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
10	5, 9	eqtrd 2775	. . . . . . . . 9 ⊢ (𝑠 = 𝑆 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)} = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
11		issmflem.s	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ SAlg)
12		ovex 7464	. . . . . . . . . . 11 ⊢ (ℝ ↑pm ∪ 𝑆) ∈ V
13	12	rabex 5345	. . . . . . . . . 10 ⊢ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} ∈ V
14	13	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} ∈ V)
15	2, 10, 11, 14	fvmptd3 7039	. . . . . . . 8 ⊢ (𝜑 → (SMblFn‘𝑆) = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
16	15	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (SMblFn‘𝑆) = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
17	1, 16	eleqtrd 2841	. . . . . 6 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
18		elrabi 3690	. . . . . 6 ⊢ (𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆))
19	17, 18	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆))
20		issmflem.d	. . . . . . 7 ⊢ 𝐷 = dom 𝐹
21		elpmi2 45168	. . . . . . 7 ⊢ (𝐹 ∈ (ℝ ↑pm ∪ 𝑆) → dom 𝐹 ⊆ ∪ 𝑆)
22	20, 21	eqsstrid 4044	. . . . . 6 ⊢ (𝐹 ∈ (ℝ ↑pm ∪ 𝑆) → 𝐷 ⊆ ∪ 𝑆)
23	22	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝐹 ∈ (ℝ ↑pm ∪ 𝑆)) → 𝐷 ⊆ ∪ 𝑆)
24	19, 23	syldan 591	. . . 4 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐷 ⊆ ∪ 𝑆)
25		elpmi 8885	. . . . . . 7 ⊢ (𝐹 ∈ (ℝ ↑pm ∪ 𝑆) → (𝐹:dom 𝐹⟶ℝ ∧ dom 𝐹 ⊆ ∪ 𝑆))
26	19, 25	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (𝐹:dom 𝐹⟶ℝ ∧ dom 𝐹 ⊆ ∪ 𝑆))
27	26	simpld 494	. . . . 5 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹:dom 𝐹⟶ℝ)
28	20	feq2i 6729	. . . . . 6 ⊢ (𝐹:𝐷⟶ℝ ↔ 𝐹:dom 𝐹⟶ℝ)
29	28	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (𝐹:𝐷⟶ℝ ↔ 𝐹:dom 𝐹⟶ℝ))
30	27, 29	mpbird 257	. . . 4 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹:𝐷⟶ℝ)
31		cnveq 5887	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → ◡𝑓 = ◡𝐹)
32	31	imaeq1d 6079	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → (◡𝑓 “ (-∞(,)𝑎)) = (◡𝐹 “ (-∞(,)𝑎)))
33		dmeq 5917	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
34	33	oveq2d 7447	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → (𝑆 ↾t dom 𝑓) = (𝑆 ↾t dom 𝐹))
35	32, 34	eleq12d 2833	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → ((◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓) ↔ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
36	35	ralbidv 3176	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓) ↔ ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
37	36	elrab 3695	. . . . . . . . . 10 ⊢ (𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} ↔ (𝐹 ∈ (ℝ ↑pm ∪ 𝑆) ∧ ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
38	37	simprbi 496	. . . . . . . . 9 ⊢ (𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
39	17, 38	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
40	39	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
41		simpr 484	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ)
42		rspa 3246	. . . . . . 7 ⊢ ((∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹) ∧ 𝑎 ∈ ℝ) → (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
43	40, 41, 42	syl2anc 584	. . . . . 6 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
44	30	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → 𝐹:𝐷⟶ℝ)
45		simpl 482	. . . . . . . . . 10 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → 𝐹:𝐷⟶ℝ)
46		simpr 484	. . . . . . . . . . 11 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ)
47	46	rexrd 11309	. . . . . . . . . 10 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ*)
48	45, 47	preimaioomnf 46675	. . . . . . . . 9 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → (◡𝐹 “ (-∞(,)𝑎)) = {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎})
49	48	eqcomd 2741	. . . . . . . 8 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} = (◡𝐹 “ (-∞(,)𝑎)))
50	44, 41, 49	syl2anc 584	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} = (◡𝐹 “ (-∞(,)𝑎)))
51	20	oveq2i 7442	. . . . . . . 8 ⊢ (𝑆 ↾t 𝐷) = (𝑆 ↾t dom 𝐹)
52	51	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → (𝑆 ↾t 𝐷) = (𝑆 ↾t dom 𝐹))
53	50, 52	eleq12d 2833	. . . . . 6 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → ({𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
54	43, 53	mpbird 257	. . . . 5 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))
55	54	ralrimiva 3144	. . . 4 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))
56	24, 30, 55	3jca 1127	. . 3 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷)))
57	56	ex 412	. 2 ⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) → (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))))
58		reex 11244	. . . . . . . . 9 ⊢ ℝ ∈ V
59	58	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → ℝ ∈ V)
60	11	uniexd 7761	. . . . . . . . 9 ⊢ (𝜑 → ∪ 𝑆 ∈ V)
61	60	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → ∪ 𝑆 ∈ V)
62		simprr 773	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → 𝐹:𝐷⟶ℝ)
63		fssxp 6764	. . . . . . . . . . . 12 ⊢ (𝐹:𝐷⟶ℝ → 𝐹 ⊆ (𝐷 × ℝ))
64	63	adantl 481	. . . . . . . . . . 11 ⊢ ((𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ) → 𝐹 ⊆ (𝐷 × ℝ))
65		xpss1 5708	. . . . . . . . . . . 12 ⊢ (𝐷 ⊆ ∪ 𝑆 → (𝐷 × ℝ) ⊆ (∪ 𝑆 × ℝ))
66	65	adantr 480	. . . . . . . . . . 11 ⊢ ((𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ) → (𝐷 × ℝ) ⊆ (∪ 𝑆 × ℝ))
67	64, 66	sstrd 4006	. . . . . . . . . 10 ⊢ ((𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ) → 𝐹 ⊆ (∪ 𝑆 × ℝ))
68	67	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → 𝐹 ⊆ (∪ 𝑆 × ℝ))
69		dmss 5916	. . . . . . . . . . . 12 ⊢ (𝐹 ⊆ (∪ 𝑆 × ℝ) → dom 𝐹 ⊆ dom (∪ 𝑆 × ℝ))
70		dmxpss 6193	. . . . . . . . . . . . 13 ⊢ dom (∪ 𝑆 × ℝ) ⊆ ∪ 𝑆
71	70	a1i 11	. . . . . . . . . . . 12 ⊢ (𝐹 ⊆ (∪ 𝑆 × ℝ) → dom (∪ 𝑆 × ℝ) ⊆ ∪ 𝑆)
72	69, 71	sstrd 4006	. . . . . . . . . . 11 ⊢ (𝐹 ⊆ (∪ 𝑆 × ℝ) → dom 𝐹 ⊆ ∪ 𝑆)
73	72	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐹 ⊆ (∪ 𝑆 × ℝ)) → dom 𝐹 ⊆ ∪ 𝑆)
74	20, 73	eqsstrid 4044	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐹 ⊆ (∪ 𝑆 × ℝ)) → 𝐷 ⊆ ∪ 𝑆)
75	68, 74	syldan 591	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → 𝐷 ⊆ ∪ 𝑆)
76		elpm2r 8884	. . . . . . . 8 ⊢ (((ℝ ∈ V ∧ ∪ 𝑆 ∈ V) ∧ (𝐹:𝐷⟶ℝ ∧ 𝐷 ⊆ ∪ 𝑆)) → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆))
77	59, 61, 62, 75, 76	syl22anc 839	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆))
78	77	3adantr3 1170	. . . . . 6 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆))
79	20	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → 𝐷 = dom 𝐹)
80	79	oveq2d 7447	. . . . . . . . . . . 12 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → (𝑆 ↾t 𝐷) = (𝑆 ↾t dom 𝐹))
81	49, 80	eleq12d 2833	. . . . . . . . . . 11 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → ({𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
82	81	ralbidva 3174	. . . . . . . . . 10 ⊢ (𝐹:𝐷⟶ℝ → (∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷) ↔ ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
83	82	biimpd 229	. . . . . . . . 9 ⊢ (𝐹:𝐷⟶ℝ → (∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
84	83	imp 406	. . . . . . . 8 ⊢ ((𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷)) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
85	84	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
86	85	3adantr1 1168	. . . . . 6 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
87	78, 86	jca 511	. . . . 5 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → (𝐹 ∈ (ℝ ↑pm ∪ 𝑆) ∧ ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
88	87, 37	sylibr 234	. . . 4 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → 𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
89	15	eqcomd 2741	. . . . 5 ⊢ (𝜑 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} = (SMblFn‘𝑆))
90	89	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} = (SMblFn‘𝑆))
91	88, 90	eleqtrd 2841	. . 3 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → 𝐹 ∈ (SMblFn‘𝑆))
92	91	ex 412	. 2 ⊢ (𝜑 → ((𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷)) → 𝐹 ∈ (SMblFn‘𝑆)))
93	57, 92	impbid 212	1 ⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) ↔ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1537   ∈ wcel 2106  ∀wral 3059  {crab 3433  Vcvv 3478   ⊆ wss 3963  ∪ cuni 4912   class class class wbr 5148   × cxp 5687  ^◡ccnv 5688  dom cdm 5689   “ cima 5692  ⟶wf 6559  ‘cfv 6563  (class class class)co 7431   ↑_pm cpm 8866  ℝcr 11152  -∞cmnf 11291   < clt 11293  (,)cioo 13384   ↾_t crest 17467  SAlgcsalg 46264  SMblFncsmblfn 46651

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-cnex 11209  ax-resscn 11210  ax-pre-lttri 11227  ax-pre-lttrn 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-po 5597  df-so 5598  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8013  df-2nd 8014  df-er 8744  df-pm 8868  df-en 8985  df-dom 8986  df-sdom 8987  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-ioo 13388  df-ico 13390  df-smblfn 46652

This theorem is referenced by:  issmf  46684