| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | smfresal.t | . . . 4
⊢ 𝑇 = {𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)} | 
| 2 |  | reex 11247 | . . . . 5
⊢ ℝ
∈ V | 
| 3 | 2 | pwex 5379 | . . . 4
⊢ 𝒫
ℝ ∈ V | 
| 4 | 1, 3 | rabex2 5340 | . . 3
⊢ 𝑇 ∈ V | 
| 5 | 4 | a1i 11 | . 2
⊢ (𝜑 → 𝑇 ∈ V) | 
| 6 |  | 0elpw 5355 | . . . . 5
⊢ ∅
∈ 𝒫 ℝ | 
| 7 | 6 | a1i 11 | . . . 4
⊢ (𝜑 → ∅ ∈ 𝒫
ℝ) | 
| 8 |  | ima0 6094 | . . . . . 6
⊢ (◡𝐹 “ ∅) = ∅ | 
| 9 | 8 | a1i 11 | . . . . 5
⊢ (𝜑 → (◡𝐹 “ ∅) =
∅) | 
| 10 |  | smfresal.s | . . . . . . 7
⊢ (𝜑 → 𝑆 ∈ SAlg) | 
| 11 | 10 | uniexd 7763 | . . . . . . . 8
⊢ (𝜑 → ∪ 𝑆
∈ V) | 
| 12 |  | smfresal.f | . . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆)) | 
| 13 |  | smfresal.d | . . . . . . . . 9
⊢ 𝐷 = dom 𝐹 | 
| 14 | 10, 12, 13 | smfdmss 46753 | . . . . . . . 8
⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑆) | 
| 15 | 11, 14 | ssexd 5323 | . . . . . . 7
⊢ (𝜑 → 𝐷 ∈ V) | 
| 16 |  | eqid 2736 | . . . . . . 7
⊢ (𝑆 ↾t 𝐷) = (𝑆 ↾t 𝐷) | 
| 17 | 10, 15, 16 | subsalsal 46379 | . . . . . 6
⊢ (𝜑 → (𝑆 ↾t 𝐷) ∈ SAlg) | 
| 18 | 17 | 0sald 46370 | . . . . 5
⊢ (𝜑 → ∅ ∈ (𝑆 ↾t 𝐷)) | 
| 19 | 9, 18 | eqeltrd 2840 | . . . 4
⊢ (𝜑 → (◡𝐹 “ ∅) ∈ (𝑆 ↾t 𝐷)) | 
| 20 | 7, 19 | jca 511 | . . 3
⊢ (𝜑 → (∅ ∈ 𝒫
ℝ ∧ (◡𝐹 “ ∅) ∈ (𝑆 ↾t 𝐷))) | 
| 21 |  | imaeq2 6073 | . . . . 5
⊢ (𝑒 = ∅ → (◡𝐹 “ 𝑒) = (◡𝐹 “ ∅)) | 
| 22 | 21 | eleq1d 2825 | . . . 4
⊢ (𝑒 = ∅ → ((◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ ∅) ∈ (𝑆 ↾t 𝐷))) | 
| 23 | 22, 1 | elrab2 3694 | . . 3
⊢ (∅
∈ 𝑇 ↔ (∅
∈ 𝒫 ℝ ∧ (◡𝐹 “ ∅) ∈ (𝑆 ↾t 𝐷))) | 
| 24 | 20, 23 | sylibr 234 | . 2
⊢ (𝜑 → ∅ ∈ 𝑇) | 
| 25 |  | eqid 2736 | . 2
⊢ ∪ 𝑇 =
∪ 𝑇 | 
| 26 |  | nfv 1913 | . . . . . . 7
⊢
Ⅎ𝑦𝜑 | 
| 27 |  | nfcv 2904 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑒𝑦 | 
| 28 |  | nfrab1 3456 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑒{𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)} | 
| 29 | 1, 28 | nfcxfr 2902 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑒𝑇 | 
| 30 | 27, 29 | eluni2f 45113 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ ∪ 𝑇
↔ ∃𝑒 ∈
𝑇 𝑦 ∈ 𝑒) | 
| 31 | 30 | biimpi 216 | . . . . . . . . . . 11
⊢ (𝑦 ∈ ∪ 𝑇
→ ∃𝑒 ∈
𝑇 𝑦 ∈ 𝑒) | 
| 32 | 31 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ∪ 𝑇) → ∃𝑒 ∈ 𝑇 𝑦 ∈ 𝑒) | 
| 33 |  | nfv 1913 | . . . . . . . . . . . 12
⊢
Ⅎ𝑒𝜑 | 
| 34 | 29 | nfuni 4913 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑒∪ 𝑇 | 
| 35 | 27, 34 | nfel 2919 | . . . . . . . . . . . 12
⊢
Ⅎ𝑒 𝑦 ∈ ∪ 𝑇 | 
| 36 | 33, 35 | nfan 1898 | . . . . . . . . . . 11
⊢
Ⅎ𝑒(𝜑 ∧ 𝑦 ∈ ∪ 𝑇) | 
| 37 | 27 | nfel1 2921 | . . . . . . . . . . 11
⊢
Ⅎ𝑒 𝑦 ∈ ℝ | 
| 38 | 1 | eleq2i 2832 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑒 ∈ 𝑇 ↔ 𝑒 ∈ {𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)}) | 
| 39 | 38 | biimpi 216 | . . . . . . . . . . . . . . . . 17
⊢ (𝑒 ∈ 𝑇 → 𝑒 ∈ {𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)}) | 
| 40 |  | rabidim1 3458 | . . . . . . . . . . . . . . . . 17
⊢ (𝑒 ∈ {𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)} → 𝑒 ∈ 𝒫 ℝ) | 
| 41 | 39, 40 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝑒 ∈ 𝑇 → 𝑒 ∈ 𝒫 ℝ) | 
| 42 |  | elpwi 4606 | . . . . . . . . . . . . . . . 16
⊢ (𝑒 ∈ 𝒫 ℝ →
𝑒 ⊆
ℝ) | 
| 43 | 41, 42 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝑒 ∈ 𝑇 → 𝑒 ⊆ ℝ) | 
| 44 | 43 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝑒 ∈ 𝑇 ∧ 𝑦 ∈ 𝑒) → 𝑒 ⊆ ℝ) | 
| 45 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ ((𝑒 ∈ 𝑇 ∧ 𝑦 ∈ 𝑒) → 𝑦 ∈ 𝑒) | 
| 46 | 44, 45 | sseldd 3983 | . . . . . . . . . . . . 13
⊢ ((𝑒 ∈ 𝑇 ∧ 𝑦 ∈ 𝑒) → 𝑦 ∈ ℝ) | 
| 47 | 46 | ex 412 | . . . . . . . . . . . 12
⊢ (𝑒 ∈ 𝑇 → (𝑦 ∈ 𝑒 → 𝑦 ∈ ℝ)) | 
| 48 | 47 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ∪ 𝑇) → (𝑒 ∈ 𝑇 → (𝑦 ∈ 𝑒 → 𝑦 ∈ ℝ))) | 
| 49 | 36, 37, 48 | rexlimd 3265 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ∪ 𝑇) → (∃𝑒 ∈ 𝑇 𝑦 ∈ 𝑒 → 𝑦 ∈ ℝ)) | 
| 50 | 32, 49 | mpd 15 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ∪ 𝑇) → 𝑦 ∈ ℝ) | 
| 51 | 50 | ex 412 | . . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ ∪ 𝑇 → 𝑦 ∈ ℝ)) | 
| 52 |  | ovexd 7467 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑦 − 1)(,)(𝑦 + 1)) ∈ V) | 
| 53 |  | ioossre 13449 | . . . . . . . . . . . . . . . 16
⊢ ((𝑦 − 1)(,)(𝑦 + 1)) ⊆
ℝ | 
| 54 | 53 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑦 − 1)(,)(𝑦 + 1)) ⊆ ℝ) | 
| 55 | 52, 54 | elpwd 4605 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝒫
ℝ) | 
| 56 | 55 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝒫
ℝ) | 
| 57 | 10, 12, 13 | smff 46752 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹:𝐷⟶ℝ) | 
| 58 | 57 | ffnd 6736 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹 Fn 𝐷) | 
| 59 |  | fncnvima2 7080 | . . . . . . . . . . . . . . . 16
⊢ (𝐹 Fn 𝐷 → (◡𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) = {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) ∈ ((𝑦 − 1)(,)(𝑦 + 1))}) | 
| 60 | 58, 59 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (◡𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) = {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) ∈ ((𝑦 − 1)(,)(𝑦 + 1))}) | 
| 61 | 60 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (◡𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) = {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) ∈ ((𝑦 − 1)(,)(𝑦 + 1))}) | 
| 62 |  | nfv 1913 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ ℝ) | 
| 63 | 10 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑆 ∈ SAlg) | 
| 64 | 15 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝐷 ∈ V) | 
| 65 | 57 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐹:𝐷⟶ℝ) | 
| 66 |  | simpr 484 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝐷) | 
| 67 | 65, 66 | ffvelcdmd 7104 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝐹‘𝑥) ∈ ℝ) | 
| 68 | 67 | adantlr 715 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐷) → (𝐹‘𝑥) ∈ ℝ) | 
| 69 | 57 | feqmptd 6976 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ (𝐹‘𝑥))) | 
| 70 | 69 | eqcomd 2742 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ (𝐹‘𝑥)) = 𝐹) | 
| 71 | 70, 12 | eqeltrd 2840 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ (𝐹‘𝑥)) ∈ (SMblFn‘𝑆)) | 
| 72 | 71 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑥 ∈ 𝐷 ↦ (𝐹‘𝑥)) ∈ (SMblFn‘𝑆)) | 
| 73 |  | peano2rem 11577 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℝ → (𝑦 − 1) ∈
ℝ) | 
| 74 | 73 | rexrd 11312 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℝ → (𝑦 − 1) ∈
ℝ*) | 
| 75 | 74 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 − 1) ∈
ℝ*) | 
| 76 |  | peano2re 11435 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℝ → (𝑦 + 1) ∈
ℝ) | 
| 77 | 76 | rexrd 11312 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℝ → (𝑦 + 1) ∈
ℝ*) | 
| 78 | 77 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + 1) ∈
ℝ*) | 
| 79 | 62, 63, 64, 68, 72, 75, 78 | smfpimioompt 46806 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) ∈ ((𝑦 − 1)(,)(𝑦 + 1))} ∈ (𝑆 ↾t 𝐷)) | 
| 80 | 61, 79 | eqeltrd 2840 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (◡𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) ∈ (𝑆 ↾t 𝐷)) | 
| 81 | 56, 80 | jca 511 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝒫 ℝ ∧ (◡𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) ∈ (𝑆 ↾t 𝐷))) | 
| 82 |  | imaeq2 6073 | . . . . . . . . . . . . . 14
⊢ (𝑒 = ((𝑦 − 1)(,)(𝑦 + 1)) → (◡𝐹 “ 𝑒) = (◡𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1)))) | 
| 83 | 82 | eleq1d 2825 | . . . . . . . . . . . . 13
⊢ (𝑒 = ((𝑦 − 1)(,)(𝑦 + 1)) → ((◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) ∈ (𝑆 ↾t 𝐷))) | 
| 84 | 83, 1 | elrab2 3694 | . . . . . . . . . . . 12
⊢ (((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝑇 ↔ (((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝒫 ℝ ∧ (◡𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) ∈ (𝑆 ↾t 𝐷))) | 
| 85 | 81, 84 | sylibr 234 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝑇) | 
| 86 |  | id 22 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℝ) | 
| 87 |  | ltm1 12110 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ → (𝑦 − 1) < 𝑦) | 
| 88 |  | ltp1 12108 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ → 𝑦 < (𝑦 + 1)) | 
| 89 | 74, 77, 86, 87, 88 | eliood 45516 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ → 𝑦 ∈ ((𝑦 − 1)(,)(𝑦 + 1))) | 
| 90 | 89 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ((𝑦 − 1)(,)(𝑦 + 1))) | 
| 91 |  | nfv 1913 | . . . . . . . . . . . 12
⊢
Ⅎ𝑒 𝑦 ∈ ((𝑦 − 1)(,)(𝑦 + 1)) | 
| 92 |  | nfcv 2904 | . . . . . . . . . . . 12
⊢
Ⅎ𝑒((𝑦 − 1)(,)(𝑦 + 1)) | 
| 93 |  | eleq2 2829 | . . . . . . . . . . . 12
⊢ (𝑒 = ((𝑦 − 1)(,)(𝑦 + 1)) → (𝑦 ∈ 𝑒 ↔ 𝑦 ∈ ((𝑦 − 1)(,)(𝑦 + 1)))) | 
| 94 | 91, 92, 29, 93 | rspcef 45082 | . . . . . . . . . . 11
⊢ ((((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝑇 ∧ 𝑦 ∈ ((𝑦 − 1)(,)(𝑦 + 1))) → ∃𝑒 ∈ 𝑇 𝑦 ∈ 𝑒) | 
| 95 | 85, 90, 94 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ∃𝑒 ∈ 𝑇 𝑦 ∈ 𝑒) | 
| 96 | 95, 30 | sylibr 234 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ∪ 𝑇) | 
| 97 | 96 | ex 412 | . . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ ℝ → 𝑦 ∈ ∪ 𝑇)) | 
| 98 | 51, 97 | impbid 212 | . . . . . . 7
⊢ (𝜑 → (𝑦 ∈ ∪ 𝑇 ↔ 𝑦 ∈ ℝ)) | 
| 99 | 26, 98 | alrimi 2212 | . . . . . 6
⊢ (𝜑 → ∀𝑦(𝑦 ∈ ∪ 𝑇 ↔ 𝑦 ∈ ℝ)) | 
| 100 |  | dfcleq 2729 | . . . . . 6
⊢ (∪ 𝑇 =
ℝ ↔ ∀𝑦(𝑦 ∈ ∪ 𝑇 ↔ 𝑦 ∈ ℝ)) | 
| 101 | 99, 100 | sylibr 234 | . . . . 5
⊢ (𝜑 → ∪ 𝑇 =
ℝ) | 
| 102 | 101 | difeq1d 4124 | . . . 4
⊢ (𝜑 → (∪ 𝑇
∖ 𝑥) = (ℝ
∖ 𝑥)) | 
| 103 | 102 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (∪ 𝑇 ∖ 𝑥) = (ℝ ∖ 𝑥)) | 
| 104 |  | difss 4135 | . . . . . . 7
⊢ (ℝ
∖ 𝑥) ⊆
ℝ | 
| 105 | 2, 104 | ssexi 5321 | . . . . . . . 8
⊢ (ℝ
∖ 𝑥) ∈
V | 
| 106 |  | elpwg 4602 | . . . . . . . 8
⊢ ((ℝ
∖ 𝑥) ∈ V →
((ℝ ∖ 𝑥) ∈
𝒫 ℝ ↔ (ℝ ∖ 𝑥) ⊆ ℝ)) | 
| 107 | 105, 106 | ax-mp 5 | . . . . . . 7
⊢ ((ℝ
∖ 𝑥) ∈ 𝒫
ℝ ↔ (ℝ ∖ 𝑥) ⊆ ℝ) | 
| 108 | 104, 107 | mpbir 231 | . . . . . 6
⊢ (ℝ
∖ 𝑥) ∈ 𝒫
ℝ | 
| 109 | 108 | a1i 11 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (ℝ ∖ 𝑥) ∈ 𝒫 ℝ) | 
| 110 | 57 | ffund 6739 | . . . . . . . . 9
⊢ (𝜑 → Fun 𝐹) | 
| 111 |  | difpreima 7084 | . . . . . . . . 9
⊢ (Fun
𝐹 → (◡𝐹 “ (ℝ ∖ 𝑥)) = ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ 𝑥))) | 
| 112 | 110, 111 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (◡𝐹 “ (ℝ ∖ 𝑥)) = ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ 𝑥))) | 
| 113 |  | fimacnv 6757 | . . . . . . . . . . 11
⊢ (𝐹:𝐷⟶ℝ → (◡𝐹 “ ℝ) = 𝐷) | 
| 114 | 57, 113 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (◡𝐹 “ ℝ) = 𝐷) | 
| 115 | 10, 14 | restuni4 45131 | . . . . . . . . . 10
⊢ (𝜑 → ∪ (𝑆
↾t 𝐷) =
𝐷) | 
| 116 | 114, 115 | eqtr4d 2779 | . . . . . . . . 9
⊢ (𝜑 → (◡𝐹 “ ℝ) = ∪ (𝑆
↾t 𝐷)) | 
| 117 | 116 | difeq1d 4124 | . . . . . . . 8
⊢ (𝜑 → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ 𝑥)) = (∪ (𝑆 ↾t 𝐷) ∖ (◡𝐹 “ 𝑥))) | 
| 118 | 112, 117 | eqtrd 2776 | . . . . . . 7
⊢ (𝜑 → (◡𝐹 “ (ℝ ∖ 𝑥)) = (∪ (𝑆 ↾t 𝐷) ∖ (◡𝐹 “ 𝑥))) | 
| 119 | 118 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (◡𝐹 “ (ℝ ∖ 𝑥)) = (∪ (𝑆 ↾t 𝐷) ∖ (◡𝐹 “ 𝑥))) | 
| 120 | 17 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝑆 ↾t 𝐷) ∈ SAlg) | 
| 121 |  | imaeq2 6073 | . . . . . . . . . . . 12
⊢ (𝑒 = 𝑥 → (◡𝐹 “ 𝑒) = (◡𝐹 “ 𝑥)) | 
| 122 | 121 | eleq1d 2825 | . . . . . . . . . . 11
⊢ (𝑒 = 𝑥 → ((◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ 𝑥) ∈ (𝑆 ↾t 𝐷))) | 
| 123 | 122, 1 | elrab2 3694 | . . . . . . . . . 10
⊢ (𝑥 ∈ 𝑇 ↔ (𝑥 ∈ 𝒫 ℝ ∧ (◡𝐹 “ 𝑥) ∈ (𝑆 ↾t 𝐷))) | 
| 124 | 123 | biimpi 216 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝑇 → (𝑥 ∈ 𝒫 ℝ ∧ (◡𝐹 “ 𝑥) ∈ (𝑆 ↾t 𝐷))) | 
| 125 | 124 | simprd 495 | . . . . . . . 8
⊢ (𝑥 ∈ 𝑇 → (◡𝐹 “ 𝑥) ∈ (𝑆 ↾t 𝐷)) | 
| 126 | 125 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (◡𝐹 “ 𝑥) ∈ (𝑆 ↾t 𝐷)) | 
| 127 | 120, 126 | saldifcld 46367 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (∪
(𝑆 ↾t
𝐷) ∖ (◡𝐹 “ 𝑥)) ∈ (𝑆 ↾t 𝐷)) | 
| 128 | 119, 127 | eqeltrd 2840 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ (𝑆 ↾t 𝐷)) | 
| 129 | 109, 128 | jca 511 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → ((ℝ ∖ 𝑥) ∈ 𝒫 ℝ ∧
(◡𝐹 “ (ℝ ∖ 𝑥)) ∈ (𝑆 ↾t 𝐷))) | 
| 130 |  | imaeq2 6073 | . . . . . 6
⊢ (𝑒 = (ℝ ∖ 𝑥) → (◡𝐹 “ 𝑒) = (◡𝐹 “ (ℝ ∖ 𝑥))) | 
| 131 | 130 | eleq1d 2825 | . . . . 5
⊢ (𝑒 = (ℝ ∖ 𝑥) → ((◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ (𝑆 ↾t 𝐷))) | 
| 132 | 131, 1 | elrab2 3694 | . . . 4
⊢ ((ℝ
∖ 𝑥) ∈ 𝑇 ↔ ((ℝ ∖ 𝑥) ∈ 𝒫 ℝ ∧
(◡𝐹 “ (ℝ ∖ 𝑥)) ∈ (𝑆 ↾t 𝐷))) | 
| 133 | 129, 132 | sylibr 234 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (ℝ ∖ 𝑥) ∈ 𝑇) | 
| 134 | 103, 133 | eqeltrd 2840 | . 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (∪ 𝑇 ∖ 𝑥) ∈ 𝑇) | 
| 135 |  | nnex 12273 | . . . . . . . 8
⊢ ℕ
∈ V | 
| 136 |  | fvex 6918 | . . . . . . . 8
⊢ (𝑔‘𝑛) ∈ V | 
| 137 | 135, 136 | iunex 7994 | . . . . . . 7
⊢ ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) ∈ V | 
| 138 | 137 | a1i 11 | . . . . . 6
⊢ (𝑔:ℕ⟶𝑇 → ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) ∈ V) | 
| 139 |  | ffvelcdm 7100 | . . . . . . . 8
⊢ ((𝑔:ℕ⟶𝑇 ∧ 𝑛 ∈ ℕ) → (𝑔‘𝑛) ∈ 𝑇) | 
| 140 | 1 | eleq2i 2832 | . . . . . . . . 9
⊢ ((𝑔‘𝑛) ∈ 𝑇 ↔ (𝑔‘𝑛) ∈ {𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)}) | 
| 141 | 140 | biimpi 216 | . . . . . . . 8
⊢ ((𝑔‘𝑛) ∈ 𝑇 → (𝑔‘𝑛) ∈ {𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)}) | 
| 142 |  | elrabi 3686 | . . . . . . . 8
⊢ ((𝑔‘𝑛) ∈ {𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)} → (𝑔‘𝑛) ∈ 𝒫 ℝ) | 
| 143 |  | elpwi 4606 | . . . . . . . 8
⊢ ((𝑔‘𝑛) ∈ 𝒫 ℝ → (𝑔‘𝑛) ⊆ ℝ) | 
| 144 | 139, 141,
142, 143 | 4syl 19 | . . . . . . 7
⊢ ((𝑔:ℕ⟶𝑇 ∧ 𝑛 ∈ ℕ) → (𝑔‘𝑛) ⊆ ℝ) | 
| 145 | 144 | iunssd 5049 | . . . . . 6
⊢ (𝑔:ℕ⟶𝑇 → ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) ⊆ ℝ) | 
| 146 | 138, 145 | elpwd 4605 | . . . . 5
⊢ (𝑔:ℕ⟶𝑇 → ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) ∈ 𝒫 ℝ) | 
| 147 | 146 | adantl 481 | . . . 4
⊢ ((𝜑 ∧ 𝑔:ℕ⟶𝑇) → ∪
𝑛 ∈ ℕ (𝑔‘𝑛) ∈ 𝒫 ℝ) | 
| 148 |  | imaiun 7266 | . . . . . 6
⊢ (◡𝐹 “ ∪
𝑛 ∈ ℕ (𝑔‘𝑛)) = ∪
𝑛 ∈ ℕ (◡𝐹 “ (𝑔‘𝑛)) | 
| 149 | 148 | a1i 11 | . . . . 5
⊢ ((𝜑 ∧ 𝑔:ℕ⟶𝑇) → (◡𝐹 “ ∪
𝑛 ∈ ℕ (𝑔‘𝑛)) = ∪
𝑛 ∈ ℕ (◡𝐹 “ (𝑔‘𝑛))) | 
| 150 | 17 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑔:ℕ⟶𝑇) → (𝑆 ↾t 𝐷) ∈ SAlg) | 
| 151 |  | nnct 14023 | . . . . . . 7
⊢ ℕ
≼ ω | 
| 152 | 151 | a1i 11 | . . . . . 6
⊢ ((𝜑 ∧ 𝑔:ℕ⟶𝑇) → ℕ ≼
ω) | 
| 153 |  | imaeq2 6073 | . . . . . . . . . . . 12
⊢ (𝑒 = (𝑔‘𝑛) → (◡𝐹 “ 𝑒) = (◡𝐹 “ (𝑔‘𝑛))) | 
| 154 | 153 | eleq1d 2825 | . . . . . . . . . . 11
⊢ (𝑒 = (𝑔‘𝑛) → ((◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷))) | 
| 155 | 154, 1 | elrab2 3694 | . . . . . . . . . 10
⊢ ((𝑔‘𝑛) ∈ 𝑇 ↔ ((𝑔‘𝑛) ∈ 𝒫 ℝ ∧ (◡𝐹 “ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷))) | 
| 156 | 155 | biimpi 216 | . . . . . . . . 9
⊢ ((𝑔‘𝑛) ∈ 𝑇 → ((𝑔‘𝑛) ∈ 𝒫 ℝ ∧ (◡𝐹 “ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷))) | 
| 157 | 156 | simprd 495 | . . . . . . . 8
⊢ ((𝑔‘𝑛) ∈ 𝑇 → (◡𝐹 “ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷)) | 
| 158 | 139, 157 | syl 17 | . . . . . . 7
⊢ ((𝑔:ℕ⟶𝑇 ∧ 𝑛 ∈ ℕ) → (◡𝐹 “ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷)) | 
| 159 | 158 | adantll 714 | . . . . . 6
⊢ (((𝜑 ∧ 𝑔:ℕ⟶𝑇) ∧ 𝑛 ∈ ℕ) → (◡𝐹 “ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷)) | 
| 160 | 150, 152,
159 | saliuncl 46343 | . . . . 5
⊢ ((𝜑 ∧ 𝑔:ℕ⟶𝑇) → ∪
𝑛 ∈ ℕ (◡𝐹 “ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷)) | 
| 161 | 149, 160 | eqeltrd 2840 | . . . 4
⊢ ((𝜑 ∧ 𝑔:ℕ⟶𝑇) → (◡𝐹 “ ∪
𝑛 ∈ ℕ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷)) | 
| 162 | 147, 161 | jca 511 | . . 3
⊢ ((𝜑 ∧ 𝑔:ℕ⟶𝑇) → (∪ 𝑛 ∈ ℕ (𝑔‘𝑛) ∈ 𝒫 ℝ ∧ (◡𝐹 “ ∪
𝑛 ∈ ℕ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷))) | 
| 163 |  | imaeq2 6073 | . . . . 5
⊢ (𝑒 = ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) → (◡𝐹 “ 𝑒) = (◡𝐹 “ ∪
𝑛 ∈ ℕ (𝑔‘𝑛))) | 
| 164 | 163 | eleq1d 2825 | . . . 4
⊢ (𝑒 = ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) → ((◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ ∪
𝑛 ∈ ℕ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷))) | 
| 165 | 164, 1 | elrab2 3694 | . . 3
⊢ (∪ 𝑛 ∈ ℕ (𝑔‘𝑛) ∈ 𝑇 ↔ (∪
𝑛 ∈ ℕ (𝑔‘𝑛) ∈ 𝒫 ℝ ∧ (◡𝐹 “ ∪
𝑛 ∈ ℕ (𝑔‘𝑛)) ∈ (𝑆 ↾t 𝐷))) | 
| 166 | 162, 165 | sylibr 234 | . 2
⊢ ((𝜑 ∧ 𝑔:ℕ⟶𝑇) → ∪
𝑛 ∈ ℕ (𝑔‘𝑛) ∈ 𝑇) | 
| 167 | 5, 24, 25, 134, 166 | issalnnd 46365 | 1
⊢ (𝜑 → 𝑇 ∈ SAlg) |