Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sssmf Structured version   Visualization version   GIF version

Theorem sssmf 40270
Description: The restriction of a sigma-measurable function, is sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
Hypotheses
Ref Expression
sssmf.s (𝜑𝑆 ∈ SAlg)
sssmf.f (𝜑𝐹 ∈ (SMblFn‘𝑆))
Assertion
Ref Expression
sssmf (𝜑 → (𝐹𝐵) ∈ (SMblFn‘𝑆))

Proof of Theorem sssmf
Dummy variables 𝑎 𝑤 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1840 . 2 𝑎𝜑
2 sssmf.s . 2 (𝜑𝑆 ∈ SAlg)
3 inss2 3814 . . 3 (𝐵 ∩ dom 𝐹) ⊆ dom 𝐹
4 sssmf.f . . . 4 (𝜑𝐹 ∈ (SMblFn‘𝑆))
5 eqid 2621 . . . 4 dom 𝐹 = dom 𝐹
62, 4, 5smfdmss 40265 . . 3 (𝜑 → dom 𝐹 𝑆)
73, 6syl5ss 3595 . 2 (𝜑 → (𝐵 ∩ dom 𝐹) ⊆ 𝑆)
82, 4, 5smff 40264 . . . . 5 (𝜑𝐹:dom 𝐹⟶ℝ)
93a1i 11 . . . . 5 (𝜑 → (𝐵 ∩ dom 𝐹) ⊆ dom 𝐹)
10 fssres 6029 . . . . 5 ((𝐹:dom 𝐹⟶ℝ ∧ (𝐵 ∩ dom 𝐹) ⊆ dom 𝐹) → (𝐹 ↾ (𝐵 ∩ dom 𝐹)):(𝐵 ∩ dom 𝐹)⟶ℝ)
118, 9, 10syl2anc 692 . . . 4 (𝜑 → (𝐹 ↾ (𝐵 ∩ dom 𝐹)):(𝐵 ∩ dom 𝐹)⟶ℝ)
128freld 38917 . . . . . . 7 (𝜑 → Rel 𝐹)
13 resindm 5405 . . . . . . 7 (Rel 𝐹 → (𝐹 ↾ (𝐵 ∩ dom 𝐹)) = (𝐹𝐵))
1412, 13syl 17 . . . . . 6 (𝜑 → (𝐹 ↾ (𝐵 ∩ dom 𝐹)) = (𝐹𝐵))
1514eqcomd 2627 . . . . 5 (𝜑 → (𝐹𝐵) = (𝐹 ↾ (𝐵 ∩ dom 𝐹)))
16 dmres 5380 . . . . . 6 dom (𝐹𝐵) = (𝐵 ∩ dom 𝐹)
1716a1i 11 . . . . 5 (𝜑 → dom (𝐹𝐵) = (𝐵 ∩ dom 𝐹))
1815, 17feq12d 5992 . . . 4 (𝜑 → ((𝐹𝐵):dom (𝐹𝐵)⟶ℝ ↔ (𝐹 ↾ (𝐵 ∩ dom 𝐹)):(𝐵 ∩ dom 𝐹)⟶ℝ))
1911, 18mpbird 247 . . 3 (𝜑 → (𝐹𝐵):dom (𝐹𝐵)⟶ℝ)
2017feq2d 5990 . . 3 (𝜑 → ((𝐹𝐵):dom (𝐹𝐵)⟶ℝ ↔ (𝐹𝐵):(𝐵 ∩ dom 𝐹)⟶ℝ))
2119, 20mpbid 222 . 2 (𝜑 → (𝐹𝐵):(𝐵 ∩ dom 𝐹)⟶ℝ)
222adantr 481 . . . . 5 ((𝜑𝑎 ∈ ℝ) → 𝑆 ∈ SAlg)
234adantr 481 . . . . 5 ((𝜑𝑎 ∈ ℝ) → 𝐹 ∈ (SMblFn‘𝑆))
24 simpr 477 . . . . 5 ((𝜑𝑎 ∈ ℝ) → 𝑎 ∈ ℝ)
2522, 23, 5, 24smfpreimalt 40263 . . . 4 ((𝜑𝑎 ∈ ℝ) → {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} ∈ (𝑆t dom 𝐹))
264dmexd 38914 . . . . . 6 (𝜑 → dom 𝐹 ∈ V)
27 elrest 16012 . . . . . 6 ((𝑆 ∈ SAlg ∧ dom 𝐹 ∈ V) → ({𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} ∈ (𝑆t dom 𝐹) ↔ ∃𝑤𝑆 {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹)))
282, 26, 27syl2anc 692 . . . . 5 (𝜑 → ({𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} ∈ (𝑆t dom 𝐹) ↔ ∃𝑤𝑆 {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹)))
2928adantr 481 . . . 4 ((𝜑𝑎 ∈ ℝ) → ({𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} ∈ (𝑆t dom 𝐹) ↔ ∃𝑤𝑆 {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹)))
3025, 29mpbid 222 . . 3 ((𝜑𝑎 ∈ ℝ) → ∃𝑤𝑆 {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹))
31 elinel1 3779 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐵 ∩ dom 𝐹) → 𝑥𝐵)
3231fvresd 6167 . . . . . . . . . . . 12 (𝑥 ∈ (𝐵 ∩ dom 𝐹) → ((𝐹𝐵)‘𝑥) = (𝐹𝑥))
3332breq1d 4625 . . . . . . . . . . 11 (𝑥 ∈ (𝐵 ∩ dom 𝐹) → (((𝐹𝐵)‘𝑥) < 𝑎 ↔ (𝐹𝑥) < 𝑎))
3433rabbiia 3173 . . . . . . . . . 10 {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ ((𝐹𝐵)‘𝑥) < 𝑎} = {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹𝑥) < 𝑎}
3534a1i 11 . . . . . . . . 9 ({𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) → {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ ((𝐹𝐵)‘𝑥) < 𝑎} = {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹𝑥) < 𝑎})
36 rabss2 3666 . . . . . . . . . . . . 13 ((𝐵 ∩ dom 𝐹) ⊆ dom 𝐹 → {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹𝑥) < 𝑎} ⊆ {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎})
373, 36ax-mp 5 . . . . . . . . . . . 12 {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹𝑥) < 𝑎} ⊆ {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎}
38 id 22 . . . . . . . . . . . . 13 ({𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) → {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹))
39 inss1 3813 . . . . . . . . . . . . . 14 (𝑤 ∩ dom 𝐹) ⊆ 𝑤
4039a1i 11 . . . . . . . . . . . . 13 ({𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) → (𝑤 ∩ dom 𝐹) ⊆ 𝑤)
4138, 40eqsstrd 3620 . . . . . . . . . . . 12 ({𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) → {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} ⊆ 𝑤)
4237, 41syl5ss 3595 . . . . . . . . . . 11 ({𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) → {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹𝑥) < 𝑎} ⊆ 𝑤)
43 ssrab2 3668 . . . . . . . . . . . 12 {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹𝑥) < 𝑎} ⊆ (𝐵 ∩ dom 𝐹)
4443a1i 11 . . . . . . . . . . 11 ({𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) → {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹𝑥) < 𝑎} ⊆ (𝐵 ∩ dom 𝐹))
4542, 44ssind 3817 . . . . . . . . . 10 ({𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) → {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹𝑥) < 𝑎} ⊆ (𝑤 ∩ (𝐵 ∩ dom 𝐹)))
46 nfrab1 3111 . . . . . . . . . . . . 13 𝑥{𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎}
47 nfcv 2761 . . . . . . . . . . . . 13 𝑥(𝑤 ∩ dom 𝐹)
4846, 47nfeq 2772 . . . . . . . . . . . 12 𝑥{𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹)
49 elinel2 3780 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝑤 ∩ (𝐵 ∩ dom 𝐹)) → 𝑥 ∈ (𝐵 ∩ dom 𝐹))
5049adantl 482 . . . . . . . . . . . . . . . . . 18 (({𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) ∧ 𝑥 ∈ (𝑤 ∩ (𝐵 ∩ dom 𝐹))) → 𝑥 ∈ (𝐵 ∩ dom 𝐹))
51 elinel1 3779 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝑤 ∩ (𝐵 ∩ dom 𝐹)) → 𝑥𝑤)
523sseli 3580 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (𝐵 ∩ dom 𝐹) → 𝑥 ∈ dom 𝐹)
5349, 52syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝑤 ∩ (𝐵 ∩ dom 𝐹)) → 𝑥 ∈ dom 𝐹)
5451, 53elind 3778 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝑤 ∩ (𝐵 ∩ dom 𝐹)) → 𝑥 ∈ (𝑤 ∩ dom 𝐹))
5554adantl 482 . . . . . . . . . . . . . . . . . . . 20 (({𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) ∧ 𝑥 ∈ (𝑤 ∩ (𝐵 ∩ dom 𝐹))) → 𝑥 ∈ (𝑤 ∩ dom 𝐹))
5638eqcomd 2627 . . . . . . . . . . . . . . . . . . . . 21 ({𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) → (𝑤 ∩ dom 𝐹) = {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎})
5756adantr 481 . . . . . . . . . . . . . . . . . . . 20 (({𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) ∧ 𝑥 ∈ (𝑤 ∩ (𝐵 ∩ dom 𝐹))) → (𝑤 ∩ dom 𝐹) = {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎})
5855, 57eleqtrd 2700 . . . . . . . . . . . . . . . . . . 19 (({𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) ∧ 𝑥 ∈ (𝑤 ∩ (𝐵 ∩ dom 𝐹))) → 𝑥 ∈ {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎})
59 rabid 3106 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} ↔ (𝑥 ∈ dom 𝐹 ∧ (𝐹𝑥) < 𝑎))
6059biimpi 206 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} → (𝑥 ∈ dom 𝐹 ∧ (𝐹𝑥) < 𝑎))
6160simprd 479 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} → (𝐹𝑥) < 𝑎)
6258, 61syl 17 . . . . . . . . . . . . . . . . . 18 (({𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) ∧ 𝑥 ∈ (𝑤 ∩ (𝐵 ∩ dom 𝐹))) → (𝐹𝑥) < 𝑎)
6350, 62jca 554 . . . . . . . . . . . . . . . . 17 (({𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) ∧ 𝑥 ∈ (𝑤 ∩ (𝐵 ∩ dom 𝐹))) → (𝑥 ∈ (𝐵 ∩ dom 𝐹) ∧ (𝐹𝑥) < 𝑎))
64 rabid 3106 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹𝑥) < 𝑎} ↔ (𝑥 ∈ (𝐵 ∩ dom 𝐹) ∧ (𝐹𝑥) < 𝑎))
6563, 64sylibr 224 . . . . . . . . . . . . . . . 16 (({𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) ∧ 𝑥 ∈ (𝑤 ∩ (𝐵 ∩ dom 𝐹))) → 𝑥 ∈ {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹𝑥) < 𝑎})
6665ex 450 . . . . . . . . . . . . . . 15 ({𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) → (𝑥 ∈ (𝑤 ∩ (𝐵 ∩ dom 𝐹)) → 𝑥 ∈ {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹𝑥) < 𝑎}))
6748, 66ralrimi 2951 . . . . . . . . . . . . . 14 ({𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) → ∀𝑥 ∈ (𝑤 ∩ (𝐵 ∩ dom 𝐹))𝑥 ∈ {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹𝑥) < 𝑎})
68 nfcv 2761 . . . . . . . . . . . . . . 15 𝑥(𝑤 ∩ (𝐵 ∩ dom 𝐹))
69 nfrab1 3111 . . . . . . . . . . . . . . 15 𝑥{𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹𝑥) < 𝑎}
7068, 69dfss3f 3576 . . . . . . . . . . . . . 14 ((𝑤 ∩ (𝐵 ∩ dom 𝐹)) ⊆ {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹𝑥) < 𝑎} ↔ ∀𝑥 ∈ (𝑤 ∩ (𝐵 ∩ dom 𝐹))𝑥 ∈ {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹𝑥) < 𝑎})
7167, 70sylibr 224 . . . . . . . . . . . . 13 ({𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) → (𝑤 ∩ (𝐵 ∩ dom 𝐹)) ⊆ {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹𝑥) < 𝑎})
7271sseld 3583 . . . . . . . . . . . 12 ({𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) → (𝑥 ∈ (𝑤 ∩ (𝐵 ∩ dom 𝐹)) → 𝑥 ∈ {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹𝑥) < 𝑎}))
7348, 72ralrimi 2951 . . . . . . . . . . 11 ({𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) → ∀𝑥 ∈ (𝑤 ∩ (𝐵 ∩ dom 𝐹))𝑥 ∈ {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹𝑥) < 𝑎})
7473, 70sylibr 224 . . . . . . . . . 10 ({𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) → (𝑤 ∩ (𝐵 ∩ dom 𝐹)) ⊆ {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹𝑥) < 𝑎})
7545, 74eqssd 3601 . . . . . . . . 9 ({𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) → {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ (𝐵 ∩ dom 𝐹)))
7635, 75eqtrd 2655 . . . . . . . 8 ({𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) → {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ ((𝐹𝐵)‘𝑥) < 𝑎} = (𝑤 ∩ (𝐵 ∩ dom 𝐹)))
7776adantl 482 . . . . . . 7 (((𝜑𝑎 ∈ ℝ) ∧ {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹)) → {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ ((𝐹𝐵)‘𝑥) < 𝑎} = (𝑤 ∩ (𝐵 ∩ dom 𝐹)))
78773adant2 1078 . . . . . 6 (((𝜑𝑎 ∈ ℝ) ∧ 𝑤𝑆 ∧ {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹)) → {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ ((𝐹𝐵)‘𝑥) < 𝑎} = (𝑤 ∩ (𝐵 ∩ dom 𝐹)))
79223ad2ant1 1080 . . . . . . 7 (((𝜑𝑎 ∈ ℝ) ∧ 𝑤𝑆 ∧ {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹)) → 𝑆 ∈ SAlg)
80 simp1l 1083 . . . . . . . 8 (((𝜑𝑎 ∈ ℝ) ∧ 𝑤𝑆 ∧ {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹)) → 𝜑)
8126, 9ssexd 4767 . . . . . . . 8 (𝜑 → (𝐵 ∩ dom 𝐹) ∈ V)
8280, 81syl 17 . . . . . . 7 (((𝜑𝑎 ∈ ℝ) ∧ 𝑤𝑆 ∧ {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹)) → (𝐵 ∩ dom 𝐹) ∈ V)
83 simp2 1060 . . . . . . 7 (((𝜑𝑎 ∈ ℝ) ∧ 𝑤𝑆 ∧ {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹)) → 𝑤𝑆)
84 eqid 2621 . . . . . . 7 (𝑤 ∩ (𝐵 ∩ dom 𝐹)) = (𝑤 ∩ (𝐵 ∩ dom 𝐹))
8579, 82, 83, 84elrestd 38797 . . . . . 6 (((𝜑𝑎 ∈ ℝ) ∧ 𝑤𝑆 ∧ {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹)) → (𝑤 ∩ (𝐵 ∩ dom 𝐹)) ∈ (𝑆t (𝐵 ∩ dom 𝐹)))
8678, 85eqeltrd 2698 . . . . 5 (((𝜑𝑎 ∈ ℝ) ∧ 𝑤𝑆 ∧ {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹)) → {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ ((𝐹𝐵)‘𝑥) < 𝑎} ∈ (𝑆t (𝐵 ∩ dom 𝐹)))
87863exp 1261 . . . 4 ((𝜑𝑎 ∈ ℝ) → (𝑤𝑆 → ({𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) → {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ ((𝐹𝐵)‘𝑥) < 𝑎} ∈ (𝑆t (𝐵 ∩ dom 𝐹)))))
8887rexlimdv 3023 . . 3 ((𝜑𝑎 ∈ ℝ) → (∃𝑤𝑆 {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) → {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ ((𝐹𝐵)‘𝑥) < 𝑎} ∈ (𝑆t (𝐵 ∩ dom 𝐹))))
8930, 88mpd 15 . 2 ((𝜑𝑎 ∈ ℝ) → {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ ((𝐹𝐵)‘𝑥) < 𝑎} ∈ (𝑆t (𝐵 ∩ dom 𝐹)))
901, 2, 7, 21, 89issmfd 40267 1 (𝜑 → (𝐹𝐵) ∈ (SMblFn‘𝑆))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wral 2907  wrex 2908  {crab 2911  Vcvv 3186  cin 3555  wss 3556   cuni 4404   class class class wbr 4615  dom cdm 5076  cres 5078  Rel wrel 5081  wf 5845  cfv 5849  (class class class)co 6607  cr 9882   < clt 10021  t crest 16005  SAlgcsalg 39851  SMblFncsmblfn 40232
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4733  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905  ax-cnex 9939  ax-resscn 9940  ax-pre-lttri 9957  ax-pre-lttrn 9958
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-op 4157  df-uni 4405  df-iun 4489  df-br 4616  df-opab 4676  df-mpt 4677  df-id 4991  df-po 4997  df-so 4998  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-1st 7116  df-2nd 7117  df-er 7690  df-pm 7808  df-en 7903  df-dom 7904  df-sdom 7905  df-pnf 10023  df-mnf 10024  df-xr 10025  df-ltxr 10026  df-le 10027  df-ioo 12124  df-ico 12126  df-rest 16007  df-smblfn 40233
This theorem is referenced by:  sssmfmpt  40282
  Copyright terms: Public domain W3C validator