| Step | Hyp | Ref
| Expression |
| 1 | | nfv 1914 |
. 2
⊢
Ⅎ𝑎𝜑 |
| 2 | | smfco.s |
. 2
⊢ (𝜑 → 𝑆 ∈ SAlg) |
| 3 | | cnvimass 6100 |
. . . 4
⊢ (◡𝐹 “ dom 𝐻) ⊆ dom 𝐹 |
| 4 | 3 | a1i 11 |
. . 3
⊢ (𝜑 → (◡𝐹 “ dom 𝐻) ⊆ dom 𝐹) |
| 5 | | smfco.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆)) |
| 6 | | eqid 2737 |
. . . 4
⊢ dom 𝐹 = dom 𝐹 |
| 7 | 2, 5, 6 | smfdmss 46748 |
. . 3
⊢ (𝜑 → dom 𝐹 ⊆ ∪ 𝑆) |
| 8 | 4, 7 | sstrd 3994 |
. 2
⊢ (𝜑 → (◡𝐹 “ dom 𝐻) ⊆ ∪ 𝑆) |
| 9 | | smfco.j |
. . . . . . . . 9
⊢ 𝐽 = (topGen‘ran
(,)) |
| 10 | | retop 24782 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) ∈ Top |
| 11 | 9, 10 | eqeltri 2837 |
. . . . . . . 8
⊢ 𝐽 ∈ Top |
| 12 | 11 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ Top) |
| 13 | | smfco.b |
. . . . . . 7
⊢ 𝐵 = (SalGen‘𝐽) |
| 14 | 12, 13 | salgencld 46364 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ SAlg) |
| 15 | | smfco.h |
. . . . . 6
⊢ (𝜑 → 𝐻 ∈ (SMblFn‘𝐵)) |
| 16 | | eqid 2737 |
. . . . . 6
⊢ dom 𝐻 = dom 𝐻 |
| 17 | 14, 15, 16 | smff 46747 |
. . . . 5
⊢ (𝜑 → 𝐻:dom 𝐻⟶ℝ) |
| 18 | 17 | ffund 6740 |
. . . 4
⊢ (𝜑 → Fun 𝐻) |
| 19 | 2, 5, 6 | smff 46747 |
. . . . 5
⊢ (𝜑 → 𝐹:dom 𝐹⟶ℝ) |
| 20 | 19 | ffund 6740 |
. . . 4
⊢ (𝜑 → Fun 𝐹) |
| 21 | 18, 20 | funcofd 6768 |
. . 3
⊢ (𝜑 → (𝐻 ∘ 𝐹):(◡𝐹 “ dom 𝐻)⟶ran 𝐻) |
| 22 | 17 | frnd 6744 |
. . 3
⊢ (𝜑 → ran 𝐻 ⊆ ℝ) |
| 23 | 21, 22 | fssd 6753 |
. 2
⊢ (𝜑 → (𝐻 ∘ 𝐹):(◡𝐹 “ dom 𝐻)⟶ℝ) |
| 24 | | cnvco 5896 |
. . . . 5
⊢ ◡(𝐻 ∘ 𝐹) = (◡𝐹 ∘ ◡𝐻) |
| 25 | 24 | imaeq1i 6075 |
. . . 4
⊢ (◡(𝐻 ∘ 𝐹) “ (-∞(,)𝑎)) = ((◡𝐹 ∘ ◡𝐻) “ (-∞(,)𝑎)) |
| 26 | 23 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (𝐻 ∘ 𝐹):(◡𝐹 “ dom 𝐻)⟶ℝ) |
| 27 | | rexr 11307 |
. . . . . 6
⊢ (𝑎 ∈ ℝ → 𝑎 ∈
ℝ*) |
| 28 | 27 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ*) |
| 29 | 26, 28 | preimaioomnf 46734 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (◡(𝐻 ∘ 𝐹) “ (-∞(,)𝑎)) = {𝑥 ∈ (◡𝐹 “ dom 𝐻) ∣ ((𝐻 ∘ 𝐹)‘𝑥) < 𝑎}) |
| 30 | | imaco 6271 |
. . . . 5
⊢ ((◡𝐹 ∘ ◡𝐻) “ (-∞(,)𝑎)) = (◡𝐹 “ (◡𝐻 “ (-∞(,)𝑎))) |
| 31 | 30 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → ((◡𝐹 ∘ ◡𝐻) “ (-∞(,)𝑎)) = (◡𝐹 “ (◡𝐻 “ (-∞(,)𝑎)))) |
| 32 | 25, 29, 31 | 3eqtr3a 2801 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ (◡𝐹 “ dom 𝐻) ∣ ((𝐻 ∘ 𝐹)‘𝑥) < 𝑎} = (◡𝐹 “ (◡𝐻 “ (-∞(,)𝑎)))) |
| 33 | 17 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝐻:dom 𝐻⟶ℝ) |
| 34 | 33, 28 | preimaioomnf 46734 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (◡𝐻 “ (-∞(,)𝑎)) = {𝑥 ∈ dom 𝐻 ∣ (𝐻‘𝑥) < 𝑎}) |
| 35 | 14 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝐵 ∈ SAlg) |
| 36 | 15 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝐻 ∈ (SMblFn‘𝐵)) |
| 37 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ) |
| 38 | 35, 36, 16, 37 | smfpreimalt 46746 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ dom 𝐻 ∣ (𝐻‘𝑥) < 𝑎} ∈ (𝐵 ↾t dom 𝐻)) |
| 39 | 34, 38 | eqeltrd 2841 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (◡𝐻 “ (-∞(,)𝑎)) ∈ (𝐵 ↾t dom 𝐻)) |
| 40 | 14 | elexd 3504 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ V) |
| 41 | 15 | dmexd 7925 |
. . . . . . 7
⊢ (𝜑 → dom 𝐻 ∈ V) |
| 42 | | elrest 17472 |
. . . . . . 7
⊢ ((𝐵 ∈ V ∧ dom 𝐻 ∈ V) → ((◡𝐻 “ (-∞(,)𝑎)) ∈ (𝐵 ↾t dom 𝐻) ↔ ∃𝑒 ∈ 𝐵 (◡𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻))) |
| 43 | 40, 41, 42 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ((◡𝐻 “ (-∞(,)𝑎)) ∈ (𝐵 ↾t dom 𝐻) ↔ ∃𝑒 ∈ 𝐵 (◡𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻))) |
| 44 | 43 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → ((◡𝐻 “ (-∞(,)𝑎)) ∈ (𝐵 ↾t dom 𝐻) ↔ ∃𝑒 ∈ 𝐵 (◡𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻))) |
| 45 | 39, 44 | mpbid 232 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → ∃𝑒 ∈ 𝐵 (◡𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻)) |
| 46 | | imaeq2 6074 |
. . . . . . . . 9
⊢ ((◡𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻) → (◡𝐹 “ (◡𝐻 “ (-∞(,)𝑎))) = (◡𝐹 “ (𝑒 ∩ dom 𝐻))) |
| 47 | 46 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐵 ∧ (◡𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻)) → (◡𝐹 “ (◡𝐻 “ (-∞(,)𝑎))) = (◡𝐹 “ (𝑒 ∩ dom 𝐻))) |
| 48 | | ovexd 7466 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐵) → (𝑆 ↾t dom 𝐹) ∈ V) |
| 49 | 5 | elexd 3504 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ V) |
| 50 | | cnvexg 7946 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ V → ◡𝐹 ∈ V) |
| 51 | | imaexg 7935 |
. . . . . . . . . . . . 13
⊢ (◡𝐹 ∈ V → (◡𝐹 “ dom 𝐻) ∈ V) |
| 52 | 49, 50, 51 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡𝐹 “ dom 𝐻) ∈ V) |
| 53 | 52 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐵) → (◡𝐹 “ dom 𝐻) ∈ V) |
| 54 | 2 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐵) → 𝑆 ∈ SAlg) |
| 55 | 5 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐵) → 𝐹 ∈ (SMblFn‘𝑆)) |
| 56 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐵) → 𝑒 ∈ 𝐵) |
| 57 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (◡𝐹 “ 𝑒) = (◡𝐹 “ 𝑒) |
| 58 | 54, 55, 6, 9, 13, 56, 57 | smfpimbor1 46815 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐵) → (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t dom 𝐹)) |
| 59 | | eqid 2737 |
. . . . . . . . . . 11
⊢ ((◡𝐹 “ 𝑒) ∩ (◡𝐹 “ dom 𝐻)) = ((◡𝐹 “ 𝑒) ∩ (◡𝐹 “ dom 𝐻)) |
| 60 | 48, 53, 58, 59 | elrestd 45113 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐵) → ((◡𝐹 “ 𝑒) ∩ (◡𝐹 “ dom 𝐻)) ∈ ((𝑆 ↾t dom 𝐹) ↾t (◡𝐹 “ dom 𝐻))) |
| 61 | | inpreima 7084 |
. . . . . . . . . . . 12
⊢ (Fun
𝐹 → (◡𝐹 “ (𝑒 ∩ dom 𝐻)) = ((◡𝐹 “ 𝑒) ∩ (◡𝐹 “ dom 𝐻))) |
| 62 | 20, 61 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (◡𝐹 “ (𝑒 ∩ dom 𝐻)) = ((◡𝐹 “ 𝑒) ∩ (◡𝐹 “ dom 𝐻))) |
| 63 | 62 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐵) → (◡𝐹 “ (𝑒 ∩ dom 𝐻)) = ((◡𝐹 “ 𝑒) ∩ (◡𝐹 “ dom 𝐻))) |
| 64 | 5 | dmexd 7925 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom 𝐹 ∈ V) |
| 65 | | restabs 23173 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ SAlg ∧ (◡𝐹 “ dom 𝐻) ⊆ dom 𝐹 ∧ dom 𝐹 ∈ V) → ((𝑆 ↾t dom 𝐹) ↾t (◡𝐹 “ dom 𝐻)) = (𝑆 ↾t (◡𝐹 “ dom 𝐻))) |
| 66 | 2, 4, 64, 65 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑆 ↾t dom 𝐹) ↾t (◡𝐹 “ dom 𝐻)) = (𝑆 ↾t (◡𝐹 “ dom 𝐻))) |
| 67 | 66 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑆 ↾t (◡𝐹 “ dom 𝐻)) = ((𝑆 ↾t dom 𝐹) ↾t (◡𝐹 “ dom 𝐻))) |
| 68 | 67 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐵) → (𝑆 ↾t (◡𝐹 “ dom 𝐻)) = ((𝑆 ↾t dom 𝐹) ↾t (◡𝐹 “ dom 𝐻))) |
| 69 | 60, 63, 68 | 3eltr4d 2856 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐵) → (◡𝐹 “ (𝑒 ∩ dom 𝐻)) ∈ (𝑆 ↾t (◡𝐹 “ dom 𝐻))) |
| 70 | 69 | 3adant3 1133 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐵 ∧ (◡𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻)) → (◡𝐹 “ (𝑒 ∩ dom 𝐻)) ∈ (𝑆 ↾t (◡𝐹 “ dom 𝐻))) |
| 71 | 47, 70 | eqeltrd 2841 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐵 ∧ (◡𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻)) → (◡𝐹 “ (◡𝐻 “ (-∞(,)𝑎))) ∈ (𝑆 ↾t (◡𝐹 “ dom 𝐻))) |
| 72 | 71 | 3exp 1120 |
. . . . . 6
⊢ (𝜑 → (𝑒 ∈ 𝐵 → ((◡𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻) → (◡𝐹 “ (◡𝐻 “ (-∞(,)𝑎))) ∈ (𝑆 ↾t (◡𝐹 “ dom 𝐻))))) |
| 73 | 72 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (𝑒 ∈ 𝐵 → ((◡𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻) → (◡𝐹 “ (◡𝐻 “ (-∞(,)𝑎))) ∈ (𝑆 ↾t (◡𝐹 “ dom 𝐻))))) |
| 74 | 73 | rexlimdv 3153 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (∃𝑒 ∈ 𝐵 (◡𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻) → (◡𝐹 “ (◡𝐻 “ (-∞(,)𝑎))) ∈ (𝑆 ↾t (◡𝐹 “ dom 𝐻)))) |
| 75 | 45, 74 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (◡𝐹 “ (◡𝐻 “ (-∞(,)𝑎))) ∈ (𝑆 ↾t (◡𝐹 “ dom 𝐻))) |
| 76 | 32, 75 | eqeltrd 2841 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ (◡𝐹 “ dom 𝐻) ∣ ((𝐻 ∘ 𝐹)‘𝑥) < 𝑎} ∈ (𝑆 ↾t (◡𝐹 “ dom 𝐻))) |
| 77 | 1, 2, 8, 23, 76 | issmfd 46750 |
1
⊢ (𝜑 → (𝐻 ∘ 𝐹) ∈ (SMblFn‘𝑆)) |