Step | Hyp | Ref
| Expression |
1 | | smfresal.t |
. . . 4
⊢ 𝑇 = {𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)} |
2 | | reex 9906 |
. . . . 5
⊢ ℝ
∈ V |
3 | 2 | pwex 4774 |
. . . 4
⊢ 𝒫
ℝ ∈ V |
4 | 1, 3 | rabex2 4742 |
. . 3
⊢ 𝑇 ∈ V |
5 | 4 | a1i 11 |
. 2
⊢ (𝜑 → 𝑇 ∈ V) |
6 | | 0elpw 4760 |
. . . . 5
⊢ ∅
∈ 𝒫 ℝ |
7 | 6 | a1i 11 |
. . . 4
⊢ (𝜑 → ∅ ∈ 𝒫
ℝ) |
8 | | ima0 5400 |
. . . . . 6
⊢ (◡𝐹 “ ∅) = ∅ |
9 | 8 | a1i 11 |
. . . . 5
⊢ (𝜑 → (◡𝐹 “ ∅) =
∅) |
10 | | smfresal.s |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ SAlg) |
11 | 10 | uniexd 38310 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝑆
∈ V) |
12 | | smfresal.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆)) |
13 | | smfresal.d |
. . . . . . . . 9
⊢ 𝐷 = dom 𝐹 |
14 | 10, 12, 13 | smfdmss 39619 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑆) |
15 | 11, 14 | ssexd 4733 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ V) |
16 | | eqid 2610 |
. . . . . . 7
⊢ (𝑆 ↾t 𝐷) = (𝑆 ↾t 𝐷) |
17 | 10, 15, 16 | subsalsal 39253 |
. . . . . 6
⊢ (𝜑 → (𝑆 ↾t 𝐷) ∈ SAlg) |
18 | 17 | 0sald 39244 |
. . . . 5
⊢ (𝜑 → ∅ ∈ (𝑆 ↾t 𝐷)) |
19 | 9, 18 | eqeltrd 2688 |
. . . 4
⊢ (𝜑 → (◡𝐹 “ ∅) ∈ (𝑆 ↾t 𝐷)) |
20 | 7, 19 | jca 553 |
. . 3
⊢ (𝜑 → (∅ ∈ 𝒫
ℝ ∧ (◡𝐹 “ ∅) ∈ (𝑆 ↾t 𝐷))) |
21 | | imaeq2 5381 |
. . . . 5
⊢ (𝑒 = ∅ → (◡𝐹 “ 𝑒) = (◡𝐹 “ ∅)) |
22 | 21 | eleq1d 2672 |
. . . 4
⊢ (𝑒 = ∅ → ((◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ ∅) ∈ (𝑆 ↾t 𝐷))) |
23 | 22, 1 | elrab2 3333 |
. . 3
⊢ (∅
∈ 𝑇 ↔ (∅
∈ 𝒫 ℝ ∧ (◡𝐹 “ ∅) ∈ (𝑆 ↾t 𝐷))) |
24 | 20, 23 | sylibr 223 |
. 2
⊢ (𝜑 → ∅ ∈ 𝑇) |
25 | | eqid 2610 |
. 2
⊢ ∪ 𝑇 =
∪ 𝑇 |
26 | | nfv 1830 |
. . . . . . 7
⊢
Ⅎ𝑦𝜑 |
27 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑒𝑦 |
28 | | nfrab1 3099 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑒{𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)} |
29 | 1, 28 | nfcxfr 2749 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑒𝑇 |
30 | 27, 29 | eluni2f 38315 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ∪ 𝑇
↔ ∃𝑒 ∈
𝑇 𝑦 ∈ 𝑒) |
31 | 30 | biimpi 205 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ∪ 𝑇
→ ∃𝑒 ∈
𝑇 𝑦 ∈ 𝑒) |
32 | 31 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ∪ 𝑇) → ∃𝑒 ∈ 𝑇 𝑦 ∈ 𝑒) |
33 | | nfv 1830 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑒𝜑 |
34 | 29 | nfuni 4378 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑒∪ 𝑇 |
35 | 27, 34 | nfel 2763 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑒 𝑦 ∈ ∪ 𝑇 |
36 | 33, 35 | nfan 1816 |
. . . . . . . . . . 11
⊢
Ⅎ𝑒(𝜑 ∧ 𝑦 ∈ ∪ 𝑇) |
37 | 27 | nfel1 2765 |
. . . . . . . . . . 11
⊢
Ⅎ𝑒 𝑦 ∈ ℝ |
38 | 1 | eleq2i 2680 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 ∈ 𝑇 ↔ 𝑒 ∈ {𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)}) |
39 | 38 | biimpi 205 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑒 ∈ 𝑇 → 𝑒 ∈ {𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)}) |
40 | | rabidim1 38318 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑒 ∈ {𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)} → 𝑒 ∈ 𝒫 ℝ) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 ∈ 𝑇 → 𝑒 ∈ 𝒫 ℝ) |
42 | | elpwi 4117 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 ∈ 𝒫 ℝ →
𝑒 ⊆
ℝ) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑒 ∈ 𝑇 → 𝑒 ⊆ ℝ) |
44 | 43 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑒 ∈ 𝑇 ∧ 𝑦 ∈ 𝑒) → 𝑒 ⊆ ℝ) |
45 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝑒 ∈ 𝑇 ∧ 𝑦 ∈ 𝑒) → 𝑦 ∈ 𝑒) |
46 | 44, 45 | sseldd 3569 |
. . . . . . . . . . . . 13
⊢ ((𝑒 ∈ 𝑇 ∧ 𝑦 ∈ 𝑒) → 𝑦 ∈ ℝ) |
47 | 46 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝑒 ∈ 𝑇 → (𝑦 ∈ 𝑒 → 𝑦 ∈ ℝ)) |
48 | 47 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ∪ 𝑇) → (𝑒 ∈ 𝑇 → (𝑦 ∈ 𝑒 → 𝑦 ∈ ℝ))) |
49 | 36, 37, 48 | rexlimd 3008 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ∪ 𝑇) → (∃𝑒 ∈ 𝑇 𝑦 ∈ 𝑒 → 𝑦 ∈ ℝ)) |
50 | 32, 49 | mpd 15 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ∪ 𝑇) → 𝑦 ∈ ℝ) |
51 | 50 | ex 449 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ ∪ 𝑇 → 𝑦 ∈ ℝ)) |
52 | | ovex 6577 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 − 1)(,)(𝑦 + 1)) ∈ V |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑦 − 1)(,)(𝑦 + 1)) ∈ V) |
54 | | ioossre 12106 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 − 1)(,)(𝑦 + 1)) ⊆
ℝ |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑦 − 1)(,)(𝑦 + 1)) ⊆ ℝ) |
56 | 53, 55 | elpwd 38264 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝒫
ℝ) |
57 | 56 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝒫
ℝ) |
58 | 10, 12, 13 | smff 39618 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹:𝐷⟶ℝ) |
59 | 58 | ffnd 5959 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹 Fn 𝐷) |
60 | | fncnvima2 6247 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 Fn 𝐷 → (◡𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) = {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) ∈ ((𝑦 − 1)(,)(𝑦 + 1))}) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (◡𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) = {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) ∈ ((𝑦 − 1)(,)(𝑦 + 1))}) |
62 | 61 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (◡𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) = {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) ∈ ((𝑦 − 1)(,)(𝑦 + 1))}) |
63 | | nfv 1830 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ ℝ) |
64 | 10 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑆 ∈ SAlg) |
65 | 15 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝐷 ∈ V) |
66 | 58 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐹:𝐷⟶ℝ) |
67 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝐷) |
68 | 66, 67 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝐹‘𝑥) ∈ ℝ) |
69 | 68 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐷) → (𝐹‘𝑥) ∈ ℝ) |
70 | 58 | feqmptd 6159 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ (𝐹‘𝑥))) |
71 | 70 | eqcomd 2616 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ (𝐹‘𝑥)) = 𝐹) |
72 | 71, 12 | eqeltrd 2688 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ (𝐹‘𝑥)) ∈ (SMblFn‘𝑆)) |
73 | 72 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑥 ∈ 𝐷 ↦ (𝐹‘𝑥)) ∈ (SMblFn‘𝑆)) |
74 | | peano2rem 10227 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℝ → (𝑦 − 1) ∈
ℝ) |
75 | 74 | rexrd 9968 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℝ → (𝑦 − 1) ∈
ℝ*) |
76 | 75 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 − 1) ∈
ℝ*) |
77 | | peano2re 10088 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℝ → (𝑦 + 1) ∈
ℝ) |
78 | 77 | rexrd 9968 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℝ → (𝑦 + 1) ∈
ℝ*) |
79 | 78 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + 1) ∈
ℝ*) |
80 | 63, 64, 65, 69, 73, 76, 79 | smfpimioompt 39671 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) ∈ ((𝑦 − 1)(,)(𝑦 + 1))} ∈ (𝑆 ↾t 𝐷)) |
81 | 62, 80 | eqeltrd 2688 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (◡𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) ∈ (𝑆 ↾t 𝐷)) |
82 | 57, 81 | jca 553 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝒫 ℝ ∧ (◡𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) ∈ (𝑆 ↾t 𝐷))) |
83 | | imaeq2 5381 |
. . . . . . . . . . . . . 14
⊢ (𝑒 = ((𝑦 − 1)(,)(𝑦 + 1)) → (◡𝐹 “ 𝑒) = (◡𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1)))) |
84 | 83 | eleq1d 2672 |
. . . . . . . . . . . . 13
⊢ (𝑒 = ((𝑦 − 1)(,)(𝑦 + 1)) → ((◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) ∈ (𝑆 ↾t 𝐷))) |
85 | 84, 1 | elrab2 3333 |
. . . . . . . . . . . 12
⊢ (((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝑇 ↔ (((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝒫 ℝ ∧ (◡𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) ∈ (𝑆 ↾t 𝐷))) |
86 | 82, 85 | sylibr 223 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝑇) |
87 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℝ) |
88 | | ltm1 10742 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ → (𝑦 − 1) < 𝑦) |
89 | | ltp1 10740 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ → 𝑦 < (𝑦 + 1)) |
90 | 75, 78, 87, 88, 89 | eliood 38567 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ → 𝑦 ∈ ((𝑦 − 1)(,)(𝑦 + 1))) |
91 | 90 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ((𝑦 − 1)(,)(𝑦 + 1))) |
92 | | nfv 1830 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑒 𝑦 ∈ ((𝑦 − 1)(,)(𝑦 + 1)) |
93 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑒((𝑦 − 1)(,)(𝑦 + 1)) |
94 | | eleq2 2677 |
. . . . . . . . . . . 12
⊢ (𝑒 = ((𝑦 − 1)(,)(𝑦 + 1)) → (𝑦 ∈ 𝑒 ↔ 𝑦 ∈ ((𝑦 − 1)(,)(𝑦 + 1)))) |
95 | 92, 93, 29, 94 | rspcef 38267 |
. . . . . . . . . . 11
⊢ ((((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝑇 ∧ 𝑦 ∈ ((𝑦 − 1)(,)(𝑦 + 1))) → ∃𝑒 ∈ 𝑇 𝑦 ∈ 𝑒) |
96 | 86, 91, 95 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ∃𝑒 ∈ 𝑇 𝑦 ∈ 𝑒) |
97 | 96, 30 | sylibr 223 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ∪ 𝑇) |
98 | 97 | ex 449 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ ℝ → 𝑦 ∈ ∪ 𝑇)) |
99 | 51, 98 | impbid 201 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ ∪ 𝑇 ↔ 𝑦 ∈ ℝ)) |
100 | 26, 99 | alrimi 2069 |
. . . . . 6
⊢ (𝜑 → ∀𝑦(𝑦 ∈ ∪ 𝑇 ↔ 𝑦 ∈ ℝ)) |
101 | | dfcleq 2604 |
. . . . . 6
⊢ (∪ 𝑇 =
ℝ ↔ ∀𝑦(𝑦 ∈ ∪ 𝑇 ↔ 𝑦 ∈ ℝ)) |
102 | 100, 101 | sylibr 223 |
. . . . 5
⊢ (𝜑 → ∪ 𝑇 =
ℝ) |
103 | 102 | difeq1d 3689 |
. . . 4
⊢ (𝜑 → (∪ 𝑇
∖ 𝑥) = (ℝ
∖ 𝑥)) |
104 | 103 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (∪ 𝑇 ∖ 𝑥) = (ℝ ∖ 𝑥)) |
105 | | difss 3699 |
. . . . . . 7
⊢ (ℝ
∖ 𝑥) ⊆
ℝ |
106 | 2, 105 | ssexi 4731 |
. . . . . . . 8
⊢ (ℝ
∖ 𝑥) ∈
V |
107 | | elpwg 4116 |
. . . . . . . 8
⊢ ((ℝ
∖ 𝑥) ∈ V →
((ℝ ∖ 𝑥) ∈
𝒫 ℝ ↔ (ℝ ∖ 𝑥) ⊆ ℝ)) |
108 | 106, 107 | ax-mp 5 |
. . . . . . 7
⊢ ((ℝ
∖ 𝑥) ∈ 𝒫
ℝ ↔ (ℝ ∖ 𝑥) ⊆ ℝ) |
109 | 105, 108 | mpbir 220 |
. . . . . 6
⊢ (ℝ
∖ 𝑥) ∈ 𝒫
ℝ |
110 | 109 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (ℝ ∖ 𝑥) ∈ 𝒫 ℝ) |
111 | 58 | ffund 5962 |
. . . . . . . . 9
⊢ (𝜑 → Fun 𝐹) |
112 | | difpreima 6251 |
. . . . . . . . 9
⊢ (Fun
𝐹 → (◡𝐹 “ (ℝ ∖ 𝑥)) = ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ 𝑥))) |
113 | 111, 112 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (◡𝐹 “ (ℝ ∖ 𝑥)) = ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ 𝑥))) |
114 | | fimacnv 6255 |
. . . . . . . . . . 11
⊢ (𝐹:𝐷⟶ℝ → (◡𝐹 “ ℝ) = 𝐷) |
115 | 58, 114 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (◡𝐹 “ ℝ) = 𝐷) |
116 | 10, 14 | restuni4 38336 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ (𝑆
↾t 𝐷) =
𝐷) |
117 | 115, 116 | eqtr4d 2647 |
. . . . . . . . 9
⊢ (𝜑 → (◡𝐹 “ ℝ) = ∪ (𝑆
↾t 𝐷)) |
118 | 117 | difeq1d 3689 |
. . . . . . . 8
⊢ (𝜑 → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ 𝑥)) = (∪ (𝑆 ↾t 𝐷) ∖ (◡𝐹 “ 𝑥))) |
119 | 113, 118 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → (◡𝐹 “ (ℝ ∖ 𝑥)) = (∪ (𝑆 ↾t 𝐷) ∖ (◡𝐹 “ 𝑥))) |
120 | 119 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (◡𝐹 “ (ℝ ∖ 𝑥)) = (∪ (𝑆 ↾t 𝐷) ∖ (◡𝐹 “ 𝑥))) |
121 | 17 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝑆 ↾t 𝐷) ∈ SAlg) |
122 | | imaeq2 5381 |
. . . . . . . . . . . 12
⊢ (𝑒 = 𝑥 → (◡𝐹 “ 𝑒) = (◡𝐹 “ 𝑥)) |
123 | 122 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑒 = 𝑥 → ((◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ 𝑥) ∈ (𝑆 ↾t 𝐷))) |
124 | 123, 1 | elrab2 3333 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑇 ↔ (𝑥 ∈ 𝒫 ℝ ∧ (◡𝐹 “ 𝑥) ∈ (𝑆 ↾t 𝐷))) |
125 | 124 | biimpi 205 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑇 → (𝑥 ∈ 𝒫 ℝ ∧ (◡𝐹 “ 𝑥) ∈ (𝑆 ↾t 𝐷))) |
126 | 125 | simprd 478 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑇 → (◡𝐹 “ 𝑥) ∈ (𝑆 ↾t 𝐷)) |
127 | 126 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (◡𝐹 “ 𝑥) ∈ (𝑆 ↾t 𝐷)) |
128 | 121, 127 | saldifcld 39241 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (∪
(𝑆 ↾t
𝐷) ∖ (◡𝐹 “ 𝑥)) ∈ (𝑆 ↾t 𝐷)) |
129 | 120, 128 | eqeltrd 2688 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ (𝑆 ↾t 𝐷)) |
130 | 110, 129 | jca 553 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → ((ℝ ∖ 𝑥) ∈ 𝒫 ℝ ∧
(◡𝐹 “ (ℝ ∖ 𝑥)) ∈ (𝑆 ↾t 𝐷))) |
131 | | imaeq2 5381 |
. . . . . 6
⊢ (𝑒 = (ℝ ∖ 𝑥) → (◡𝐹 “ 𝑒) = (◡𝐹 “ (ℝ ∖ 𝑥))) |
132 | 131 | eleq1d 2672 |
. . . . 5
⊢ (𝑒 = (ℝ ∖ 𝑥) → ((◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ (𝑆 ↾t 𝐷))) |
133 | 132, 1 | elrab2 3333 |
. . . 4
⊢ ((ℝ
∖ 𝑥) ∈ 𝑇 ↔ ((ℝ ∖ 𝑥) ∈ 𝒫 ℝ ∧
(◡𝐹 “ (ℝ ∖ 𝑥)) ∈ (𝑆 ↾t 𝐷))) |
134 | 130, 133 | sylibr 223 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (ℝ ∖ 𝑥) ∈ 𝑇) |
135 | 104, 134 | eqeltrd 2688 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (∪ 𝑇 ∖ 𝑥) ∈ 𝑇) |
136 | | nnex 10903 |
. . . . . . . 8
⊢ ℕ
∈ V |
137 | | fvex 6113 |
. . . . . . . 8
⊢ (𝑔‘𝑛) ∈ V |
138 | 136, 137 | iunex 7039 |
. . . . . . 7
⊢ ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) ∈ V |
139 | 138 | a1i 11 |
. . . . . 6
⊢ (𝑔:ℕ⟶𝑇 → ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) ∈ V) |
140 | | ffvelrn 6265 |
. . . . . . . 8
⊢ ((𝑔:ℕ⟶𝑇 ∧ 𝑛 ∈ ℕ) → (𝑔‘𝑛) ∈ 𝑇) |
141 | 1 | eleq2i 2680 |
. . . . . . . . . . 11
⊢ ((𝑔‘𝑛) ∈ 𝑇 ↔ (𝑔‘𝑛) ∈ {𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)}) |
142 | 141 | biimpi 205 |
. . . . . . . . . 10
⊢ ((𝑔‘𝑛) ∈ 𝑇 → (𝑔‘𝑛) ∈ {𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)}) |
143 | | elrabi 3328 |
. . . . . . . . . 10
⊢ ((𝑔‘𝑛) ∈ {𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)} → (𝑔‘𝑛) ∈ 𝒫 ℝ) |
144 | 142, 143 | syl 17 |
. . . . . . . . 9
⊢ ((𝑔‘𝑛) ∈ 𝑇 → (𝑔‘𝑛) ∈ 𝒫 ℝ) |
145 | | elpwi 4117 |
. . . . . . . . 9
⊢ ((𝑔‘𝑛) ∈ 𝒫 ℝ → (𝑔‘𝑛) ⊆ ℝ) |
146 | 144, 145 | syl 17 |
. . . . . . . 8
⊢ ((𝑔‘𝑛) ∈ 𝑇 → (𝑔‘𝑛) ⊆ ℝ) |
147 | 140, 146 | syl 17 |
. . . . . . 7
⊢ ((𝑔:ℕ⟶𝑇 ∧ 𝑛 ∈ ℕ) → (𝑔‘𝑛) ⊆ ℝ) |
148 | 147 | iunssd 38299 |
. . . . . 6
⊢ (𝑔:ℕ⟶𝑇 → ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) ⊆ ℝ) |
149 | 139, 148 | elpwd 38264 |
. . . . 5
⊢ (𝑔:ℕ⟶𝑇 → ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) ∈ 𝒫 ℝ) |
150 | 149 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑔:ℕ⟶𝑇) → ∪
𝑛 ∈ ℕ (𝑔‘𝑛) ∈ 𝒫 ℝ) |
151 | | imaiun 6407 |
. . . . . 6
⊢ (◡𝐹 “ ∪
𝑛 ∈ ℕ (𝑔‘𝑛)) = ∪
𝑛 ∈ ℕ (◡𝐹 “ (𝑔‘𝑛)) |
152 | 151 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔:ℕ⟶𝑇) → (◡𝐹 “ ∪
𝑛 ∈ ℕ (𝑔‘𝑛)) = ∪
𝑛 ∈ ℕ (◡𝐹 “ (𝑔‘𝑛))) |
153 | 17 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔:ℕ⟶𝑇) → (𝑆 ↾t 𝐷) ∈ SAlg) |
154 | | nnct 12642 |
. . . . . . 7
⊢ ℕ
≼ ω |
155 | 154 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔:ℕ⟶𝑇) → ℕ ≼
ω) |
156 | | imaeq2 5381 |
. . . . . . . . . . . 12
⊢ (𝑒 = (𝑔‘𝑛) → (◡𝐹 “ 𝑒) = (◡𝐹 “ (𝑔‘𝑛))) |
157 | 156 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑒 = (𝑔‘𝑛) → ((◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷))) |
158 | 157, 1 | elrab2 3333 |
. . . . . . . . . 10
⊢ ((𝑔‘𝑛) ∈ 𝑇 ↔ ((𝑔‘𝑛) ∈ 𝒫 ℝ ∧ (◡𝐹 “ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷))) |
159 | 158 | biimpi 205 |
. . . . . . . . 9
⊢ ((𝑔‘𝑛) ∈ 𝑇 → ((𝑔‘𝑛) ∈ 𝒫 ℝ ∧ (◡𝐹 “ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷))) |
160 | 159 | simprd 478 |
. . . . . . . 8
⊢ ((𝑔‘𝑛) ∈ 𝑇 → (◡𝐹 “ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷)) |
161 | 140, 160 | syl 17 |
. . . . . . 7
⊢ ((𝑔:ℕ⟶𝑇 ∧ 𝑛 ∈ ℕ) → (◡𝐹 “ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷)) |
162 | 161 | adantll 746 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔:ℕ⟶𝑇) ∧ 𝑛 ∈ ℕ) → (◡𝐹 “ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷)) |
163 | 153, 155,
162 | saliuncl 39218 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔:ℕ⟶𝑇) → ∪
𝑛 ∈ ℕ (◡𝐹 “ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷)) |
164 | 152, 163 | eqeltrd 2688 |
. . . 4
⊢ ((𝜑 ∧ 𝑔:ℕ⟶𝑇) → (◡𝐹 “ ∪
𝑛 ∈ ℕ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷)) |
165 | 150, 164 | jca 553 |
. . 3
⊢ ((𝜑 ∧ 𝑔:ℕ⟶𝑇) → (∪ 𝑛 ∈ ℕ (𝑔‘𝑛) ∈ 𝒫 ℝ ∧ (◡𝐹 “ ∪
𝑛 ∈ ℕ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷))) |
166 | | imaeq2 5381 |
. . . . 5
⊢ (𝑒 = ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) → (◡𝐹 “ 𝑒) = (◡𝐹 “ ∪
𝑛 ∈ ℕ (𝑔‘𝑛))) |
167 | 166 | eleq1d 2672 |
. . . 4
⊢ (𝑒 = ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) → ((◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ ∪
𝑛 ∈ ℕ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷))) |
168 | 167, 1 | elrab2 3333 |
. . 3
⊢ (∪ 𝑛 ∈ ℕ (𝑔‘𝑛) ∈ 𝑇 ↔ (∪
𝑛 ∈ ℕ (𝑔‘𝑛) ∈ 𝒫 ℝ ∧ (◡𝐹 “ ∪
𝑛 ∈ ℕ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷))) |
169 | 165, 168 | sylibr 223 |
. 2
⊢ ((𝜑 ∧ 𝑔:ℕ⟶𝑇) → ∪
𝑛 ∈ ℕ (𝑔‘𝑛) ∈ 𝑇) |
170 | 5, 24, 25, 135, 169 | issalnnd 39239 |
1
⊢ (𝜑 → 𝑇 ∈ SAlg) |