Theorem smfresal 47472

Description: Given a sigma-measurable function, the subsets of ℝ whose preimage is in the sigma-algebra induced by the function's domain, form a sigma-algebra. First part of the proof of Proposition 121E (f) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)

Hypotheses

Ref	Expression
smfresal.s	⊢ (𝜑 → 𝑆 ∈ SAlg)
smfresal.f	⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))
smfresal.d	⊢ 𝐷 = dom 𝐹
smfresal.t	⊢ 𝑇 = {𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)}

Assertion

Ref	Expression
smfresal	⊢ (𝜑 → 𝑇 ∈ SAlg)

Distinct variable groups:   𝐷,𝑒   𝑒,𝐹   𝑆,𝑒   𝜑,𝑒

Allowed substitution hint:   𝑇(𝑒)

Proof of Theorem smfresal

Dummy variables 𝑛 𝑥 𝑔 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		smfresal.t	. . . 4 ⊢ 𝑇 = {𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)}
2		reex 11190	. . . . 5 ⊢ ℝ ∈ V
3	2	pwex 5351	. . . 4 ⊢ 𝒫 ℝ ∈ V
4	1, 3	rabex2 5311	. . 3 ⊢ 𝑇 ∈ V
5	4	a1i 11	. 2 ⊢ (𝜑 → 𝑇 ∈ V)
6		0elpw 5326	. . . . 5 ⊢ ∅ ∈ 𝒫 ℝ
7	6	a1i 11	. . . 4 ⊢ (𝜑 → ∅ ∈ 𝒫 ℝ)
8		ima0 6079	. . . . . 6 ⊢ (◡𝐹 “ ∅) = ∅
9	8	a1i 11	. . . . 5 ⊢ (𝜑 → (◡𝐹 “ ∅) = ∅)
10		smfresal.s	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ SAlg)
11	10	uniexd 7740	. . . . . . . 8 ⊢ (𝜑 → ∪ 𝑆 ∈ V)
12		smfresal.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))
13		smfresal.d	. . . . . . . . 9 ⊢ 𝐷 = dom 𝐹
14	10, 12, 13	smfdmss 47417	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑆)
15	11, 14	ssexd 5294	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ V)
16		eqid 2761	. . . . . . 7 ⊢ (𝑆 ↾t 𝐷) = (𝑆 ↾t 𝐷)
17	10, 15, 16	subsalsal 47043	. . . . . 6 ⊢ (𝜑 → (𝑆 ↾t 𝐷) ∈ SAlg)
18	17	0sald 47034	. . . . 5 ⊢ (𝜑 → ∅ ∈ (𝑆 ↾t 𝐷))
19	9, 18	eqeltrd 2861	. . . 4 ⊢ (𝜑 → (◡𝐹 “ ∅) ∈ (𝑆 ↾t 𝐷))
20	7, 19	jca 520	. . 3 ⊢ (𝜑 → (∅ ∈ 𝒫 ℝ ∧ (◡𝐹 “ ∅) ∈ (𝑆 ↾t 𝐷)))
21		imaeq2 6058	. . . . 5 ⊢ (𝑒 = ∅ → (◡𝐹 “ 𝑒) = (◡𝐹 “ ∅))
22	21	eleq1d 2846	. . . 4 ⊢ (𝑒 = ∅ → ((◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ ∅) ∈ (𝑆 ↾t 𝐷)))
23	22, 1	elrab2 3653	. . 3 ⊢ (∅ ∈ 𝑇 ↔ (∅ ∈ 𝒫 ℝ ∧ (◡𝐹 “ ∅) ∈ (𝑆 ↾t 𝐷)))
24	20, 23	sylibr 237	. 2 ⊢ (𝜑 → ∅ ∈ 𝑇)
25		eqid 2761	. 2 ⊢ ∪ 𝑇 = ∪ 𝑇
26		nfv 1942	. . . . . . 7 ⊢ Ⅎ𝑦𝜑
27		nfcv 2923	. . . . . . . . . . . 12 ⊢ Ⅎ𝑒𝑦
28		nfrab1 3434	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑒{𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)}
29	1, 28	nfcxfr 2921	. . . . . . . . . . . 12 ⊢ Ⅎ𝑒𝑇
30	27, 29	eluni2f 45791	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ∪ 𝑇 ↔ ∃𝑒 ∈ 𝑇 𝑦 ∈ 𝑒)
31	30	bilani 509	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ∪ 𝑇) → ∃𝑒 ∈ 𝑇 𝑦 ∈ 𝑒)
32		nfv 1942	. . . . . . . . . . . 12 ⊢ Ⅎ𝑒𝜑
33	29	nfuni 4878	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑒∪ 𝑇
34	27, 33	nfel 2937	. . . . . . . . . . . 12 ⊢ Ⅎ𝑒 𝑦 ∈ ∪ 𝑇
35	32, 34	nfan 1927	. . . . . . . . . . 11 ⊢ Ⅎ𝑒(𝜑 ∧ 𝑦 ∈ ∪ 𝑇)
36	27	nfel1 2939	. . . . . . . . . . 11 ⊢ Ⅎ𝑒 𝑦 ∈ ℝ
37	1	eleq2i 2853	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 ∈ 𝑇 ↔ 𝑒 ∈ {𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)})
38	37	biimpi 219	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 ∈ 𝑇 → 𝑒 ∈ {𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)})
39		rabidim1 3436	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 ∈ {𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)} → 𝑒 ∈ 𝒫 ℝ)
40	38, 39	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 ∈ 𝑇 → 𝑒 ∈ 𝒫 ℝ)
41		elpwi 4568	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 ∈ 𝒫 ℝ → 𝑒 ⊆ ℝ)
42	40, 41	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝑒 ∈ 𝑇 → 𝑒 ⊆ ℝ)
43	42	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝑒 ∈ 𝑇 ∧ 𝑦 ∈ 𝑒) → 𝑒 ⊆ ℝ)
44		simpr 489	. . . . . . . . . . . . . 14 ⊢ ((𝑒 ∈ 𝑇 ∧ 𝑦 ∈ 𝑒) → 𝑦 ∈ 𝑒)
45	43, 44	sseldd 3937	. . . . . . . . . . . . 13 ⊢ ((𝑒 ∈ 𝑇 ∧ 𝑦 ∈ 𝑒) → 𝑦 ∈ ℝ)
46	45	ex 417	. . . . . . . . . . . 12 ⊢ (𝑒 ∈ 𝑇 → (𝑦 ∈ 𝑒 → 𝑦 ∈ ℝ))
47	46	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ∪ 𝑇) → (𝑒 ∈ 𝑇 → (𝑦 ∈ 𝑒 → 𝑦 ∈ ℝ)))
48	35, 36, 47	rexlimd 3270	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ∪ 𝑇) → (∃𝑒 ∈ 𝑇 𝑦 ∈ 𝑒 → 𝑦 ∈ ℝ))
49	31, 48	mpd 16	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ∪ 𝑇) → 𝑦 ∈ ℝ)
50	49	ex 417	. . . . . . . 8 ⊢ (𝜑 → (𝑦 ∈ ∪ 𝑇 → 𝑦 ∈ ℝ))
51		ovexd 7445	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑦 − 1)(,)(𝑦 + 1)) ∈ V)
52		ioossre 13433	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 − 1)(,)(𝑦 + 1)) ⊆ ℝ
53	52	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑦 − 1)(,)(𝑦 + 1)) ⊆ ℝ)
54	51, 53	elpwd 4567	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝒫 ℝ)
55	54	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝒫 ℝ)
56	10, 12, 13	smff 47416	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)
57	56	ffnd 6706	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹 Fn 𝐷)
58		fncnvima2 7056	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 Fn 𝐷 → (◡𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) = {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) ∈ ((𝑦 − 1)(,)(𝑦 + 1))})
59	57, 58	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (◡𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) = {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) ∈ ((𝑦 − 1)(,)(𝑦 + 1))})
60	59	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (◡𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) = {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) ∈ ((𝑦 − 1)(,)(𝑦 + 1))})
61		nfv 1942	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ ℝ)
62	10	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑆 ∈ SAlg)
63	15	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝐷 ∈ V)
64	56	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐹:𝐷⟶ℝ)
65		simpr 489	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝐷)
66	64, 65	ffvelcdmd 7080	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝐹‘𝑥) ∈ ℝ)
67	66	adantlr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐷) → (𝐹‘𝑥) ∈ ℝ)
68	56	feqmptd 6949	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ (𝐹‘𝑥)))
69	68	eqcomd 2767	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ (𝐹‘𝑥)) = 𝐹)
70	69, 12	eqeltrd 2861	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ (𝐹‘𝑥)) ∈ (SMblFn‘𝑆))
71	70	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑥 ∈ 𝐷 ↦ (𝐹‘𝑥)) ∈ (SMblFn‘𝑆))
72		peano2rem 11524	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℝ → (𝑦 − 1) ∈ ℝ)
73	72	rexrd 11258	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℝ → (𝑦 − 1) ∈ ℝ*)
74	73	adantl 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 − 1) ∈ ℝ*)
75		peano2re 11382	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℝ → (𝑦 + 1) ∈ ℝ)
76	75	rexrd 11258	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℝ → (𝑦 + 1) ∈ ℝ*)
77	76	adantl 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + 1) ∈ ℝ*)
78	61, 62, 63, 67, 71, 74, 77	smfpimioompt 47470	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) ∈ ((𝑦 − 1)(,)(𝑦 + 1))} ∈ (𝑆 ↾t 𝐷))
79	60, 78	eqeltrd 2861	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (◡𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) ∈ (𝑆 ↾t 𝐷))
80	55, 79	jca 520	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝒫 ℝ ∧ (◡𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) ∈ (𝑆 ↾t 𝐷)))
81		imaeq2 6058	. . . . . . . . . . . . . 14 ⊢ (𝑒 = ((𝑦 − 1)(,)(𝑦 + 1)) → (◡𝐹 “ 𝑒) = (◡𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))))
82	81	eleq1d 2846	. . . . . . . . . . . . 13 ⊢ (𝑒 = ((𝑦 − 1)(,)(𝑦 + 1)) → ((◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) ∈ (𝑆 ↾t 𝐷)))
83	82, 1	elrab2 3653	. . . . . . . . . . . 12 ⊢ (((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝑇 ↔ (((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝒫 ℝ ∧ (◡𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) ∈ (𝑆 ↾t 𝐷)))
84	80, 83	sylibr 237	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝑇)
85		id 23	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℝ → 𝑦 ∈ ℝ)
86		ltm1 12056	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℝ → (𝑦 − 1) < 𝑦)
87		ltp1 12054	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℝ → 𝑦 < (𝑦 + 1))
88	73, 76, 85, 86, 87	eliood 46184	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ → 𝑦 ∈ ((𝑦 − 1)(,)(𝑦 + 1)))
89	88	adantl 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ((𝑦 − 1)(,)(𝑦 + 1)))
90		nfv 1942	. . . . . . . . . . . 12 ⊢ Ⅎ𝑒 𝑦 ∈ ((𝑦 − 1)(,)(𝑦 + 1))
91		nfcv 2923	. . . . . . . . . . . 12 ⊢ Ⅎ𝑒((𝑦 − 1)(,)(𝑦 + 1))
92		eleq2 2850	. . . . . . . . . . . 12 ⊢ (𝑒 = ((𝑦 − 1)(,)(𝑦 + 1)) → (𝑦 ∈ 𝑒 ↔ 𝑦 ∈ ((𝑦 − 1)(,)(𝑦 + 1))))
93	90, 91, 29, 92	rspcef 45762	. . . . . . . . . . 11 ⊢ ((((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝑇 ∧ 𝑦 ∈ ((𝑦 − 1)(,)(𝑦 + 1))) → ∃𝑒 ∈ 𝑇 𝑦 ∈ 𝑒)
94	84, 89, 93	syl2anc 595	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ∃𝑒 ∈ 𝑇 𝑦 ∈ 𝑒)
95	94, 30	sylibr 237	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ∪ 𝑇)
96	95	ex 417	. . . . . . . 8 ⊢ (𝜑 → (𝑦 ∈ ℝ → 𝑦 ∈ ∪ 𝑇))
97	50, 96	impbid 215	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ ∪ 𝑇 ↔ 𝑦 ∈ ℝ))
98	26, 97	alrimi 2247	. . . . . 6 ⊢ (𝜑 → ∀𝑦(𝑦 ∈ ∪ 𝑇 ↔ 𝑦 ∈ ℝ))
99		dfcleq 2754	. . . . . 6 ⊢ (∪ 𝑇 = ℝ ↔ ∀𝑦(𝑦 ∈ ∪ 𝑇 ↔ 𝑦 ∈ ℝ))
100	98, 99	sylibr 237	. . . . 5 ⊢ (𝜑 → ∪ 𝑇 = ℝ)
101	100	difeq1d 4079	. . . 4 ⊢ (𝜑 → (∪ 𝑇 ∖ 𝑥) = (ℝ ∖ 𝑥))
102	101	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (∪ 𝑇 ∖ 𝑥) = (ℝ ∖ 𝑥))
103		difss 4089	. . . . . . 7 ⊢ (ℝ ∖ 𝑥) ⊆ ℝ
104	2, 103	ssexi 5292	. . . . . . . 8 ⊢ (ℝ ∖ 𝑥) ∈ V
105		elpwg 4564	. . . . . . . 8 ⊢ ((ℝ ∖ 𝑥) ∈ V → ((ℝ ∖ 𝑥) ∈ 𝒫 ℝ ↔ (ℝ ∖ 𝑥) ⊆ ℝ))
106	104, 105	ax-mp 5	. . . . . . 7 ⊢ ((ℝ ∖ 𝑥) ∈ 𝒫 ℝ ↔ (ℝ ∖ 𝑥) ⊆ ℝ)
107	103, 106	mpbir 234	. . . . . 6 ⊢ (ℝ ∖ 𝑥) ∈ 𝒫 ℝ
108	107	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (ℝ ∖ 𝑥) ∈ 𝒫 ℝ)
109	56	ffund 6710	. . . . . . . . 9 ⊢ (𝜑 → Fun 𝐹)
110		difpreima 7060	. . . . . . . . 9 ⊢ (Fun 𝐹 → (◡𝐹 “ (ℝ ∖ 𝑥)) = ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ 𝑥)))
111	109, 110	syl 18	. . . . . . . 8 ⊢ (𝜑 → (◡𝐹 “ (ℝ ∖ 𝑥)) = ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ 𝑥)))
112		fimacnv 6728	. . . . . . . . . . 11 ⊢ (𝐹:𝐷⟶ℝ → (◡𝐹 “ ℝ) = 𝐷)
113	56, 112	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (◡𝐹 “ ℝ) = 𝐷)
114	10, 14	restuni4 45809	. . . . . . . . . 10 ⊢ (𝜑 → ∪ (𝑆 ↾t 𝐷) = 𝐷)
115	113, 114	eqtr4d 2799	. . . . . . . . 9 ⊢ (𝜑 → (◡𝐹 “ ℝ) = ∪ (𝑆 ↾t 𝐷))
116	115	difeq1d 4079	. . . . . . . 8 ⊢ (𝜑 → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ 𝑥)) = (∪ (𝑆 ↾t 𝐷) ∖ (◡𝐹 “ 𝑥)))
117	111, 116	eqtrd 2796	. . . . . . 7 ⊢ (𝜑 → (◡𝐹 “ (ℝ ∖ 𝑥)) = (∪ (𝑆 ↾t 𝐷) ∖ (◡𝐹 “ 𝑥)))
118	117	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (◡𝐹 “ (ℝ ∖ 𝑥)) = (∪ (𝑆 ↾t 𝐷) ∖ (◡𝐹 “ 𝑥)))
119	17	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝑆 ↾t 𝐷) ∈ SAlg)
120		imaeq2 6058	. . . . . . . . . . . 12 ⊢ (𝑒 = 𝑥 → (◡𝐹 “ 𝑒) = (◡𝐹 “ 𝑥))
121	120	eleq1d 2846	. . . . . . . . . . 11 ⊢ (𝑒 = 𝑥 → ((◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ 𝑥) ∈ (𝑆 ↾t 𝐷)))
122	121, 1	elrab2 3653	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝑇 ↔ (𝑥 ∈ 𝒫 ℝ ∧ (◡𝐹 “ 𝑥) ∈ (𝑆 ↾t 𝐷)))
123	122	biimpi 219	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑇 → (𝑥 ∈ 𝒫 ℝ ∧ (◡𝐹 “ 𝑥) ∈ (𝑆 ↾t 𝐷)))
124	123	simprd 500	. . . . . . . 8 ⊢ (𝑥 ∈ 𝑇 → (◡𝐹 “ 𝑥) ∈ (𝑆 ↾t 𝐷))
125	124	adantl 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (◡𝐹 “ 𝑥) ∈ (𝑆 ↾t 𝐷))
126	119, 125	saldifcld 47031	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (∪ (𝑆 ↾t 𝐷) ∖ (◡𝐹 “ 𝑥)) ∈ (𝑆 ↾t 𝐷))
127	118, 126	eqeltrd 2861	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ (𝑆 ↾t 𝐷))
128	108, 127	jca 520	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → ((ℝ ∖ 𝑥) ∈ 𝒫 ℝ ∧ (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ (𝑆 ↾t 𝐷)))
129		imaeq2 6058	. . . . . 6 ⊢ (𝑒 = (ℝ ∖ 𝑥) → (◡𝐹 “ 𝑒) = (◡𝐹 “ (ℝ ∖ 𝑥)))
130	129	eleq1d 2846	. . . . 5 ⊢ (𝑒 = (ℝ ∖ 𝑥) → ((◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ (𝑆 ↾t 𝐷)))
131	130, 1	elrab2 3653	. . . 4 ⊢ ((ℝ ∖ 𝑥) ∈ 𝑇 ↔ ((ℝ ∖ 𝑥) ∈ 𝒫 ℝ ∧ (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ (𝑆 ↾t 𝐷)))
132	128, 131	sylibr 237	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (ℝ ∖ 𝑥) ∈ 𝑇)
133	102, 132	eqeltrd 2861	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (∪ 𝑇 ∖ 𝑥) ∈ 𝑇)
134		nnex 12238	. . . . . . . 8 ⊢ ℕ ∈ V
135		fvex 6894	. . . . . . . 8 ⊢ (𝑔‘𝑛) ∈ V
136	134, 135	iunex 7964	. . . . . . 7 ⊢ ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) ∈ V
137	136	a1i 11	. . . . . 6 ⊢ (𝑔:ℕ⟶𝑇 → ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) ∈ V)
138		ffvelcdm 7076	. . . . . . . 8 ⊢ ((𝑔:ℕ⟶𝑇 ∧ 𝑛 ∈ ℕ) → (𝑔‘𝑛) ∈ 𝑇)
139	1	eleq2i 2853	. . . . . . . . 9 ⊢ ((𝑔‘𝑛) ∈ 𝑇 ↔ (𝑔‘𝑛) ∈ {𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)})
140	139	biimpi 219	. . . . . . . 8 ⊢ ((𝑔‘𝑛) ∈ 𝑇 → (𝑔‘𝑛) ∈ {𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)})
141		elrabi 3645	. . . . . . . 8 ⊢ ((𝑔‘𝑛) ∈ {𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)} → (𝑔‘𝑛) ∈ 𝒫 ℝ)
142		elpwi 4568	. . . . . . . 8 ⊢ ((𝑔‘𝑛) ∈ 𝒫 ℝ → (𝑔‘𝑛) ⊆ ℝ)
143	138, 140, 141, 142	4syl 20	. . . . . . 7 ⊢ ((𝑔:ℕ⟶𝑇 ∧ 𝑛 ∈ ℕ) → (𝑔‘𝑛) ⊆ ℝ)
144	143	iunssd 5014	. . . . . 6 ⊢ (𝑔:ℕ⟶𝑇 → ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) ⊆ ℝ)
145	137, 144	elpwd 4567	. . . . 5 ⊢ (𝑔:ℕ⟶𝑇 → ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) ∈ 𝒫 ℝ)
146	145	adantl 486	. . . 4 ⊢ ((𝜑 ∧ 𝑔:ℕ⟶𝑇) → ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) ∈ 𝒫 ℝ)
147		imaiun 7243	. . . . . 6 ⊢ (◡𝐹 “ ∪ 𝑛 ∈ ℕ (𝑔‘𝑛)) = ∪ 𝑛 ∈ ℕ (◡𝐹 “ (𝑔‘𝑛))
148	147	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑔:ℕ⟶𝑇) → (◡𝐹 “ ∪ 𝑛 ∈ ℕ (𝑔‘𝑛)) = ∪ 𝑛 ∈ ℕ (◡𝐹 “ (𝑔‘𝑛)))
149	17	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔:ℕ⟶𝑇) → (𝑆 ↾t 𝐷) ∈ SAlg)
150		nnct 14016	. . . . . . 7 ⊢ ℕ ≼ ω
151	150	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔:ℕ⟶𝑇) → ℕ ≼ ω)
152		imaeq2 6058	. . . . . . . . . . . 12 ⊢ (𝑒 = (𝑔‘𝑛) → (◡𝐹 “ 𝑒) = (◡𝐹 “ (𝑔‘𝑛)))
153	152	eleq1d 2846	. . . . . . . . . . 11 ⊢ (𝑒 = (𝑔‘𝑛) → ((◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷)))
154	153, 1	elrab2 3653	. . . . . . . . . 10 ⊢ ((𝑔‘𝑛) ∈ 𝑇 ↔ ((𝑔‘𝑛) ∈ 𝒫 ℝ ∧ (◡𝐹 “ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷)))
155	154	biimpi 219	. . . . . . . . 9 ⊢ ((𝑔‘𝑛) ∈ 𝑇 → ((𝑔‘𝑛) ∈ 𝒫 ℝ ∧ (◡𝐹 “ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷)))
156	155	simprd 500	. . . . . . . 8 ⊢ ((𝑔‘𝑛) ∈ 𝑇 → (◡𝐹 “ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷))
157	138, 156	syl 18	. . . . . . 7 ⊢ ((𝑔:ℕ⟶𝑇 ∧ 𝑛 ∈ ℕ) → (◡𝐹 “ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷))
158	157	adantll 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:ℕ⟶𝑇) ∧ 𝑛 ∈ ℕ) → (◡𝐹 “ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷))
159	149, 151, 158	saliuncl 47007	. . . . 5 ⊢ ((𝜑 ∧ 𝑔:ℕ⟶𝑇) → ∪ 𝑛 ∈ ℕ (◡𝐹 “ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷))
160	148, 159	eqeltrd 2861	. . . 4 ⊢ ((𝜑 ∧ 𝑔:ℕ⟶𝑇) → (◡𝐹 “ ∪ 𝑛 ∈ ℕ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷))
161	146, 160	jca 520	. . 3 ⊢ ((𝜑 ∧ 𝑔:ℕ⟶𝑇) → (∪ 𝑛 ∈ ℕ (𝑔‘𝑛) ∈ 𝒫 ℝ ∧ (◡𝐹 “ ∪ 𝑛 ∈ ℕ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷)))
162		imaeq2 6058	. . . . 5 ⊢ (𝑒 = ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) → (◡𝐹 “ 𝑒) = (◡𝐹 “ ∪ 𝑛 ∈ ℕ (𝑔‘𝑛)))
163	162	eleq1d 2846	. . . 4 ⊢ (𝑒 = ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) → ((◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ ∪ 𝑛 ∈ ℕ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷)))
164	163, 1	elrab2 3653	. . 3 ⊢ (∪ 𝑛 ∈ ℕ (𝑔‘𝑛) ∈ 𝑇 ↔ (∪ 𝑛 ∈ ℕ (𝑔‘𝑛) ∈ 𝒫 ℝ ∧ (◡𝐹 “ ∪ 𝑛 ∈ ℕ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷)))
165	161, 164	sylibr 237	. 2 ⊢ ((𝜑 ∧ 𝑔:ℕ⟶𝑇) → ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) ∈ 𝑇)
166	5, 24, 25, 133, 165	issalnnd 47029	1 ⊢ (𝜑 → 𝑇 ∈ SAlg)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1566   = wceq 1568   ∈ wcel 2141  ∃wrex 3087  {crab 3414  Vcvv 3453   ∖ cdif 3901   ⊆ wss 3904  ∅c0 4285  𝒫 cpw 4561  ∪ cuni 4871  ∪ ciun 4955   class class class wbr 5108   ↦ cmpt 5191  ^◡ccnv 5660  dom cdm 5661   “ cima 5664  Fun wfun 6530   Fn wfn 6531  ⟶wf 6532  ‘cfv 6536  (class class class)co 7410  ωcom 7861   ≼ cdom 8940  ℝcr 11098  1c1 11100   + caddc 11102  ℝ^*cxr 11241   − cmin 11440  ℕcn 12232  (,)cioo 13371   ↾_t crest 17472  SAlgcsalg 46992  SMblFncsmblfn 47379

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5237  ax-sep 5256  ax-nul 5268  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-inf2 9609  ax-cc 10418  ax-ac2 10446  ax-cnex 11155  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-mulcom 11163  ax-addass 11164  ax-mulass 11165  ax-distr 11166  ax-i2m1 11167  ax-1ne0 11168  ax-1rid 11169  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172  ax-pre-lttri 11173  ax-pre-lttrn 11174  ax-pre-ltadd 11175  ax-pre-mulgt0 11176  ax-pre-sup 11177

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-int 4912  df-iun 4957  df-iin 4958  df-br 5109  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-se 5615  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7862  df-1st 7985  df-2nd 7986  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-1o 8452  df-2o 8453  df-er 8693  df-map 8825  df-pm 8826  df-en 8943  df-dom 8944  df-sdom 8945  df-fin 8946  df-sup 9401  df-inf 9402  df-card 9924  df-acn 9927  df-ac 10099  df-pnf 11244  df-mnf 11245  df-xr 11246  df-ltxr 11247  df-le 11248  df-sub 11442  df-neg 11443  df-div 11871  df-nn 12233  df-n0 12504  df-z 12591  df-uz 12862  df-q 12972  df-rp 13016  df-ioo 13375  df-ico 13377  df-fl 13824  df-rest 17474  df-salg 46993  df-smblfn 47380

This theorem is referenced by:  smfpimbor1lem1  47482  smfpimbor1lem2  47483