Step | Hyp | Ref
| Expression |
1 | | nfv 2015 |
. 2
⊢
Ⅎ𝑎𝜑 |
2 | | smfco.s |
. 2
⊢ (𝜑 → 𝑆 ∈ SAlg) |
3 | | cnvimass 5727 |
. . . 4
⊢ (◡𝐹 “ dom 𝐻) ⊆ dom 𝐹 |
4 | 3 | a1i 11 |
. . 3
⊢ (𝜑 → (◡𝐹 “ dom 𝐻) ⊆ dom 𝐹) |
5 | | smfco.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆)) |
6 | | eqid 2826 |
. . . 4
⊢ dom 𝐹 = dom 𝐹 |
7 | 2, 5, 6 | smfdmss 41737 |
. . 3
⊢ (𝜑 → dom 𝐹 ⊆ ∪ 𝑆) |
8 | 4, 7 | sstrd 3838 |
. 2
⊢ (𝜑 → (◡𝐹 “ dom 𝐻) ⊆ ∪ 𝑆) |
9 | | smfco.j |
. . . . . . . . 9
⊢ 𝐽 = (topGen‘ran
(,)) |
10 | | retop 22936 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) ∈ Top |
11 | 9, 10 | eqeltri 2903 |
. . . . . . . 8
⊢ 𝐽 ∈ Top |
12 | 11 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ Top) |
13 | | smfco.b |
. . . . . . 7
⊢ 𝐵 = (SalGen‘𝐽) |
14 | 12, 13 | salgencld 41359 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ SAlg) |
15 | | smfco.h |
. . . . . 6
⊢ (𝜑 → 𝐻 ∈ (SMblFn‘𝐵)) |
16 | | eqid 2826 |
. . . . . 6
⊢ dom 𝐻 = dom 𝐻 |
17 | 14, 15, 16 | smff 41736 |
. . . . 5
⊢ (𝜑 → 𝐻:dom 𝐻⟶ℝ) |
18 | 17 | ffund 6283 |
. . . 4
⊢ (𝜑 → Fun 𝐻) |
19 | 2, 5, 6 | smff 41736 |
. . . . 5
⊢ (𝜑 → 𝐹:dom 𝐹⟶ℝ) |
20 | 19 | ffund 6283 |
. . . 4
⊢ (𝜑 → Fun 𝐹) |
21 | 18, 20 | fco3 40227 |
. . 3
⊢ (𝜑 → (𝐻 ∘ 𝐹):(◡𝐹 “ dom 𝐻)⟶ran 𝐻) |
22 | 17 | frnd 6286 |
. . 3
⊢ (𝜑 → ran 𝐻 ⊆ ℝ) |
23 | 21, 22 | fssd 6293 |
. 2
⊢ (𝜑 → (𝐻 ∘ 𝐹):(◡𝐹 “ dom 𝐻)⟶ℝ) |
24 | 23 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (𝐻 ∘ 𝐹):(◡𝐹 “ dom 𝐻)⟶ℝ) |
25 | | rexr 10403 |
. . . . . . 7
⊢ (𝑎 ∈ ℝ → 𝑎 ∈
ℝ*) |
26 | 25 | adantl 475 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ*) |
27 | 24, 26 | preimaioomnf 41724 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (◡(𝐻 ∘ 𝐹) “ (-∞(,)𝑎)) = {𝑥 ∈ (◡𝐹 “ dom 𝐻) ∣ ((𝐻 ∘ 𝐹)‘𝑥) < 𝑎}) |
28 | 27 | eqcomd 2832 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ (◡𝐹 “ dom 𝐻) ∣ ((𝐻 ∘ 𝐹)‘𝑥) < 𝑎} = (◡(𝐻 ∘ 𝐹) “ (-∞(,)𝑎))) |
29 | | cnvco 5541 |
. . . . . 6
⊢ ◡(𝐻 ∘ 𝐹) = (◡𝐹 ∘ ◡𝐻) |
30 | 29 | imaeq1i 5705 |
. . . . 5
⊢ (◡(𝐻 ∘ 𝐹) “ (-∞(,)𝑎)) = ((◡𝐹 ∘ ◡𝐻) “ (-∞(,)𝑎)) |
31 | 30 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (◡(𝐻 ∘ 𝐹) “ (-∞(,)𝑎)) = ((◡𝐹 ∘ ◡𝐻) “ (-∞(,)𝑎))) |
32 | | imaco 5882 |
. . . . 5
⊢ ((◡𝐹 ∘ ◡𝐻) “ (-∞(,)𝑎)) = (◡𝐹 “ (◡𝐻 “ (-∞(,)𝑎))) |
33 | 32 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → ((◡𝐹 ∘ ◡𝐻) “ (-∞(,)𝑎)) = (◡𝐹 “ (◡𝐻 “ (-∞(,)𝑎)))) |
34 | 28, 31, 33 | 3eqtrd 2866 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ (◡𝐹 “ dom 𝐻) ∣ ((𝐻 ∘ 𝐹)‘𝑥) < 𝑎} = (◡𝐹 “ (◡𝐻 “ (-∞(,)𝑎)))) |
35 | 17 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝐻:dom 𝐻⟶ℝ) |
36 | 35, 26 | preimaioomnf 41724 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (◡𝐻 “ (-∞(,)𝑎)) = {𝑥 ∈ dom 𝐻 ∣ (𝐻‘𝑥) < 𝑎}) |
37 | 36 | eqcomd 2832 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ dom 𝐻 ∣ (𝐻‘𝑥) < 𝑎} = (◡𝐻 “ (-∞(,)𝑎))) |
38 | 37 | eqcomd 2832 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (◡𝐻 “ (-∞(,)𝑎)) = {𝑥 ∈ dom 𝐻 ∣ (𝐻‘𝑥) < 𝑎}) |
39 | 14 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝐵 ∈ SAlg) |
40 | 15 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝐻 ∈ (SMblFn‘𝐵)) |
41 | | simpr 479 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ) |
42 | 39, 40, 16, 41 | smfpreimalt 41735 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ dom 𝐻 ∣ (𝐻‘𝑥) < 𝑎} ∈ (𝐵 ↾t dom 𝐻)) |
43 | 38, 42 | eqeltrd 2907 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (◡𝐻 “ (-∞(,)𝑎)) ∈ (𝐵 ↾t dom 𝐻)) |
44 | 14 | elexd 3432 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ V) |
45 | 15 | dmexd 7361 |
. . . . . . 7
⊢ (𝜑 → dom 𝐻 ∈ V) |
46 | | elrest 16442 |
. . . . . . 7
⊢ ((𝐵 ∈ V ∧ dom 𝐻 ∈ V) → ((◡𝐻 “ (-∞(,)𝑎)) ∈ (𝐵 ↾t dom 𝐻) ↔ ∃𝑒 ∈ 𝐵 (◡𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻))) |
47 | 44, 45, 46 | syl2anc 581 |
. . . . . 6
⊢ (𝜑 → ((◡𝐻 “ (-∞(,)𝑎)) ∈ (𝐵 ↾t dom 𝐻) ↔ ∃𝑒 ∈ 𝐵 (◡𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻))) |
48 | 47 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → ((◡𝐻 “ (-∞(,)𝑎)) ∈ (𝐵 ↾t dom 𝐻) ↔ ∃𝑒 ∈ 𝐵 (◡𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻))) |
49 | 43, 48 | mpbid 224 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → ∃𝑒 ∈ 𝐵 (◡𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻)) |
50 | | imaeq2 5704 |
. . . . . . . . 9
⊢ ((◡𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻) → (◡𝐹 “ (◡𝐻 “ (-∞(,)𝑎))) = (◡𝐹 “ (𝑒 ∩ dom 𝐻))) |
51 | 50 | 3ad2ant3 1171 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐵 ∧ (◡𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻)) → (◡𝐹 “ (◡𝐻 “ (-∞(,)𝑎))) = (◡𝐹 “ (𝑒 ∩ dom 𝐻))) |
52 | | ovexd 6940 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐵) → (𝑆 ↾t dom 𝐹) ∈ V) |
53 | 5 | elexd 3432 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹 ∈ V) |
54 | | cnvexg 7375 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ V → ◡𝐹 ∈ V) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ◡𝐹 ∈ V) |
56 | | imaexg 7366 |
. . . . . . . . . . . . 13
⊢ (◡𝐹 ∈ V → (◡𝐹 “ dom 𝐻) ∈ V) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡𝐹 “ dom 𝐻) ∈ V) |
58 | 57 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐵) → (◡𝐹 “ dom 𝐻) ∈ V) |
59 | 2 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐵) → 𝑆 ∈ SAlg) |
60 | 5 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐵) → 𝐹 ∈ (SMblFn‘𝑆)) |
61 | | simpr 479 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐵) → 𝑒 ∈ 𝐵) |
62 | | eqid 2826 |
. . . . . . . . . . . 12
⊢ (◡𝐹 “ 𝑒) = (◡𝐹 “ 𝑒) |
63 | 59, 60, 6, 9, 13, 61, 62 | smfpimbor1 41802 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐵) → (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t dom 𝐹)) |
64 | | eqid 2826 |
. . . . . . . . . . 11
⊢ ((◡𝐹 “ 𝑒) ∩ (◡𝐹 “ dom 𝐻)) = ((◡𝐹 “ 𝑒) ∩ (◡𝐹 “ dom 𝐻)) |
65 | 52, 58, 63, 64 | elrestd 40107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐵) → ((◡𝐹 “ 𝑒) ∩ (◡𝐹 “ dom 𝐻)) ∈ ((𝑆 ↾t dom 𝐹) ↾t (◡𝐹 “ dom 𝐻))) |
66 | | inpreima 6592 |
. . . . . . . . . . . . 13
⊢ (Fun
𝐹 → (◡𝐹 “ (𝑒 ∩ dom 𝐻)) = ((◡𝐹 “ 𝑒) ∩ (◡𝐹 “ dom 𝐻))) |
67 | 20, 66 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡𝐹 “ (𝑒 ∩ dom 𝐻)) = ((◡𝐹 “ 𝑒) ∩ (◡𝐹 “ dom 𝐻))) |
68 | 67 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐵) → (◡𝐹 “ (𝑒 ∩ dom 𝐻)) = ((◡𝐹 “ 𝑒) ∩ (◡𝐹 “ dom 𝐻))) |
69 | 5 | dmexd 7361 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom 𝐹 ∈ V) |
70 | | restabs 21341 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ SAlg ∧ (◡𝐹 “ dom 𝐻) ⊆ dom 𝐹 ∧ dom 𝐹 ∈ V) → ((𝑆 ↾t dom 𝐹) ↾t (◡𝐹 “ dom 𝐻)) = (𝑆 ↾t (◡𝐹 “ dom 𝐻))) |
71 | 2, 4, 69, 70 | syl3anc 1496 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑆 ↾t dom 𝐹) ↾t (◡𝐹 “ dom 𝐻)) = (𝑆 ↾t (◡𝐹 “ dom 𝐻))) |
72 | 71 | eqcomd 2832 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 ↾t (◡𝐹 “ dom 𝐻)) = ((𝑆 ↾t dom 𝐹) ↾t (◡𝐹 “ dom 𝐻))) |
73 | 72 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐵) → (𝑆 ↾t (◡𝐹 “ dom 𝐻)) = ((𝑆 ↾t dom 𝐹) ↾t (◡𝐹 “ dom 𝐻))) |
74 | 68, 73 | eleq12d 2901 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐵) → ((◡𝐹 “ (𝑒 ∩ dom 𝐻)) ∈ (𝑆 ↾t (◡𝐹 “ dom 𝐻)) ↔ ((◡𝐹 “ 𝑒) ∩ (◡𝐹 “ dom 𝐻)) ∈ ((𝑆 ↾t dom 𝐹) ↾t (◡𝐹 “ dom 𝐻)))) |
75 | 65, 74 | mpbird 249 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐵) → (◡𝐹 “ (𝑒 ∩ dom 𝐻)) ∈ (𝑆 ↾t (◡𝐹 “ dom 𝐻))) |
76 | 75 | 3adant3 1168 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐵 ∧ (◡𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻)) → (◡𝐹 “ (𝑒 ∩ dom 𝐻)) ∈ (𝑆 ↾t (◡𝐹 “ dom 𝐻))) |
77 | 51, 76 | eqeltrd 2907 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐵 ∧ (◡𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻)) → (◡𝐹 “ (◡𝐻 “ (-∞(,)𝑎))) ∈ (𝑆 ↾t (◡𝐹 “ dom 𝐻))) |
78 | 77 | 3exp 1154 |
. . . . . 6
⊢ (𝜑 → (𝑒 ∈ 𝐵 → ((◡𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻) → (◡𝐹 “ (◡𝐻 “ (-∞(,)𝑎))) ∈ (𝑆 ↾t (◡𝐹 “ dom 𝐻))))) |
79 | 78 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (𝑒 ∈ 𝐵 → ((◡𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻) → (◡𝐹 “ (◡𝐻 “ (-∞(,)𝑎))) ∈ (𝑆 ↾t (◡𝐹 “ dom 𝐻))))) |
80 | 79 | rexlimdv 3240 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (∃𝑒 ∈ 𝐵 (◡𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻) → (◡𝐹 “ (◡𝐻 “ (-∞(,)𝑎))) ∈ (𝑆 ↾t (◡𝐹 “ dom 𝐻)))) |
81 | 49, 80 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (◡𝐹 “ (◡𝐻 “ (-∞(,)𝑎))) ∈ (𝑆 ↾t (◡𝐹 “ dom 𝐻))) |
82 | 34, 81 | eqeltrd 2907 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ (◡𝐹 “ dom 𝐻) ∣ ((𝐻 ∘ 𝐹)‘𝑥) < 𝑎} ∈ (𝑆 ↾t (◡𝐹 “ dom 𝐻))) |
83 | 1, 2, 8, 23, 82 | issmfd 41739 |
1
⊢ (𝜑 → (𝐻 ∘ 𝐹) ∈ (SMblFn‘𝑆)) |