| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | smfrec.x | . 2
⊢
Ⅎ𝑥𝜑 | 
| 2 |  | nfv 1914 | . 2
⊢
Ⅎ𝑎𝜑 | 
| 3 |  | smfrec.s | . 2
⊢ (𝜑 → 𝑆 ∈ SAlg) | 
| 4 |  | smfrec.e | . . . 4
⊢ 𝐶 = {𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 0} | 
| 5 |  | ssrab2 4080 | . . . 4
⊢ {𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 0} ⊆ 𝐴 | 
| 6 | 4, 5 | eqsstri 4030 | . . 3
⊢ 𝐶 ⊆ 𝐴 | 
| 7 |  | eqid 2737 | . . . . . 6
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) | 
| 8 |  | smfrec.b | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) | 
| 9 | 1, 7, 8 | dmmptdf 45229 | . . . . 5
⊢ (𝜑 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴) | 
| 10 | 9 | eqcomd 2743 | . . . 4
⊢ (𝜑 → 𝐴 = dom (𝑥 ∈ 𝐴 ↦ 𝐵)) | 
| 11 |  | smfrec.m | . . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆)) | 
| 12 |  | eqid 2737 | . . . . 5
⊢ dom
(𝑥 ∈ 𝐴 ↦ 𝐵) = dom (𝑥 ∈ 𝐴 ↦ 𝐵) | 
| 13 | 3, 11, 12 | smfdmss 46748 | . . . 4
⊢ (𝜑 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ ∪ 𝑆) | 
| 14 | 10, 13 | eqsstrd 4018 | . . 3
⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑆) | 
| 15 | 6, 14 | sstrid 3995 | . 2
⊢ (𝜑 → 𝐶 ⊆ ∪ 𝑆) | 
| 16 |  | 1red 11262 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 1 ∈ ℝ) | 
| 17 | 6 | sseli 3979 | . . . . 5
⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐴) | 
| 18 | 17 | adantl 481 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ 𝐴) | 
| 19 | 18, 8 | syldan 591 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐵 ∈ ℝ) | 
| 20 | 4 | eleq2i 2833 | . . . . . 6
⊢ (𝑥 ∈ 𝐶 ↔ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 0}) | 
| 21 | 20 | biimpi 216 | . . . . 5
⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 0}) | 
| 22 |  | rabidim2 45107 | . . . . 5
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 0} → 𝐵 ≠ 0) | 
| 23 | 21, 22 | syl 17 | . . . 4
⊢ (𝑥 ∈ 𝐶 → 𝐵 ≠ 0) | 
| 24 | 23 | adantl 481 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐵 ≠ 0) | 
| 25 | 16, 19, 24 | redivcld 12095 | . 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (1 / 𝐵) ∈ ℝ) | 
| 26 |  | nfv 1914 | . . . . . . 7
⊢
Ⅎ𝑥 𝑎 ∈ ℝ | 
| 27 | 1, 26 | nfan 1899 | . . . . . 6
⊢
Ⅎ𝑥(𝜑 ∧ 𝑎 ∈ ℝ) | 
| 28 |  | nfv 1914 | . . . . . 6
⊢
Ⅎ𝑥0 < 𝑎 | 
| 29 | 27, 28 | nfan 1899 | . . . . 5
⊢
Ⅎ𝑥((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 0 < 𝑎) | 
| 30 | 19 | ad4ant14 752 | . . . . 5
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 0 < 𝑎) ∧ 𝑥 ∈ 𝐶) → 𝐵 ∈ ℝ) | 
| 31 | 23 | adantl 481 | . . . . 5
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 0 < 𝑎) ∧ 𝑥 ∈ 𝐶) → 𝐵 ≠ 0) | 
| 32 |  | simpl 482 | . . . . . . 7
⊢ ((𝑎 ∈ ℝ ∧ 0 <
𝑎) → 𝑎 ∈
ℝ) | 
| 33 |  | simpr 484 | . . . . . . 7
⊢ ((𝑎 ∈ ℝ ∧ 0 <
𝑎) → 0 < 𝑎) | 
| 34 | 32, 33 | elrpd 13074 | . . . . . 6
⊢ ((𝑎 ∈ ℝ ∧ 0 <
𝑎) → 𝑎 ∈
ℝ+) | 
| 35 | 34 | adantll 714 | . . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 0 < 𝑎) → 𝑎 ∈ ℝ+) | 
| 36 | 29, 30, 31, 35 | pimrecltpos 46723 | . . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 0 < 𝑎) → {𝑥 ∈ 𝐶 ∣ (1 / 𝐵) < 𝑎} = ({𝑥 ∈ 𝐶 ∣ (1 / 𝑎) < 𝐵} ∪ {𝑥 ∈ 𝐶 ∣ 𝐵 < 0})) | 
| 37 |  | smfrec.a | . . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑉) | 
| 38 | 4, 37 | rabexd 5340 | . . . . . . 7
⊢ (𝜑 → 𝐶 ∈ V) | 
| 39 |  | eqid 2737 | . . . . . . 7
⊢ (𝑆 ↾t 𝐶) = (𝑆 ↾t 𝐶) | 
| 40 | 3, 38, 39 | subsalsal 46374 | . . . . . 6
⊢ (𝜑 → (𝑆 ↾t 𝐶) ∈ SAlg) | 
| 41 | 40 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 0 < 𝑎) → (𝑆 ↾t 𝐶) ∈ SAlg) | 
| 42 | 3 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝑆 ∈ SAlg) | 
| 43 | 42 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 0 < 𝑎) → 𝑆 ∈ SAlg) | 
| 44 | 6 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → 𝐶 ⊆ 𝐴) | 
| 45 | 3, 11, 44 | sssmfmpt 46765 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ 𝐵) ∈ (SMblFn‘𝑆)) | 
| 46 | 45 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (𝑥 ∈ 𝐶 ↦ 𝐵) ∈ (SMblFn‘𝑆)) | 
| 47 | 46 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 0 < 𝑎) → (𝑥 ∈ 𝐶 ↦ 𝐵) ∈ (SMblFn‘𝑆)) | 
| 48 | 34 | rprecred 13088 | . . . . . . 7
⊢ ((𝑎 ∈ ℝ ∧ 0 <
𝑎) → (1 / 𝑎) ∈
ℝ) | 
| 49 | 48 | adantll 714 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 0 < 𝑎) → (1 / 𝑎) ∈ ℝ) | 
| 50 | 29, 43, 30, 47, 49 | smfpimgtmpt 46796 | . . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 0 < 𝑎) → {𝑥 ∈ 𝐶 ∣ (1 / 𝑎) < 𝐵} ∈ (𝑆 ↾t 𝐶)) | 
| 51 |  | 0red 11264 | . . . . . . 7
⊢ (𝜑 → 0 ∈
ℝ) | 
| 52 | 1, 3, 19, 45, 51 | smfpimltmpt 46761 | . . . . . 6
⊢ (𝜑 → {𝑥 ∈ 𝐶 ∣ 𝐵 < 0} ∈ (𝑆 ↾t 𝐶)) | 
| 53 | 52 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 0 < 𝑎) → {𝑥 ∈ 𝐶 ∣ 𝐵 < 0} ∈ (𝑆 ↾t 𝐶)) | 
| 54 | 41, 50, 53 | saluncld 46363 | . . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 0 < 𝑎) → ({𝑥 ∈ 𝐶 ∣ (1 / 𝑎) < 𝐵} ∪ {𝑥 ∈ 𝐶 ∣ 𝐵 < 0}) ∈ (𝑆 ↾t 𝐶)) | 
| 55 | 36, 54 | eqeltrd 2841 | . . 3
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 0 < 𝑎) → {𝑥 ∈ 𝐶 ∣ (1 / 𝐵) < 𝑎} ∈ (𝑆 ↾t 𝐶)) | 
| 56 |  | nfv 1914 | . . . . . . . 8
⊢
Ⅎ𝑥 𝑎 = 0 | 
| 57 | 1, 56 | nfan 1899 | . . . . . . 7
⊢
Ⅎ𝑥(𝜑 ∧ 𝑎 = 0) | 
| 58 |  | breq2 5147 | . . . . . . . . 9
⊢ (𝑎 = 0 → ((1 / 𝐵) < 𝑎 ↔ (1 / 𝐵) < 0)) | 
| 59 | 58 | ad2antlr 727 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 = 0) ∧ 𝑥 ∈ 𝐶) → ((1 / 𝐵) < 𝑎 ↔ (1 / 𝐵) < 0)) | 
| 60 | 19, 24 | reclt0 45402 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐵 < 0 ↔ (1 / 𝐵) < 0)) | 
| 61 | 60 | bicomd 223 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((1 / 𝐵) < 0 ↔ 𝐵 < 0)) | 
| 62 | 61 | adantlr 715 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 = 0) ∧ 𝑥 ∈ 𝐶) → ((1 / 𝐵) < 0 ↔ 𝐵 < 0)) | 
| 63 | 59, 62 | bitrd 279 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑎 = 0) ∧ 𝑥 ∈ 𝐶) → ((1 / 𝐵) < 𝑎 ↔ 𝐵 < 0)) | 
| 64 | 57, 63 | rabbida 3463 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 = 0) → {𝑥 ∈ 𝐶 ∣ (1 / 𝐵) < 𝑎} = {𝑥 ∈ 𝐶 ∣ 𝐵 < 0}) | 
| 65 | 52 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 = 0) → {𝑥 ∈ 𝐶 ∣ 𝐵 < 0} ∈ (𝑆 ↾t 𝐶)) | 
| 66 | 64, 65 | eqeltrd 2841 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 = 0) → {𝑥 ∈ 𝐶 ∣ (1 / 𝐵) < 𝑎} ∈ (𝑆 ↾t 𝐶)) | 
| 67 | 66 | ad4ant14 752 | . . . 4
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ¬ 0 < 𝑎) ∧ 𝑎 = 0) → {𝑥 ∈ 𝐶 ∣ (1 / 𝐵) < 𝑎} ∈ (𝑆 ↾t 𝐶)) | 
| 68 |  | simpll 767 | . . . . 5
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ¬ 0 < 𝑎) ∧ ¬ 𝑎 = 0) → (𝜑 ∧ 𝑎 ∈ ℝ)) | 
| 69 |  | simpll 767 | . . . . . . 7
⊢ (((𝑎 ∈ ℝ ∧ ¬ 0
< 𝑎) ∧ ¬ 𝑎 = 0) → 𝑎 ∈ ℝ) | 
| 70 |  | 0red 11264 | . . . . . . 7
⊢ (((𝑎 ∈ ℝ ∧ ¬ 0
< 𝑎) ∧ ¬ 𝑎 = 0) → 0 ∈
ℝ) | 
| 71 |  | neqne 2948 | . . . . . . . 8
⊢ (¬
𝑎 = 0 → 𝑎 ≠ 0) | 
| 72 | 71 | adantl 481 | . . . . . . 7
⊢ (((𝑎 ∈ ℝ ∧ ¬ 0
< 𝑎) ∧ ¬ 𝑎 = 0) → 𝑎 ≠ 0) | 
| 73 |  | simplr 769 | . . . . . . 7
⊢ (((𝑎 ∈ ℝ ∧ ¬ 0
< 𝑎) ∧ ¬ 𝑎 = 0) → ¬ 0 < 𝑎) | 
| 74 | 69, 70, 72, 73 | lttri5d 45311 | . . . . . 6
⊢ (((𝑎 ∈ ℝ ∧ ¬ 0
< 𝑎) ∧ ¬ 𝑎 = 0) → 𝑎 < 0) | 
| 75 | 74 | adantlll 718 | . . . . 5
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ¬ 0 < 𝑎) ∧ ¬ 𝑎 = 0) → 𝑎 < 0) | 
| 76 |  | nfv 1914 | . . . . . . . 8
⊢
Ⅎ𝑥 𝑎 < 0 | 
| 77 | 27, 76 | nfan 1899 | . . . . . . 7
⊢
Ⅎ𝑥((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) | 
| 78 | 8 | adantlr 715 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) | 
| 79 | 17, 78 | sylan2 593 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑥 ∈ 𝐶) → 𝐵 ∈ ℝ) | 
| 80 | 79 | adantlr 715 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) ∧ 𝑥 ∈ 𝐶) → 𝐵 ∈ ℝ) | 
| 81 | 23 | adantl 481 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) ∧ 𝑥 ∈ 𝐶) → 𝐵 ≠ 0) | 
| 82 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ) | 
| 83 | 82 | adantr 480 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) → 𝑎 ∈ ℝ) | 
| 84 |  | simpr 484 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) → 𝑎 < 0) | 
| 85 | 77, 80, 81, 83, 84 | pimrecltneg 46739 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) → {𝑥 ∈ 𝐶 ∣ (1 / 𝐵) < 𝑎} = {𝑥 ∈ 𝐶 ∣ 𝐵 ∈ ((1 / 𝑎)(,)0)}) | 
| 86 | 42 | adantr 480 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) → 𝑆 ∈ SAlg) | 
| 87 | 38 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) → 𝐶 ∈ V) | 
| 88 | 46 | adantr 480 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) → (𝑥 ∈ 𝐶 ↦ 𝐵) ∈ (SMblFn‘𝑆)) | 
| 89 |  | 1red 11262 | . . . . . . . . . 10
⊢ ((𝑎 ∈ ℝ ∧ 𝑎 < 0) → 1 ∈
ℝ) | 
| 90 |  | simpl 482 | . . . . . . . . . 10
⊢ ((𝑎 ∈ ℝ ∧ 𝑎 < 0) → 𝑎 ∈
ℝ) | 
| 91 |  | lt0ne0 11729 | . . . . . . . . . 10
⊢ ((𝑎 ∈ ℝ ∧ 𝑎 < 0) → 𝑎 ≠ 0) | 
| 92 | 89, 90, 91 | redivcld 12095 | . . . . . . . . 9
⊢ ((𝑎 ∈ ℝ ∧ 𝑎 < 0) → (1 / 𝑎) ∈
ℝ) | 
| 93 | 92 | adantll 714 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) → (1 / 𝑎) ∈ ℝ) | 
| 94 | 93 | rexrd 11311 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) → (1 / 𝑎) ∈
ℝ*) | 
| 95 | 51 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) → 0 ∈
ℝ) | 
| 96 | 95 | rexrd 11311 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) → 0 ∈
ℝ*) | 
| 97 | 77, 86, 87, 80, 88, 94, 96 | smfpimioompt 46801 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) → {𝑥 ∈ 𝐶 ∣ 𝐵 ∈ ((1 / 𝑎)(,)0)} ∈ (𝑆 ↾t 𝐶)) | 
| 98 | 85, 97 | eqeltrd 2841 | . . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 < 0) → {𝑥 ∈ 𝐶 ∣ (1 / 𝐵) < 𝑎} ∈ (𝑆 ↾t 𝐶)) | 
| 99 | 68, 75, 98 | syl2anc 584 | . . . 4
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ¬ 0 < 𝑎) ∧ ¬ 𝑎 = 0) → {𝑥 ∈ 𝐶 ∣ (1 / 𝐵) < 𝑎} ∈ (𝑆 ↾t 𝐶)) | 
| 100 | 67, 99 | pm2.61dan 813 | . . 3
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ¬ 0 < 𝑎) → {𝑥 ∈ 𝐶 ∣ (1 / 𝐵) < 𝑎} ∈ (𝑆 ↾t 𝐶)) | 
| 101 | 55, 100 | pm2.61dan 813 | . 2
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐶 ∣ (1 / 𝐵) < 𝑎} ∈ (𝑆 ↾t 𝐶)) | 
| 102 | 1, 2, 3, 15, 25, 101 | issmfdmpt 46763 | 1
⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (1 / 𝐵)) ∈ (SMblFn‘𝑆)) |