Theorem issmflem 47501

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 490	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹 ∈ (SMblFn‘𝑆))
2		df-smblfn 47470	. . . . . . . . 9 ⊢ SMblFn = (𝑠 ∈ SAlg ↦ {𝑓 ∈ (ℝ ↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)})
3		unieq 4885	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑆 → ∪ 𝑠 = ∪ 𝑆)
4	3	oveq2d 7435	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑆 → (ℝ ↑pm ∪ 𝑠) = (ℝ ↑pm ∪ 𝑆))
5	4	rabeqdv 3433	. . . . . . . . . 10 ⊢ (𝑠 = 𝑆 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)} = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)})
6		oveq1 7426	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑆 → (𝑠 ↾t dom 𝑓) = (𝑆 ↾t dom 𝑓))
7	6	eleq2d 2851	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑆 → ((◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓) ↔ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)))
8	7	ralbidv 3190	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑆 → (∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓) ↔ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)))
9	8	rabbidv 3425	. . . . . . . . . 10 ⊢ (𝑠 = 𝑆 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)} = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
10	5, 9	eqtrd 2800	. . . . . . . . 9 ⊢ (𝑠 = 𝑆 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)} = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
11		issmflem.s	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ SAlg)
12		ovex 7452	. . . . . . . . . . 11 ⊢ (ℝ ↑pm ∪ 𝑆) ∈ V
13	12	rabex 5311	. . . . . . . . . 10 ⊢ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} ∈ V
14	13	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} ∈ V)
15	2, 10, 11, 14	fvmptd3 7017	. . . . . . . 8 ⊢ (𝜑 → (SMblFn‘𝑆) = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
16	15	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (SMblFn‘𝑆) = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
17	1, 16	eleqtrd 2867	. . . . . 6 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
18		elrabi 3648	. . . . . 6 ⊢ (𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆))
19	17, 18	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆))
20		issmflem.d	. . . . . . 7 ⊢ 𝐷 = dom 𝐹
21		elpmi2 46001	. . . . . . 7 ⊢ (𝐹 ∈ (ℝ ↑pm ∪ 𝑆) → dom 𝐹 ⊆ ∪ 𝑆)
22	20, 21	eqsstrid 3976	. . . . . 6 ⊢ (𝐹 ∈ (ℝ ↑pm ∪ 𝑆) → 𝐷 ⊆ ∪ 𝑆)
23	22	adantl 487	. . . . 5 ⊢ ((𝜑 ∧ 𝐹 ∈ (ℝ ↑pm ∪ 𝑆)) → 𝐷 ⊆ ∪ 𝑆)
24	19, 23	syldan 603	. . . 4 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐷 ⊆ ∪ 𝑆)
25		elpmi 8849	. . . . . . 7 ⊢ (𝐹 ∈ (ℝ ↑pm ∪ 𝑆) → (𝐹:dom 𝐹⟶ℝ ∧ dom 𝐹 ⊆ ∪ 𝑆))
26	19, 25	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (𝐹:dom 𝐹⟶ℝ ∧ dom 𝐹 ⊆ ∪ 𝑆))
27	26	simpld 500	. . . . 5 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹:dom 𝐹⟶ℝ)
28	20	feq2i 6701	. . . . . 6 ⊢ (𝐹:𝐷⟶ℝ ↔ 𝐹:dom 𝐹⟶ℝ)
29	28	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (𝐹:𝐷⟶ℝ ↔ 𝐹:dom 𝐹⟶ℝ))
30	27, 29	mpbird 260	. . . 4 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹:𝐷⟶ℝ)
31		cnveq 5861	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → ◡𝑓 = ◡𝐹)
32	31	imaeq1d 6063	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → (◡𝑓 “ (-∞(,)𝑎)) = (◡𝐹 “ (-∞(,)𝑎)))
33		dmeq 5895	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
34	33	oveq2d 7435	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → (𝑆 ↾t dom 𝑓) = (𝑆 ↾t dom 𝐹))
35	32, 34	eleq12d 2859	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → ((◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓) ↔ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
36	35	ralbidv 3190	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓) ↔ ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
37	36	elrab 3652	. . . . . . . . . 10 ⊢ (𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} ↔ (𝐹 ∈ (ℝ ↑pm ∪ 𝑆) ∧ ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
38	37	simprbi 503	. . . . . . . . 9 ⊢ (𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
39	17, 38	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
40	39	adantr 486	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
41		simpr 490	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ)
42		rspa 3256	. . . . . . 7 ⊢ ((∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹) ∧ 𝑎 ∈ ℝ) → (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
43	40, 41, 42	syl2anc 596	. . . . . 6 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
44	30	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → 𝐹:𝐷⟶ℝ)
45		simpl 488	. . . . . . . . . 10 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → 𝐹:𝐷⟶ℝ)
46		simpr 490	. . . . . . . . . . 11 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ)
47	46	rexrd 11276	. . . . . . . . . 10 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ*)
48	45, 47	preimaioomnf 47493	. . . . . . . . 9 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → (◡𝐹 “ (-∞(,)𝑎)) = {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎})
49	48	eqcomd 2771	. . . . . . . 8 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} = (◡𝐹 “ (-∞(,)𝑎)))
50	44, 41, 49	syl2anc 596	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} = (◡𝐹 “ (-∞(,)𝑎)))
51	20	oveq2i 7430	. . . . . . . 8 ⊢ (𝑆 ↾t 𝐷) = (𝑆 ↾t dom 𝐹)
52	51	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → (𝑆 ↾t 𝐷) = (𝑆 ↾t dom 𝐹))
53	50, 52	eleq12d 2859	. . . . . 6 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → ({𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
54	43, 53	mpbird 260	. . . . 5 ⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))
55	54	ralrimiva 3159	. . . 4 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))
56	24, 30, 55	3jca 1146	. . 3 ⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷)))
57	56	ex 418	. 2 ⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) → (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))))
58		reex 11208	. . . . . . . . 9 ⊢ ℝ ∈ V
59	58	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → ℝ ∈ V)
60	11	uniexd 7750	. . . . . . . . 9 ⊢ (𝜑 → ∪ 𝑆 ∈ V)
61	60	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → ∪ 𝑆 ∈ V)
62		simprr 785	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → 𝐹:𝐷⟶ℝ)
63		fssxp 6737	. . . . . . . . . . . 12 ⊢ (𝐹:𝐷⟶ℝ → 𝐹 ⊆ (𝐷 × ℝ))
64	63	adantl 487	. . . . . . . . . . 11 ⊢ ((𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ) → 𝐹 ⊆ (𝐷 × ℝ))
65		xpss1 5682	. . . . . . . . . . . 12 ⊢ (𝐷 ⊆ ∪ 𝑆 → (𝐷 × ℝ) ⊆ (∪ 𝑆 × ℝ))
66	65	adantr 486	. . . . . . . . . . 11 ⊢ ((𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ) → (𝐷 × ℝ) ⊆ (∪ 𝑆 × ℝ))
67	64, 66	sstrd 3948	. . . . . . . . . 10 ⊢ ((𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ) → 𝐹 ⊆ (∪ 𝑆 × ℝ))
68	67	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → 𝐹 ⊆ (∪ 𝑆 × ℝ))
69		dmss 5894	. . . . . . . . . . . 12 ⊢ (𝐹 ⊆ (∪ 𝑆 × ℝ) → dom 𝐹 ⊆ dom (∪ 𝑆 × ℝ))
70		dmxpss 6171	. . . . . . . . . . . . 13 ⊢ dom (∪ 𝑆 × ℝ) ⊆ ∪ 𝑆
71	70	a1i 11	. . . . . . . . . . . 12 ⊢ (𝐹 ⊆ (∪ 𝑆 × ℝ) → dom (∪ 𝑆 × ℝ) ⊆ ∪ 𝑆)
72	69, 71	sstrd 3948	. . . . . . . . . . 11 ⊢ (𝐹 ⊆ (∪ 𝑆 × ℝ) → dom 𝐹 ⊆ ∪ 𝑆)
73	72	adantl 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐹 ⊆ (∪ 𝑆 × ℝ)) → dom 𝐹 ⊆ ∪ 𝑆)
74	20, 73	eqsstrid 3976	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐹 ⊆ (∪ 𝑆 × ℝ)) → 𝐷 ⊆ ∪ 𝑆)
75	68, 74	syldan 603	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → 𝐷 ⊆ ∪ 𝑆)
76		elpm2r 8848	. . . . . . . 8 ⊢ (((ℝ ∈ V ∧ ∪ 𝑆 ∈ V) ∧ (𝐹:𝐷⟶ℝ ∧ 𝐷 ⊆ ∪ 𝑆)) → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆))
77	59, 61, 62, 75, 76	syl22anc 852	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆))
78	77	3adantr3 1190	. . . . . 6 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆))
79	20	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → 𝐷 = dom 𝐹)
80	79	oveq2d 7435	. . . . . . . . . . . 12 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → (𝑆 ↾t 𝐷) = (𝑆 ↾t dom 𝐹))
81	49, 80	eleq12d 2859	. . . . . . . . . . 11 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → ({𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
82	81	ralbidva 3188	. . . . . . . . . 10 ⊢ (𝐹:𝐷⟶ℝ → (∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷) ↔ ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
83	82	biimpd 232	. . . . . . . . 9 ⊢ (𝐹:𝐷⟶ℝ → (∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
84	83	imp 412	. . . . . . . 8 ⊢ ((𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷)) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
85	84	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
86	85	3adantr1 1188	. . . . . 6 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))
87	78, 86	jca 521	. . . . 5 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → (𝐹 ∈ (ℝ ↑pm ∪ 𝑆) ∧ ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)))
88	87, 37	sylibr 237	. . . 4 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → 𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)})
89	15	eqcomd 2771	. . . . 5 ⊢ (𝜑 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} = (SMblFn‘𝑆))
90	89	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → {𝑓 ∈ (ℝ ↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} = (SMblFn‘𝑆))
91	88, 90	eleqtrd 2867	. . 3 ⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → 𝐹 ∈ (SMblFn‘𝑆))
92	91	ex 418	. 2 ⊢ (𝜑 → ((𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷)) → 𝐹 ∈ (SMblFn‘𝑆)))
93	57, 92	impbid 215	1 ⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) ↔ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146  ∀wral 3081  {crab 3418  Vcvv 3457   ⊆ wss 3906  ∪ cuni 4874   class class class wbr 5111   × cxp 5661  ^◡ccnv 5662  dom cdm 5663   “ cima 5666  ⟶wf 6536  ‘cfv 6540  (class class class)co 7419   ↑_pm cpm 8831  ℝcr 11116  -∞cmnf 11258   < clt 11260  (,)cioo 13390   ↾_t crest 17497  SAlgcsalg 47082  SMblFncsmblfn 47469

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-cnex 11173  ax-resscn 11174  ax-pre-lttri 11191  ax-pre-lttrn 11192

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-po 5571  df-so 5572  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7422  df-oprab 7423  df-mpo 7424  df-1st 7992  df-2nd 7993  df-er 8700  df-pm 8833  df-en 8950  df-dom 8951  df-sdom 8952  df-pnf 11262  df-mnf 11263  df-xr 11264  df-ltxr 11265  df-le 11266  df-ioo 13394  df-ico 13396  df-smblfn 47470

This theorem is used by:  issmf  47502