Theorem issmflem 39613

Description: The predicate "𝐹 is a 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 476	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹 ∈ (SMblFn‘𝑆))
2		df-smblfn 39587	. . . . . . . . . 10 ⊢ SMblFn = (𝑠 ∈ SAlg ↦ {𝑓 ∈ (ℝ ↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)})
3	2	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → SMblFn = (𝑠 ∈ SAlg ↦ {𝑓 ∈ (ℝ ↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)}))
4		unieq 4380	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑆 → ∪ 𝑠 = ∪ 𝑆)
5	4	oveq2d 6565	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑆 → (ℝ ↑pm ∪ 𝑠) = (ℝ ↑pm ∪ 𝑆))
6	5	rabeqd 38304	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑆 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)} = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)})
7		oveq1 6556	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑆 → (𝑠 ↾t dom 𝑓) = (𝑆 ↾t dom 𝑓))
8	7	eleq2d 2673	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑆 → ((◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓) ↔ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)))
9	8	ralbidv 2969	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑆 → (∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓) ↔ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)))
10	9	rabbidv 3164	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑆 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)} = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
11	6, 10	eqtrd 2644	. . . . . . . . . 10 ⊢ (𝑠 = 𝑆 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)} = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
12	11	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 = 𝑆) → {𝑓 ∈ (ℝ ↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)} = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
13		issmflem.s	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ SAlg)
14		ovex 6577	. . . . . . . . . . 11 ⊢ (ℝ ↑pm ∪ 𝑆) ∈ V
15	14	rabex 4740	. . . . . . . . . 10 ⊢ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} ∈ V
16	15	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} ∈ V)
17	3, 12, 13, 16	fvmptd 6197	. . . . . . . 8 ⊢ (𝜑 → (SMblFn‘𝑆) = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
18	17	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (SMblFn‘𝑆) = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
19	1, 18	eleqtrd 2690	. . . . . 6 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
20		elrabi 3328	. . . . . 6 ⊢ (𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆))
21	19, 20	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆))
22		issmflem.d	. . . . . . 7 ⊢ 𝐷 = dom 𝐹
23		elpmi2 38413	. . . . . . 7 ⊢ (𝐹 ∈ (ℝ ↑pm ∪ 𝑆) → dom 𝐹 ⊆ ∪ 𝑆)
24	22, 23	syl5eqss 3612	. . . . . 6 ⊢ (𝐹 ∈ (ℝ ↑pm ∪ 𝑆) → 𝐷 ⊆ ∪ 𝑆)
25	24	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝐹 ∈ (ℝ ↑pm ∪ 𝑆)) → 𝐷 ⊆ ∪ 𝑆)
26	21, 25	syldan 486	. . . 4 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐷 ⊆ ∪ 𝑆)
27		elpmi 7762	. . . . . . 7 ⊢ (𝐹 ∈ (ℝ ↑pm ∪ 𝑆) → (𝐹:dom 𝐹⟶ℝ ∧ dom 𝐹 ⊆ ∪ 𝑆))
28	21, 27	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (𝐹:dom 𝐹⟶ℝ ∧ dom 𝐹 ⊆ ∪ 𝑆))
29	28	simpld 474	. . . . 5 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹:dom 𝐹⟶ℝ)
30	22	feq2i 5950	. . . . . 6 ⊢ (𝐹:𝐷⟶ℝ ↔ 𝐹:dom 𝐹⟶ℝ)
31	30	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (𝐹:𝐷⟶ℝ ↔ 𝐹:dom 𝐹⟶ℝ))
32	29, 31	mpbird 246	. . . 4 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹:𝐷⟶ℝ)
33		cnveq 5218	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → ◡𝑓 = ◡𝐹)
34	33	imaeq1d 5384	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → (◡𝑓 “ (-∞(,)𝑎)) = (◡𝐹 “ (-∞(,)𝑎)))
35		dmeq 5246	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
36	35	oveq2d 6565	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → (𝑆 ↾t dom 𝑓) = (𝑆 ↾t dom 𝐹))
37	34, 36	eleq12d 2682	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → ((◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓) ↔ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
38	37	ralbidv 2969	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓) ↔ ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
39	38	elrab 3331	. . . . . . . . . 10 ⊢ (𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} ↔ (𝐹 ∈ (ℝ ↑pm ∪ 𝑆) ∧ ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
40	39	simprbi 479	. . . . . . . . 9 ⊢ (𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
41	19, 40	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
42	41	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
43		simpr 476	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ)
44		rspa 2914	. . . . . . 7 ⊢ ((∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹) ∧ 𝑎 ∈ ℝ) → (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
45	42, 43, 44	syl2anc 691	. . . . . 6 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
46	32	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → 𝐹:𝐷⟶ℝ)
47		simpl 472	. . . . . . . . . 10 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → 𝐹:𝐷⟶ℝ)
48		simpr 476	. . . . . . . . . . 11 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ)
49	48	rexrd 9968	. . . . . . . . . 10 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ*)
50	47, 49	preimaioomnf 39606	. . . . . . . . 9 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → (◡𝐹 “ (-∞(,)𝑎)) = {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎})
51	50	eqcomd 2616	. . . . . . . 8 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} = (◡𝐹 “ (-∞(,)𝑎)))
52	46, 43, 51	syl2anc 691	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} = (◡𝐹 “ (-∞(,)𝑎)))
53	22	oveq2i 6560	. . . . . . . 8 ⊢ (𝑆 ↾t 𝐷) = (𝑆 ↾t dom 𝐹)
54	53	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → (𝑆 ↾t 𝐷) = (𝑆 ↾t dom 𝐹))
55	52, 54	eleq12d 2682	. . . . . 6 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → ({𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
56	45, 55	mpbird 246	. . . . 5 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))
57	56	ralrimiva 2949	. . . 4 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))
58	26, 32, 57	3jca 1235	. . 3 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷)))
59	58	ex 449	. 2 ⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) → (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))))
60		reex 9906	. . . . . . . . 9 ⊢ ℝ ∈ V
61	60	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → ℝ ∈ V)
62	13	uniexd 38310	. . . . . . . . 9 ⊢ (𝜑 → ∪ 𝑆 ∈ V)
63	62	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → ∪ 𝑆 ∈ V)
64		simprr 792	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → 𝐹:𝐷⟶ℝ)
65		fssxp 5973	. . . . . . . . . . . 12 ⊢ (𝐹:𝐷⟶ℝ → 𝐹 ⊆ (𝐷 × ℝ))
66	65	adantl 481	. . . . . . . . . . 11 ⊢ ((𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ) → 𝐹 ⊆ (𝐷 × ℝ))
67		xpss1 5151	. . . . . . . . . . . 12 ⊢ (𝐷 ⊆ ∪ 𝑆 → (𝐷 × ℝ) ⊆ (∪ 𝑆 × ℝ))
68	67	adantr 480	. . . . . . . . . . 11 ⊢ ((𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ) → (𝐷 × ℝ) ⊆ (∪ 𝑆 × ℝ))
69	66, 68	sstrd 3578	. . . . . . . . . 10 ⊢ ((𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ) → 𝐹 ⊆ (∪ 𝑆 × ℝ))
70	69	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → 𝐹 ⊆ (∪ 𝑆 × ℝ))
71		dmss 5245	. . . . . . . . . . . 12 ⊢ (𝐹 ⊆ (∪ 𝑆 × ℝ) → dom 𝐹 ⊆ dom (∪ 𝑆 × ℝ))
72		dmxpss 5484	. . . . . . . . . . . . 13 ⊢ dom (∪ 𝑆 × ℝ) ⊆ ∪ 𝑆
73	72	a1i 11	. . . . . . . . . . . 12 ⊢ (𝐹 ⊆ (∪ 𝑆 × ℝ) → dom (∪ 𝑆 × ℝ) ⊆ ∪ 𝑆)
74	71, 73	sstrd 3578	. . . . . . . . . . 11 ⊢ (𝐹 ⊆ (∪ 𝑆 × ℝ) → dom 𝐹 ⊆ ∪ 𝑆)
75	74	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐹 ⊆ (∪ 𝑆 × ℝ)) → dom 𝐹 ⊆ ∪ 𝑆)
76	22, 75	syl5eqss 3612	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐹 ⊆ (∪ 𝑆 × ℝ)) → 𝐷 ⊆ ∪ 𝑆)
77	70, 76	syldan 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → 𝐷 ⊆ ∪ 𝑆)
78		elpm2r 7761	. . . . . . . 8 ⊢ (((ℝ ∈ V ∧ ∪ 𝑆 ∈ V) ∧ (𝐹:𝐷⟶ℝ ∧ 𝐷 ⊆ ∪ 𝑆)) → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆))
79	61, 63, 64, 77, 78	syl22anc 1319	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆))
80	79	3adantr3 1215	. . . . . 6 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆))
81	22	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → 𝐷 = dom 𝐹)
82	81	oveq2d 6565	. . . . . . . . . . . 12 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → (𝑆 ↾t 𝐷) = (𝑆 ↾t dom 𝐹))
83	51, 82	eleq12d 2682	. . . . . . . . . . 11 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → ({𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
84	83	ralbidva 2968	. . . . . . . . . 10 ⊢ (𝐹:𝐷⟶ℝ → (∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷) ↔ ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
85	84	biimpd 218	. . . . . . . . 9 ⊢ (𝐹:𝐷⟶ℝ → (∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
86	85	imp 444	. . . . . . . 8 ⊢ ((𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷)) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
87	86	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
88	87	3adantr1 1213	. . . . . 6 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
89	80, 88	jca 553	. . . . 5 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → (𝐹 ∈ (ℝ ↑pm ∪ 𝑆) ∧ ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
90	89, 39	sylibr 223	. . . 4 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → 𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
91	17	eqcomd 2616	. . . . 5 ⊢ (𝜑 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} = (SMblFn‘𝑆))
92	91	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} = (SMblFn‘𝑆))
93	90, 92	eleqtrd 2690	. . 3 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → 𝐹 ∈ (SMblFn‘𝑆))
94	93	ex 449	. 2 ⊢ (𝜑 → ((𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷)) → 𝐹 ∈ (SMblFn‘𝑆)))
95	59, 94	impbid 201	1 ⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) ↔ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  {crab 2900  Vcvv 3173   ⊆ wss 3540  ∪ cuni 4372   class class class wbr 4583   ↦ cmpt 4643   × cxp 5036  ^◡ccnv 5037  dom cdm 5038   “ cima 5041  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↑_pm cpm 7745  ℝcr 9814  -∞cmnf 9951   < clt 9953  (,)cioo 12046   ↾_t crest 15904  SAlgcsalg 39204  SMblFncsmblfn 39586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-pre-lttri 9889  ax-pre-lttrn 9890

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-po 4959  df-so 4960  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-1st 7059  df-2nd 7060  df-er 7629  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-ioo 12050  df-ico 12052  df-smblfn 39587

This theorem is referenced by:  issmf  39614