Step | Hyp | Ref
| Expression |
1 | | issmfge.s |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ SAlg) |
2 | 1 | adantr 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝑆 ∈ SAlg) |
3 | | simpr 489 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹 ∈ (SMblFn‘𝑆)) |
4 | | issmfge.d |
. . . . . 6
⊢ 𝐷 = dom 𝐹 |
5 | 2, 3, 4 | smfdmss 43718 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐷 ⊆ ∪ 𝑆) |
6 | 2, 3, 4 | smff 43717 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹:𝐷⟶ℝ) |
7 | | nfv 1916 |
. . . . . . . . 9
⊢
Ⅎ𝑦𝜑 |
8 | | nfv 1916 |
. . . . . . . . 9
⊢
Ⅎ𝑦 𝐹 ∈ (SMblFn‘𝑆) |
9 | 7, 8 | nfan 1901 |
. . . . . . . 8
⊢
Ⅎ𝑦(𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) |
10 | | nfv 1916 |
. . . . . . . 8
⊢
Ⅎ𝑦 𝑏 ∈ ℝ |
11 | 9, 10 | nfan 1901 |
. . . . . . 7
⊢
Ⅎ𝑦((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑏 ∈ ℝ) |
12 | | nfv 1916 |
. . . . . . 7
⊢
Ⅎ𝑐((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑏 ∈ ℝ) |
13 | 1 | uniexd 7459 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ 𝑆
∈ V) |
14 | 13 | adantr 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐷 ⊆ ∪ 𝑆) → ∪ 𝑆
∈ V) |
15 | | simpr 489 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐷 ⊆ ∪ 𝑆) → 𝐷 ⊆ ∪ 𝑆) |
16 | 14, 15 | ssexd 5187 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐷 ⊆ ∪ 𝑆) → 𝐷 ∈ V) |
17 | 5, 16 | syldan 595 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐷 ∈ V) |
18 | | eqid 2759 |
. . . . . . . . 9
⊢ (𝑆 ↾t 𝐷) = (𝑆 ↾t 𝐷) |
19 | 2, 17, 18 | subsalsal 43350 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (𝑆 ↾t 𝐷) ∈ SAlg) |
20 | 19 | adantr 485 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑏 ∈ ℝ) → (𝑆 ↾t 𝐷) ∈ SAlg) |
21 | 6 | ffvelrnda 6835 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑦 ∈ 𝐷) → (𝐹‘𝑦) ∈ ℝ) |
22 | 21 | rexrd 10714 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑦 ∈ 𝐷) → (𝐹‘𝑦) ∈
ℝ*) |
23 | 22 | adantlr 715 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑏 ∈ ℝ) ∧ 𝑦 ∈ 𝐷) → (𝐹‘𝑦) ∈
ℝ*) |
24 | 2 | adantr 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑐 ∈ ℝ) → 𝑆 ∈ SAlg) |
25 | 3 | adantr 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑐 ∈ ℝ) → 𝐹 ∈ (SMblFn‘𝑆)) |
26 | | simpr 489 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑐 ∈ ℝ) → 𝑐 ∈ ℝ) |
27 | 24, 25, 4, 26 | smfpreimagt 43746 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑐 ∈ ℝ) → {𝑦 ∈ 𝐷 ∣ 𝑐 < (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷)) |
28 | 27 | adantlr 715 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑏 ∈ ℝ) ∧ 𝑐 ∈ ℝ) → {𝑦 ∈ 𝐷 ∣ 𝑐 < (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷)) |
29 | | simpr 489 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑏 ∈ ℝ) → 𝑏 ∈ ℝ) |
30 | 11, 12, 20, 23, 28, 29 | salpreimagtge 43710 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑏 ∈ ℝ) → {𝑦 ∈ 𝐷 ∣ 𝑏 ≤ (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷)) |
31 | 30 | ralrimiva 3111 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 ≤ (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷)) |
32 | 5, 6, 31 | 3jca 1126 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 ≤ (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷))) |
33 | 32 | ex 417 |
. . 3
⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) → (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 ≤ (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷)))) |
34 | | nfv 1916 |
. . . . . . 7
⊢
Ⅎ𝑦 𝐷 ⊆ ∪ 𝑆 |
35 | | nfv 1916 |
. . . . . . 7
⊢
Ⅎ𝑦 𝐹:𝐷⟶ℝ |
36 | | nfcv 2917 |
. . . . . . . 8
⊢
Ⅎ𝑦ℝ |
37 | | nfrab1 3300 |
. . . . . . . . 9
⊢
Ⅎ𝑦{𝑦 ∈ 𝐷 ∣ 𝑏 ≤ (𝐹‘𝑦)} |
38 | | nfcv 2917 |
. . . . . . . . 9
⊢
Ⅎ𝑦(𝑆 ↾t 𝐷) |
39 | 37, 38 | nfel 2931 |
. . . . . . . 8
⊢
Ⅎ𝑦{𝑦 ∈ 𝐷 ∣ 𝑏 ≤ (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷) |
40 | 36, 39 | nfralw 3151 |
. . . . . . 7
⊢
Ⅎ𝑦∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 ≤ (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷) |
41 | 34, 35, 40 | nf3an 1903 |
. . . . . 6
⊢
Ⅎ𝑦(𝐷 ⊆ ∪ 𝑆
∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 ≤ (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷)) |
42 | 7, 41 | nfan 1901 |
. . . . 5
⊢
Ⅎ𝑦(𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 ≤ (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷))) |
43 | | nfv 1916 |
. . . . . 6
⊢
Ⅎ𝑏𝜑 |
44 | | nfv 1916 |
. . . . . . 7
⊢
Ⅎ𝑏 𝐷 ⊆ ∪ 𝑆 |
45 | | nfv 1916 |
. . . . . . 7
⊢
Ⅎ𝑏 𝐹:𝐷⟶ℝ |
46 | | nfra1 3145 |
. . . . . . 7
⊢
Ⅎ𝑏∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 ≤ (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷) |
47 | 44, 45, 46 | nf3an 1903 |
. . . . . 6
⊢
Ⅎ𝑏(𝐷 ⊆ ∪ 𝑆
∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 ≤ (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷)) |
48 | 43, 47 | nfan 1901 |
. . . . 5
⊢
Ⅎ𝑏(𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 ≤ (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷))) |
49 | 1 | adantr 485 |
. . . . 5
⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 ≤ (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷))) → 𝑆 ∈ SAlg) |
50 | | simpr1 1192 |
. . . . 5
⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 ≤ (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷))) → 𝐷 ⊆ ∪ 𝑆) |
51 | | simpr2 1193 |
. . . . 5
⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 ≤ (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷))) → 𝐹:𝐷⟶ℝ) |
52 | | simpr3 1194 |
. . . . 5
⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 ≤ (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷))) → ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 ≤ (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷)) |
53 | 42, 48, 49, 4, 50, 51, 52 | issmfgelem 43753 |
. . . 4
⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 ≤ (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷))) → 𝐹 ∈ (SMblFn‘𝑆)) |
54 | 53 | ex 417 |
. . 3
⊢ (𝜑 → ((𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 ≤ (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷)) → 𝐹 ∈ (SMblFn‘𝑆))) |
55 | 33, 54 | impbid 215 |
. 2
⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) ↔ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 ≤ (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷)))) |
56 | | breq1 5028 |
. . . . . . . 8
⊢ (𝑏 = 𝑎 → (𝑏 ≤ (𝐹‘𝑦) ↔ 𝑎 ≤ (𝐹‘𝑦))) |
57 | 56 | rabbidv 3390 |
. . . . . . 7
⊢ (𝑏 = 𝑎 → {𝑦 ∈ 𝐷 ∣ 𝑏 ≤ (𝐹‘𝑦)} = {𝑦 ∈ 𝐷 ∣ 𝑎 ≤ (𝐹‘𝑦)}) |
58 | | fveq2 6651 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥)) |
59 | 58 | breq2d 5037 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → (𝑎 ≤ (𝐹‘𝑦) ↔ 𝑎 ≤ (𝐹‘𝑥))) |
60 | 59 | cbvrabv 3402 |
. . . . . . . 8
⊢ {𝑦 ∈ 𝐷 ∣ 𝑎 ≤ (𝐹‘𝑦)} = {𝑥 ∈ 𝐷 ∣ 𝑎 ≤ (𝐹‘𝑥)} |
61 | 60 | a1i 11 |
. . . . . . 7
⊢ (𝑏 = 𝑎 → {𝑦 ∈ 𝐷 ∣ 𝑎 ≤ (𝐹‘𝑦)} = {𝑥 ∈ 𝐷 ∣ 𝑎 ≤ (𝐹‘𝑥)}) |
62 | 57, 61 | eqtrd 2794 |
. . . . . 6
⊢ (𝑏 = 𝑎 → {𝑦 ∈ 𝐷 ∣ 𝑏 ≤ (𝐹‘𝑦)} = {𝑥 ∈ 𝐷 ∣ 𝑎 ≤ (𝐹‘𝑥)}) |
63 | 62 | eleq1d 2835 |
. . . . 5
⊢ (𝑏 = 𝑎 → ({𝑦 ∈ 𝐷 ∣ 𝑏 ≤ (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷) ↔ {𝑥 ∈ 𝐷 ∣ 𝑎 ≤ (𝐹‘𝑥)} ∈ (𝑆 ↾t 𝐷))) |
64 | 63 | cbvralvw 3359 |
. . . 4
⊢
(∀𝑏 ∈
ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 ≤ (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷) ↔ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ 𝑎 ≤ (𝐹‘𝑥)} ∈ (𝑆 ↾t 𝐷)) |
65 | 64 | 3anbi3i 1157 |
. . 3
⊢ ((𝐷 ⊆ ∪ 𝑆
∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 ≤ (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷)) ↔ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ 𝑎 ≤ (𝐹‘𝑥)} ∈ (𝑆 ↾t 𝐷))) |
66 | 65 | a1i 11 |
. 2
⊢ (𝜑 → ((𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 ≤ (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷)) ↔ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ 𝑎 ≤ (𝐹‘𝑥)} ∈ (𝑆 ↾t 𝐷)))) |
67 | 55, 66 | bitrd 282 |
1
⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) ↔ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ 𝑎 ≤ (𝐹‘𝑥)} ∈ (𝑆 ↾t 𝐷)))) |