| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | issmfgt.s | . . . . . . 7
⊢ (𝜑 → 𝑆 ∈ SAlg) | 
| 2 | 1 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝑆 ∈ SAlg) | 
| 3 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹 ∈ (SMblFn‘𝑆)) | 
| 4 |  | issmfgt.d | . . . . . 6
⊢ 𝐷 = dom 𝐹 | 
| 5 | 2, 3, 4 | smfdmss 46753 | . . . . 5
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐷 ⊆ ∪ 𝑆) | 
| 6 | 2, 3, 4 | smff 46752 | . . . . 5
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹:𝐷⟶ℝ) | 
| 7 |  | nfv 1913 | . . . . . . 7
⊢
Ⅎ𝑏𝜑 | 
| 8 |  | nfv 1913 | . . . . . . 7
⊢
Ⅎ𝑏 𝐹 ∈ (SMblFn‘𝑆) | 
| 9 | 7, 8 | nfan 1898 | . . . . . 6
⊢
Ⅎ𝑏(𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) | 
| 10 | 2, 5 | restuni4 45131 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → ∪
(𝑆 ↾t
𝐷) = 𝐷) | 
| 11 | 10 | eqcomd 2742 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐷 = ∪ (𝑆 ↾t 𝐷)) | 
| 12 | 11 | rabeqdv 3451 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → {𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} = {𝑦 ∈ ∪ (𝑆 ↾t 𝐷) ∣ 𝑏 < (𝐹‘𝑦)}) | 
| 13 | 12 | adantr 480 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑏 ∈ ℝ) → {𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} = {𝑦 ∈ ∪ (𝑆 ↾t 𝐷) ∣ 𝑏 < (𝐹‘𝑦)}) | 
| 14 |  | nfv 1913 | . . . . . . . . . . 11
⊢
Ⅎ𝑦𝜑 | 
| 15 |  | nfv 1913 | . . . . . . . . . . 11
⊢
Ⅎ𝑦 𝐹 ∈ (SMblFn‘𝑆) | 
| 16 | 14, 15 | nfan 1898 | . . . . . . . . . 10
⊢
Ⅎ𝑦(𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) | 
| 17 |  | nfv 1913 | . . . . . . . . . 10
⊢
Ⅎ𝑦 𝑏 ∈ ℝ | 
| 18 | 16, 17 | nfan 1898 | . . . . . . . . 9
⊢
Ⅎ𝑦((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑏 ∈ ℝ) | 
| 19 |  | nfv 1913 | . . . . . . . . 9
⊢
Ⅎ𝑐((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑏 ∈ ℝ) | 
| 20 | 1 | uniexd 7763 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ∪ 𝑆
∈ V) | 
| 21 | 20 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐷 ⊆ ∪ 𝑆) → ∪ 𝑆
∈ V) | 
| 22 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐷 ⊆ ∪ 𝑆) → 𝐷 ⊆ ∪ 𝑆) | 
| 23 | 21, 22 | ssexd 5323 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐷 ⊆ ∪ 𝑆) → 𝐷 ∈ V) | 
| 24 | 5, 23 | syldan 591 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐷 ∈ V) | 
| 25 |  | eqid 2736 | . . . . . . . . . . 11
⊢ (𝑆 ↾t 𝐷) = (𝑆 ↾t 𝐷) | 
| 26 | 2, 24, 25 | subsalsal 46379 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (𝑆 ↾t 𝐷) ∈ SAlg) | 
| 27 | 26 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑏 ∈ ℝ) → (𝑆 ↾t 𝐷) ∈ SAlg) | 
| 28 |  | eqid 2736 | . . . . . . . . 9
⊢ ∪ (𝑆
↾t 𝐷) =
∪ (𝑆 ↾t 𝐷) | 
| 29 | 6 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑦 ∈ ∪ (𝑆 ↾t 𝐷)) → 𝐹:𝐷⟶ℝ) | 
| 30 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑦 ∈ ∪ (𝑆 ↾t 𝐷)) → 𝑦 ∈ ∪ (𝑆 ↾t 𝐷)) | 
| 31 | 10 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑦 ∈ ∪ (𝑆 ↾t 𝐷)) → ∪ (𝑆
↾t 𝐷) =
𝐷) | 
| 32 | 30, 31 | eleqtrd 2842 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑦 ∈ ∪ (𝑆 ↾t 𝐷)) → 𝑦 ∈ 𝐷) | 
| 33 | 29, 32 | ffvelcdmd 7104 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑦 ∈ ∪ (𝑆 ↾t 𝐷)) → (𝐹‘𝑦) ∈ ℝ) | 
| 34 | 33 | rexrd 11312 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑦 ∈ ∪ (𝑆 ↾t 𝐷)) → (𝐹‘𝑦) ∈
ℝ*) | 
| 35 | 34 | adantlr 715 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑏 ∈ ℝ) ∧ 𝑦 ∈ ∪ (𝑆 ↾t 𝐷)) → (𝐹‘𝑦) ∈
ℝ*) | 
| 36 | 2, 4 | issmfle 46765 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (𝐹 ∈ (SMblFn‘𝑆) ↔ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑐 ∈ ℝ {𝑦 ∈ 𝐷 ∣ (𝐹‘𝑦) ≤ 𝑐} ∈ (𝑆 ↾t 𝐷)))) | 
| 37 | 3, 36 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑐 ∈ ℝ {𝑦 ∈ 𝐷 ∣ (𝐹‘𝑦) ≤ 𝑐} ∈ (𝑆 ↾t 𝐷))) | 
| 38 | 37 | simp3d 1144 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → ∀𝑐 ∈ ℝ {𝑦 ∈ 𝐷 ∣ (𝐹‘𝑦) ≤ 𝑐} ∈ (𝑆 ↾t 𝐷)) | 
| 39 | 10 | rabeqdv 3451 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → {𝑦 ∈ ∪ (𝑆 ↾t 𝐷) ∣ (𝐹‘𝑦) ≤ 𝑐} = {𝑦 ∈ 𝐷 ∣ (𝐹‘𝑦) ≤ 𝑐}) | 
| 40 | 39 | eleq1d 2825 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → ({𝑦 ∈ ∪ (𝑆 ↾t 𝐷) ∣ (𝐹‘𝑦) ≤ 𝑐} ∈ (𝑆 ↾t 𝐷) ↔ {𝑦 ∈ 𝐷 ∣ (𝐹‘𝑦) ≤ 𝑐} ∈ (𝑆 ↾t 𝐷))) | 
| 41 | 40 | ralbidv 3177 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (∀𝑐 ∈ ℝ {𝑦 ∈ ∪ (𝑆 ↾t 𝐷) ∣ (𝐹‘𝑦) ≤ 𝑐} ∈ (𝑆 ↾t 𝐷) ↔ ∀𝑐 ∈ ℝ {𝑦 ∈ 𝐷 ∣ (𝐹‘𝑦) ≤ 𝑐} ∈ (𝑆 ↾t 𝐷))) | 
| 42 | 38, 41 | mpbird 257 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → ∀𝑐 ∈ ℝ {𝑦 ∈ ∪ (𝑆 ↾t 𝐷) ∣ (𝐹‘𝑦) ≤ 𝑐} ∈ (𝑆 ↾t 𝐷)) | 
| 43 | 42 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑐 ∈ ℝ) → ∀𝑐 ∈ ℝ {𝑦 ∈ ∪ (𝑆
↾t 𝐷)
∣ (𝐹‘𝑦) ≤ 𝑐} ∈ (𝑆 ↾t 𝐷)) | 
| 44 |  | simpr 484 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑐 ∈ ℝ) → 𝑐 ∈ ℝ) | 
| 45 |  | rspa 3247 | . . . . . . . . . . 11
⊢
((∀𝑐 ∈
ℝ {𝑦 ∈ ∪ (𝑆
↾t 𝐷)
∣ (𝐹‘𝑦) ≤ 𝑐} ∈ (𝑆 ↾t 𝐷) ∧ 𝑐 ∈ ℝ) → {𝑦 ∈ ∪ (𝑆 ↾t 𝐷) ∣ (𝐹‘𝑦) ≤ 𝑐} ∈ (𝑆 ↾t 𝐷)) | 
| 46 | 43, 44, 45 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑐 ∈ ℝ) → {𝑦 ∈ ∪ (𝑆 ↾t 𝐷) ∣ (𝐹‘𝑦) ≤ 𝑐} ∈ (𝑆 ↾t 𝐷)) | 
| 47 | 46 | adantlr 715 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑏 ∈ ℝ) ∧ 𝑐 ∈ ℝ) → {𝑦 ∈ ∪ (𝑆 ↾t 𝐷) ∣ (𝐹‘𝑦) ≤ 𝑐} ∈ (𝑆 ↾t 𝐷)) | 
| 48 |  | simpr 484 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑏 ∈ ℝ) → 𝑏 ∈ ℝ) | 
| 49 | 18, 19, 27, 28, 35, 47, 48 | salpreimalegt 46729 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑏 ∈ ℝ) → {𝑦 ∈ ∪ (𝑆 ↾t 𝐷) ∣ 𝑏 < (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷)) | 
| 50 | 13, 49 | eqeltrd 2840 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑏 ∈ ℝ) → {𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷)) | 
| 51 | 50 | ex 412 | . . . . . 6
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (𝑏 ∈ ℝ → {𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷))) | 
| 52 | 9, 51 | ralrimi 3256 | . . . . 5
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷)) | 
| 53 | 5, 6, 52 | 3jca 1128 | . . . 4
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷))) | 
| 54 | 53 | ex 412 | . . 3
⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) → (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷)))) | 
| 55 |  | nfv 1913 | . . . . . . 7
⊢
Ⅎ𝑦 𝐷 ⊆ ∪ 𝑆 | 
| 56 |  | nfv 1913 | . . . . . . 7
⊢
Ⅎ𝑦 𝐹:𝐷⟶ℝ | 
| 57 |  | nfcv 2904 | . . . . . . . 8
⊢
Ⅎ𝑦ℝ | 
| 58 |  | nfrab1 3456 | . . . . . . . . 9
⊢
Ⅎ𝑦{𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} | 
| 59 |  | nfcv 2904 | . . . . . . . . 9
⊢
Ⅎ𝑦(𝑆 ↾t 𝐷) | 
| 60 | 58, 59 | nfel 2919 | . . . . . . . 8
⊢
Ⅎ𝑦{𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷) | 
| 61 | 57, 60 | nfralw 3310 | . . . . . . 7
⊢
Ⅎ𝑦∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷) | 
| 62 | 55, 56, 61 | nf3an 1900 | . . . . . 6
⊢
Ⅎ𝑦(𝐷 ⊆ ∪ 𝑆
∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷)) | 
| 63 | 14, 62 | nfan 1898 | . . . . 5
⊢
Ⅎ𝑦(𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷))) | 
| 64 |  | nfv 1913 | . . . . . . 7
⊢
Ⅎ𝑏 𝐷 ⊆ ∪ 𝑆 | 
| 65 |  | nfv 1913 | . . . . . . 7
⊢
Ⅎ𝑏 𝐹:𝐷⟶ℝ | 
| 66 |  | nfra1 3283 | . . . . . . 7
⊢
Ⅎ𝑏∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷) | 
| 67 | 64, 65, 66 | nf3an 1900 | . . . . . 6
⊢
Ⅎ𝑏(𝐷 ⊆ ∪ 𝑆
∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷)) | 
| 68 | 7, 67 | nfan 1898 | . . . . 5
⊢
Ⅎ𝑏(𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷))) | 
| 69 | 1 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷))) → 𝑆 ∈ SAlg) | 
| 70 |  | simpr1 1194 | . . . . 5
⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷))) → 𝐷 ⊆ ∪ 𝑆) | 
| 71 |  | simpr2 1195 | . . . . 5
⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷))) → 𝐹:𝐷⟶ℝ) | 
| 72 |  | simpr3 1196 | . . . . 5
⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷))) → ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷)) | 
| 73 | 63, 68, 69, 4, 70, 71, 72 | issmfgtlem 46775 | . . . 4
⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷))) → 𝐹 ∈ (SMblFn‘𝑆)) | 
| 74 | 73 | ex 412 | . . 3
⊢ (𝜑 → ((𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷)) → 𝐹 ∈ (SMblFn‘𝑆))) | 
| 75 | 54, 74 | impbid 212 | . 2
⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) ↔ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷)))) | 
| 76 |  | breq1 5145 | . . . . . . . 8
⊢ (𝑏 = 𝑎 → (𝑏 < (𝐹‘𝑦) ↔ 𝑎 < (𝐹‘𝑦))) | 
| 77 | 76 | rabbidv 3443 | . . . . . . 7
⊢ (𝑏 = 𝑎 → {𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} = {𝑦 ∈ 𝐷 ∣ 𝑎 < (𝐹‘𝑦)}) | 
| 78 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥)) | 
| 79 | 78 | breq2d 5154 | . . . . . . . . 9
⊢ (𝑦 = 𝑥 → (𝑎 < (𝐹‘𝑦) ↔ 𝑎 < (𝐹‘𝑥))) | 
| 80 | 79 | cbvrabv 3446 | . . . . . . . 8
⊢ {𝑦 ∈ 𝐷 ∣ 𝑎 < (𝐹‘𝑦)} = {𝑥 ∈ 𝐷 ∣ 𝑎 < (𝐹‘𝑥)} | 
| 81 | 80 | a1i 11 | . . . . . . 7
⊢ (𝑏 = 𝑎 → {𝑦 ∈ 𝐷 ∣ 𝑎 < (𝐹‘𝑦)} = {𝑥 ∈ 𝐷 ∣ 𝑎 < (𝐹‘𝑥)}) | 
| 82 | 77, 81 | eqtrd 2776 | . . . . . 6
⊢ (𝑏 = 𝑎 → {𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} = {𝑥 ∈ 𝐷 ∣ 𝑎 < (𝐹‘𝑥)}) | 
| 83 | 82 | eleq1d 2825 | . . . . 5
⊢ (𝑏 = 𝑎 → ({𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷) ↔ {𝑥 ∈ 𝐷 ∣ 𝑎 < (𝐹‘𝑥)} ∈ (𝑆 ↾t 𝐷))) | 
| 84 | 83 | cbvralvw 3236 | . . . 4
⊢
(∀𝑏 ∈
ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷) ↔ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ 𝑎 < (𝐹‘𝑥)} ∈ (𝑆 ↾t 𝐷)) | 
| 85 | 84 | 3anbi3i 1159 | . . 3
⊢ ((𝐷 ⊆ ∪ 𝑆
∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷)) ↔ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ 𝑎 < (𝐹‘𝑥)} ∈ (𝑆 ↾t 𝐷))) | 
| 86 | 85 | a1i 11 | . 2
⊢ (𝜑 → ((𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑏 ∈ ℝ {𝑦 ∈ 𝐷 ∣ 𝑏 < (𝐹‘𝑦)} ∈ (𝑆 ↾t 𝐷)) ↔ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ 𝑎 < (𝐹‘𝑥)} ∈ (𝑆 ↾t 𝐷)))) | 
| 87 | 75, 86 | bitrd 279 | 1
⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) ↔ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ 𝑎 < (𝐹‘𝑥)} ∈ (𝑆 ↾t 𝐷)))) |