| Step | Hyp | Ref
| Expression |
| 1 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑖𝜑 |
| 2 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑖𝑓 |
| 3 | | nfixp1 8958 |
. . . . . . . . 9
⊢
Ⅎ𝑖X𝑖 ∈
𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) |
| 4 | 2, 3 | nfel 2920 |
. . . . . . . 8
⊢
Ⅎ𝑖 𝑓 ∈ X𝑖 ∈
𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) |
| 5 | 1, 4 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑖(𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) |
| 6 | | ixpfn 8943 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ X𝑖 ∈
𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) → 𝑓 Fn 𝑋) |
| 7 | 6 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 Fn 𝑋) |
| 8 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑖 → (𝐵‘𝑘) = (𝐵‘𝑖)) |
| 9 | 8 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑖 → (-∞(,)(𝐵‘𝑘)) = (-∞(,)(𝐵‘𝑖))) |
| 10 | | iftrue 4531 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) = (-∞(,)(𝐵‘𝑖))) |
| 11 | 9, 10 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑖 → (-∞(,)(𝐵‘𝑘)) = if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ)) |
| 12 | | eqimss 4042 |
. . . . . . . . . . . . . . . . 17
⊢
((-∞(,)(𝐵‘𝑘)) = if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) → (-∞(,)(𝐵‘𝑘)) ⊆ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ)) |
| 13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑖 → (-∞(,)(𝐵‘𝑘)) ⊆ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ)) |
| 14 | | ioossre 13448 |
. . . . . . . . . . . . . . . . 17
⊢
(-∞(,)(𝐵‘𝑘)) ⊆ ℝ |
| 15 | | iffalse 4534 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) = ℝ) |
| 16 | 14, 15 | sseqtrrid 4027 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑘 = 𝑖 → (-∞(,)(𝐵‘𝑘)) ⊆ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ)) |
| 17 | 13, 16 | pm2.61i 182 |
. . . . . . . . . . . . . . 15
⊢
(-∞(,)(𝐵‘𝑘)) ⊆ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) |
| 18 | | mnfxr 11318 |
. . . . . . . . . . . . . . . . 17
⊢ -∞
∈ ℝ* |
| 19 | 18 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → -∞ ∈
ℝ*) |
| 20 | | hspdifhsp.b |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐵:𝑋⟶ℝ) |
| 21 | 20 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ) |
| 22 | 21 | rexrd 11311 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈
ℝ*) |
| 23 | 22 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈
ℝ*) |
| 24 | | hspdifhsp.a |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐴:𝑋⟶ℝ) |
| 25 | 24 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) |
| 26 | | icossre 13468 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ*) → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ℝ) |
| 27 | 25, 22, 26 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ℝ) |
| 28 | 27 | adantlr 715 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ℝ) |
| 29 | | simpl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∈ X𝑖 ∈
𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) |
| 30 | | simpr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∈ X𝑖 ∈
𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) |
| 31 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = 𝑘 → (𝐴‘𝑖) = (𝐴‘𝑘)) |
| 32 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = 𝑘 → (𝐵‘𝑖) = (𝐵‘𝑘)) |
| 33 | 31, 32 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑘 → ((𝐴‘𝑖)[,)(𝐵‘𝑖)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
| 34 | 33 | fvixp 8942 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∈ X𝑖 ∈
𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
| 35 | 29, 30, 34 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ X𝑖 ∈
𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
| 36 | 35 | adantll 714 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
| 37 | 28, 36 | sseldd 3984 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ) |
| 38 | 37 | mnfltd 13166 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → -∞ < (𝑓‘𝑘)) |
| 39 | 25 | rexrd 11311 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈
ℝ*) |
| 40 | 39 | adantlr 715 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈
ℝ*) |
| 41 | | icoltub 45521 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴‘𝑘) ∈ ℝ* ∧ (𝐵‘𝑘) ∈ ℝ* ∧ (𝑓‘𝑘) ∈ ((𝐴‘𝑘)[,)(𝐵‘𝑘))) → (𝑓‘𝑘) < (𝐵‘𝑘)) |
| 42 | 40, 23, 36, 41 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) < (𝐵‘𝑘)) |
| 43 | 19, 23, 37, 38, 42 | eliood 45511 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ (-∞(,)(𝐵‘𝑘))) |
| 44 | 17, 43 | sselid 3981 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ)) |
| 45 | 44 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ)) |
| 46 | 45 | ralrimiva 3146 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ)) |
| 47 | 7, 46 | jca 511 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))) |
| 48 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑓 ∈ V |
| 49 | 48 | elixp 8944 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ X𝑘 ∈
𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))) |
| 50 | 47, 49 | sylibr 234 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ)) |
| 51 | | hspdifhsp.h |
. . . . . . . . . . . . 13
⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈
𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ))) |
| 52 | | equequ1 2024 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = 𝑘 → (𝑖 = 𝑙 ↔ 𝑘 = 𝑙)) |
| 53 | 52 | ifbid 4549 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = 𝑘 → if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)) |
| 54 | 53 | cbvixpv 8955 |
. . . . . . . . . . . . . . . 16
⊢ X𝑖 ∈
𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ) |
| 55 | 54 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝑙 ∈ 𝑥 ∧ 𝑦 ∈ ℝ) → X𝑖 ∈
𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)) |
| 56 | 55 | mpoeq3ia 7511 |
. . . . . . . . . . . . . 14
⊢ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈
𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ)) = (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈
𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)) |
| 57 | 56 | mpteq2i 5247 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈
𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ))) = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈
𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))) |
| 58 | 51, 57 | eqtri 2765 |
. . . . . . . . . . . 12
⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈
𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))) |
| 59 | | hspdifhsp.x |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ∈ Fin) |
| 60 | 59 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝑋 ∈ Fin) |
| 61 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋) |
| 62 | 20 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝐵:𝑋⟶ℝ) |
| 63 | 62, 61 | ffvelcdmd 7105 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈ ℝ) |
| 64 | 58, 60, 61, 63 | hspval 46624 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑖(𝐻‘𝑋)(𝐵‘𝑖)) = X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ)) |
| 65 | 64 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑖(𝐻‘𝑋)(𝐵‘𝑖)) = X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ)) |
| 66 | 50, 65 | eleqtrrd 2844 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) |
| 67 | 18 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → -∞ ∈
ℝ*) |
| 68 | 24 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝐴:𝑋⟶ℝ) |
| 69 | 68, 61 | ffvelcdmd 7105 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ) |
| 70 | 69 | rexrd 11311 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈
ℝ*) |
| 71 | 70 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → (𝐴‘𝑖) ∈
ℝ*) |
| 72 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) |
| 73 | 58, 60, 61, 69 | hspval 46624 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑖(𝐻‘𝑋)(𝐴‘𝑖)) = X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ)) |
| 74 | 73 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → (𝑖(𝐻‘𝑋)(𝐴‘𝑖)) = X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ)) |
| 75 | 72, 74 | eleqtrd 2843 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ)) |
| 76 | 61 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → 𝑖 ∈ 𝑋) |
| 77 | | iftrue 4531 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) = (-∞(,)(𝐴‘𝑖))) |
| 78 | 77 | fvixp 8942 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ X𝑘 ∈
𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ (-∞(,)(𝐴‘𝑖))) |
| 79 | 75, 76, 78 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → (𝑓‘𝑖) ∈ (-∞(,)(𝐴‘𝑖))) |
| 80 | | iooltub 45523 |
. . . . . . . . . . . 12
⊢
((-∞ ∈ ℝ* ∧ (𝐴‘𝑖) ∈ ℝ* ∧ (𝑓‘𝑖) ∈ (-∞(,)(𝐴‘𝑖))) → (𝑓‘𝑖) < (𝐴‘𝑖)) |
| 81 | 67, 71, 79, 80 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → (𝑓‘𝑖) < (𝐴‘𝑖)) |
| 82 | 81 | adantllr 719 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → (𝑓‘𝑖) < (𝐴‘𝑖)) |
| 83 | 70 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈
ℝ*) |
| 84 | 63 | rexrd 11311 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈
ℝ*) |
| 85 | 84 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈
ℝ*) |
| 86 | 48 | elixp 8944 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ X𝑖 ∈
𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))) |
| 87 | 86 | biimpi 216 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ X𝑖 ∈
𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) → (𝑓 Fn 𝑋 ∧ ∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))) |
| 88 | 87 | simprd 495 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ X𝑖 ∈
𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) → ∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖))) |
| 89 | | rspa 3248 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑖 ∈
𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖))) |
| 90 | 88, 89 | sylan 580 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ X𝑖 ∈
𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖))) |
| 91 | 90 | adantll 714 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖))) |
| 92 | | icogelb 13438 |
. . . . . . . . . . . . 13
⊢ (((𝐴‘𝑖) ∈ ℝ* ∧ (𝐵‘𝑖) ∈ ℝ* ∧ (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖))) → (𝐴‘𝑖) ≤ (𝑓‘𝑖)) |
| 93 | 83, 85, 91, 92 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ≤ (𝑓‘𝑖)) |
| 94 | 69 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ) |
| 95 | | icossre 13468 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴‘𝑖) ∈ ℝ ∧ (𝐵‘𝑖) ∈ ℝ*) → ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ⊆ ℝ) |
| 96 | 69, 84, 95 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ⊆ ℝ) |
| 97 | 96 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ⊆ ℝ) |
| 98 | 97, 91 | sseldd 3984 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ℝ) |
| 99 | 94, 98 | lenltd 11407 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝐴‘𝑖) ≤ (𝑓‘𝑖) ↔ ¬ (𝑓‘𝑖) < (𝐴‘𝑖))) |
| 100 | 93, 99 | mpbid 232 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ¬ (𝑓‘𝑖) < (𝐴‘𝑖)) |
| 101 | 100 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → ¬ (𝑓‘𝑖) < (𝐴‘𝑖)) |
| 102 | 82, 101 | pm2.65da 817 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ¬ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) |
| 103 | 66, 102 | eldifd 3962 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) |
| 104 | 103 | ex 412 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) → (𝑖 ∈ 𝑋 → 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))) |
| 105 | 5, 104 | ralrimi 3257 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) → ∀𝑖 ∈ 𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) |
| 106 | | eliin 4996 |
. . . . . . 7
⊢ (𝑓 ∈ V → (𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ↔ ∀𝑖 ∈ 𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))) |
| 107 | 48, 106 | ax-mp 5 |
. . . . . 6
⊢ (𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ↔ ∀𝑖 ∈ 𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) |
| 108 | 105, 107 | sylibr 234 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) → 𝑓 ∈ ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) |
| 109 | 108 | ex 412 |
. . . 4
⊢ (𝜑 → (𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) → 𝑓 ∈ ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))) |
| 110 | | hspdifhsp.n |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ≠ ∅) |
| 111 | | n0 4353 |
. . . . . . . . . . 11
⊢ (𝑋 ≠ ∅ ↔
∃𝑘 𝑘 ∈ 𝑋) |
| 112 | 111 | biimpi 216 |
. . . . . . . . . 10
⊢ (𝑋 ≠ ∅ →
∃𝑘 𝑘 ∈ 𝑋) |
| 113 | 110, 112 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ∃𝑘 𝑘 ∈ 𝑋) |
| 114 | 113 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → ∃𝑘 𝑘 ∈ 𝑋) |
| 115 | | simpl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) |
| 116 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) |
| 117 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = 𝑘 → 𝑖 = 𝑘) |
| 118 | 117, 32 | oveq12d 7449 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = 𝑘 → (𝑖(𝐻‘𝑋)(𝐵‘𝑖)) = (𝑘(𝐻‘𝑋)(𝐵‘𝑘))) |
| 119 | 117, 31 | oveq12d 7449 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = 𝑘 → (𝑖(𝐻‘𝑋)(𝐴‘𝑖)) = (𝑘(𝐻‘𝑋)(𝐴‘𝑘))) |
| 120 | 118, 119 | difeq12d 4127 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑘 → ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) = ((𝑘(𝐻‘𝑋)(𝐵‘𝑘)) ∖ (𝑘(𝐻‘𝑋)(𝐴‘𝑘)))) |
| 121 | 120 | eleq2d 2827 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑘 → (𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ↔ 𝑓 ∈ ((𝑘(𝐻‘𝑋)(𝐵‘𝑘)) ∖ (𝑘(𝐻‘𝑋)(𝐴‘𝑘))))) |
| 122 | 115, 116,
121 | eliind 45076 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ ((𝑘(𝐻‘𝑋)(𝐵‘𝑘)) ∖ (𝑘(𝐻‘𝑋)(𝐴‘𝑘)))) |
| 123 | 122 | eldifad 3963 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ (𝑘(𝐻‘𝑋)(𝐵‘𝑘))) |
| 124 | 123 | adantll 714 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ (𝑘(𝐻‘𝑋)(𝐵‘𝑘))) |
| 125 | | equequ1 2024 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = ℎ → (𝑖 = 𝑙 ↔ ℎ = 𝑙)) |
| 126 | 125 | ifbid 4549 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = ℎ → if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = if(ℎ = 𝑙, (-∞(,)𝑦), ℝ)) |
| 127 | 126 | cbvixpv 8955 |
. . . . . . . . . . . . . . . . 17
⊢ X𝑖 ∈
𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = Xℎ ∈ 𝑥 if(ℎ = 𝑙, (-∞(,)𝑦), ℝ) |
| 128 | 127 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑙 ∈ 𝑥 ∧ 𝑦 ∈ ℝ) → X𝑖 ∈
𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = Xℎ ∈ 𝑥 if(ℎ = 𝑙, (-∞(,)𝑦), ℝ)) |
| 129 | 128 | mpoeq3ia 7511 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈
𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ)) = (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ Xℎ ∈
𝑥 if(ℎ = 𝑙, (-∞(,)𝑦), ℝ)) |
| 130 | 129 | mpteq2i 5247 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈
𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ))) = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ Xℎ ∈
𝑥 if(ℎ = 𝑙, (-∞(,)𝑦), ℝ))) |
| 131 | 51, 130 | eqtri 2765 |
. . . . . . . . . . . . 13
⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ Xℎ ∈
𝑥 if(ℎ = 𝑙, (-∞(,)𝑦), ℝ))) |
| 132 | 59 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → 𝑋 ∈ Fin) |
| 133 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) |
| 134 | 21 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ) |
| 135 | 131, 132,
133, 134 | hspval 46624 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → (𝑘(𝐻‘𝑋)(𝐵‘𝑘)) = Xℎ ∈ 𝑋 if(ℎ = 𝑘, (-∞(,)(𝐵‘𝑘)), ℝ)) |
| 136 | 124, 135 | eleqtrd 2843 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ Xℎ ∈ 𝑋 if(ℎ = 𝑘, (-∞(,)(𝐵‘𝑘)), ℝ)) |
| 137 | | ixpfn 8943 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ Xℎ ∈
𝑋 if(ℎ = 𝑘, (-∞(,)(𝐵‘𝑘)), ℝ) → 𝑓 Fn 𝑋) |
| 138 | 136, 137 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → 𝑓 Fn 𝑋) |
| 139 | 138 | ex 412 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → (𝑘 ∈ 𝑋 → 𝑓 Fn 𝑋)) |
| 140 | 139 | exlimdv 1933 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → (∃𝑘 𝑘 ∈ 𝑋 → 𝑓 Fn 𝑋)) |
| 141 | 114, 140 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → 𝑓 Fn 𝑋) |
| 142 | | nfii1 5029 |
. . . . . . . . . 10
⊢
Ⅎ𝑖∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) |
| 143 | 2, 142 | nfel 2920 |
. . . . . . . . 9
⊢
Ⅎ𝑖 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) |
| 144 | 1, 143 | nfan 1899 |
. . . . . . . 8
⊢
Ⅎ𝑖(𝜑 ∧ 𝑓 ∈ ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) |
| 145 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝜑) |
| 146 | 107 | biimpi 216 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → ∀𝑖 ∈ 𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) |
| 147 | 146 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ∀𝑖 ∈ 𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) |
| 148 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋) |
| 149 | | rspa 3248 |
. . . . . . . . . . . 12
⊢
((∀𝑖 ∈
𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) |
| 150 | 147, 148,
149 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) |
| 151 | 150 | adantll 714 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) |
| 152 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋) |
| 153 | 70 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈
ℝ*) |
| 154 | 84 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈
ℝ*) |
| 155 | | simpll 767 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝜑) |
| 156 | | eldifi 4131 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) |
| 157 | 156 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) |
| 158 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋) |
| 159 | | ioossre 13448 |
. . . . . . . . . . . . . 14
⊢
(-∞(,)(𝐵‘𝑖)) ⊆ ℝ |
| 160 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) |
| 161 | 64 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑖(𝐻‘𝑋)(𝐵‘𝑖)) = X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ)) |
| 162 | 160, 161 | eleqtrd 2843 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ)) |
| 163 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋) |
| 164 | 10 | fvixp 8942 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ X𝑘 ∈
𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ (-∞(,)(𝐵‘𝑖))) |
| 165 | 162, 163,
164 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ (-∞(,)(𝐵‘𝑖))) |
| 166 | 159, 165 | sselid 3981 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ℝ) |
| 167 | 155, 157,
158, 166 | syl21anc 838 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ℝ) |
| 168 | 167 | rexrd 11311 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈
ℝ*) |
| 169 | | simpl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → 𝜑) |
| 170 | 156 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) |
| 171 | 169, 170 | jca 511 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → (𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖)))) |
| 172 | 171 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖)))) |
| 173 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → 𝑖 ∈ 𝑋) |
| 174 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝑓‘𝑖) < (𝐴‘𝑖)) |
| 175 | | ixpfn 8943 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ X𝑘 ∈
𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) → 𝑓 Fn 𝑋) |
| 176 | 162, 175 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 Fn 𝑋) |
| 177 | 176 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → 𝑓 Fn 𝑋) |
| 178 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = 𝑖 → (𝑓‘𝑘) = (𝑓‘𝑖)) |
| 179 | 178 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 = 𝑖) → (𝑓‘𝑘) = (𝑓‘𝑖)) |
| 180 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → -∞ ∈
ℝ*) |
| 181 | 70 | ad4ant13 751 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝐴‘𝑖) ∈
ℝ*) |
| 182 | 166 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝑓‘𝑖) ∈ ℝ) |
| 183 | 182 | mnfltd 13166 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → -∞ < (𝑓‘𝑖)) |
| 184 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝑓‘𝑖) < (𝐴‘𝑖)) |
| 185 | 180, 181,
182, 183, 184 | eliood 45511 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝑓‘𝑖) ∈ (-∞(,)(𝐴‘𝑖))) |
| 186 | 185 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 = 𝑖) → (𝑓‘𝑖) ∈ (-∞(,)(𝐴‘𝑖))) |
| 187 | 179, 186 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ (-∞(,)(𝐴‘𝑖))) |
| 188 | 187 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ (-∞(,)(𝐴‘𝑖))) |
| 189 | 77 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑖 → (-∞(,)(𝐴‘𝑖)) = if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ)) |
| 190 | 189 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝑖) → (-∞(,)(𝐴‘𝑖)) = if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ)) |
| 191 | 188, 190 | eleqtrd 2843 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ)) |
| 192 | 10, 159 | eqsstrdi 4028 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ⊆
ℝ) |
| 193 | | ssid 4006 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ℝ
⊆ ℝ |
| 194 | 15, 193 | eqsstrdi 4028 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ⊆
ℝ) |
| 195 | 192, 194 | pm2.61i 182 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ⊆ ℝ |
| 196 | 162 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ)) |
| 197 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) |
| 198 | | fvixp2 45204 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑓 ∈ X𝑘 ∈
𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ)) |
| 199 | 196, 197,
198 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ)) |
| 200 | 195, 199 | sselid 3981 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ) |
| 201 | 200 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ ℝ) |
| 202 | | iffalse 4534 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬
𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) = ℝ) |
| 203 | 202 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
𝑘 = 𝑖 → ℝ = if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ)) |
| 204 | 203 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝑖) → ℝ = if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ)) |
| 205 | 201, 204 | eleqtrd 2843 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ)) |
| 206 | 205 | adantllr 719 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ)) |
| 207 | 191, 206 | pm2.61dan 813 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ)) |
| 208 | 207 | ralrimiva 3146 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ)) |
| 209 | 177, 208 | jca 511 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))) |
| 210 | 48 | elixp 8944 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ X𝑘 ∈
𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))) |
| 211 | 209, 210 | sylibr 234 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ)) |
| 212 | 73 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) = (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) |
| 213 | 212 | ad4ant13 751 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) = (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) |
| 214 | 211, 213 | eleqtrd 2843 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) |
| 215 | 172, 173,
174, 214 | syl21anc 838 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) |
| 216 | | eldifn 4132 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → ¬ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) |
| 217 | 216 | ad3antlr 731 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → ¬ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) |
| 218 | 215, 217 | pm2.65da 817 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → ¬ (𝑓‘𝑖) < (𝐴‘𝑖)) |
| 219 | 155, 158,
69 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ) |
| 220 | 219, 167 | lenltd 11407 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → ((𝐴‘𝑖) ≤ (𝑓‘𝑖) ↔ ¬ (𝑓‘𝑖) < (𝐴‘𝑖))) |
| 221 | 218, 220 | mpbird 257 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ≤ (𝑓‘𝑖)) |
| 222 | 18 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → -∞ ∈
ℝ*) |
| 223 | 84 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈
ℝ*) |
| 224 | | iooltub 45523 |
. . . . . . . . . . . . 13
⊢
((-∞ ∈ ℝ* ∧ (𝐵‘𝑖) ∈ ℝ* ∧ (𝑓‘𝑖) ∈ (-∞(,)(𝐵‘𝑖))) → (𝑓‘𝑖) < (𝐵‘𝑖)) |
| 225 | 222, 223,
165, 224 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) < (𝐵‘𝑖)) |
| 226 | 155, 157,
158, 225 | syl21anc 838 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) < (𝐵‘𝑖)) |
| 227 | 153, 154,
168, 221, 226 | elicod 13437 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖))) |
| 228 | 145, 151,
152, 227 | syl21anc 838 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖))) |
| 229 | 228 | ex 412 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → (𝑖 ∈ 𝑋 → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))) |
| 230 | 144, 229 | ralrimi 3257 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → ∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖))) |
| 231 | 141, 230 | jca 511 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → (𝑓 Fn 𝑋 ∧ ∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))) |
| 232 | 231, 86 | sylibr 234 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) |
| 233 | 232 | ex 412 |
. . . 4
⊢ (𝜑 → (𝑓 ∈ ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)))) |
| 234 | 109, 233 | impbid 212 |
. . 3
⊢ (𝜑 → (𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ↔ 𝑓 ∈ ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))) |
| 235 | 234 | alrimiv 1927 |
. 2
⊢ (𝜑 → ∀𝑓(𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ↔ 𝑓 ∈ ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))) |
| 236 | | dfcleq 2730 |
. 2
⊢ (X𝑖 ∈
𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) = ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ↔ ∀𝑓(𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ↔ 𝑓 ∈ ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))) |
| 237 | 235, 236 | sylibr 234 |
1
⊢ (𝜑 → X𝑖 ∈
𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) = ∩
𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) |