Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hspdifhsp Structured version   Visualization version   GIF version

Theorem hspdifhsp 44947
Description: A n-dimensional half-open interval is the intersection of the difference of half spaces. This is a substep of Proposition 115G (a) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
Hypotheses
Ref Expression
hspdifhsp.x (πœ‘ β†’ 𝑋 ∈ Fin)
hspdifhsp.n (πœ‘ β†’ 𝑋 β‰  βˆ…)
hspdifhsp.a (πœ‘ β†’ 𝐴:π‘‹βŸΆβ„)
hspdifhsp.b (πœ‘ β†’ 𝐡:π‘‹βŸΆβ„)
hspdifhsp.h 𝐻 = (π‘₯ ∈ Fin ↦ (𝑙 ∈ π‘₯, 𝑦 ∈ ℝ ↦ X𝑖 ∈ π‘₯ if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ)))
Assertion
Ref Expression
hspdifhsp (πœ‘ β†’ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) = ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))))
Distinct variable groups:   𝐴,𝑖,𝑙,π‘₯,𝑦   𝐡,𝑖,𝑙,π‘₯,𝑦   𝑖,𝐻,𝑙,π‘₯,𝑦   𝑖,𝑋,𝑙,π‘₯,𝑦   πœ‘,𝑖,𝑙,π‘₯,𝑦

Proof of Theorem hspdifhsp
Dummy variables 𝑓 β„Ž π‘˜ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1918 . . . . . . . 8 β„²π‘–πœ‘
2 nfcv 2904 . . . . . . . . 9 Ⅎ𝑖𝑓
3 nfixp1 8862 . . . . . . . . 9 Ⅎ𝑖X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))
42, 3nfel 2918 . . . . . . . 8 Ⅎ𝑖 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))
51, 4nfan 1903 . . . . . . 7 Ⅎ𝑖(πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)))
6 ixpfn 8847 . . . . . . . . . . . . 13 (𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) β†’ 𝑓 Fn 𝑋)
76ad2antlr 726 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑓 Fn 𝑋)
8 fveq2 6846 . . . . . . . . . . . . . . . . . . 19 (π‘˜ = 𝑖 β†’ (π΅β€˜π‘˜) = (π΅β€˜π‘–))
98oveq2d 7377 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑖 β†’ (-∞(,)(π΅β€˜π‘˜)) = (-∞(,)(π΅β€˜π‘–)))
10 iftrue 4496 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑖 β†’ if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ) = (-∞(,)(π΅β€˜π‘–)))
119, 10eqtr4d 2776 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑖 β†’ (-∞(,)(π΅β€˜π‘˜)) = if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
12 eqimss 4004 . . . . . . . . . . . . . . . . 17 ((-∞(,)(π΅β€˜π‘˜)) = if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ) β†’ (-∞(,)(π΅β€˜π‘˜)) βŠ† if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
1311, 12syl 17 . . . . . . . . . . . . . . . 16 (π‘˜ = 𝑖 β†’ (-∞(,)(π΅β€˜π‘˜)) βŠ† if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
14 ioossre 13334 . . . . . . . . . . . . . . . . 17 (-∞(,)(π΅β€˜π‘˜)) βŠ† ℝ
15 iffalse 4499 . . . . . . . . . . . . . . . . 17 (Β¬ π‘˜ = 𝑖 β†’ if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ) = ℝ)
1614, 15sseqtrrid 4001 . . . . . . . . . . . . . . . 16 (Β¬ π‘˜ = 𝑖 β†’ (-∞(,)(π΅β€˜π‘˜)) βŠ† if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
1713, 16pm2.61i 182 . . . . . . . . . . . . . . 15 (-∞(,)(π΅β€˜π‘˜)) βŠ† if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ)
18 mnfxr 11220 . . . . . . . . . . . . . . . . 17 -∞ ∈ ℝ*
1918a1i 11 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ π‘˜ ∈ 𝑋) β†’ -∞ ∈ ℝ*)
20 hspdifhsp.b . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐡:π‘‹βŸΆβ„)
2120ffvelcdmda 7039 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘˜ ∈ 𝑋) β†’ (π΅β€˜π‘˜) ∈ ℝ)
2221rexrd 11213 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘˜ ∈ 𝑋) β†’ (π΅β€˜π‘˜) ∈ ℝ*)
2322adantlr 714 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ π‘˜ ∈ 𝑋) β†’ (π΅β€˜π‘˜) ∈ ℝ*)
24 hspdifhsp.a . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐴:π‘‹βŸΆβ„)
2524ffvelcdmda 7039 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘˜ ∈ 𝑋) β†’ (π΄β€˜π‘˜) ∈ ℝ)
26 icossre 13354 . . . . . . . . . . . . . . . . . . 19 (((π΄β€˜π‘˜) ∈ ℝ ∧ (π΅β€˜π‘˜) ∈ ℝ*) β†’ ((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜)) βŠ† ℝ)
2725, 22, 26syl2anc 585 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘˜ ∈ 𝑋) β†’ ((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜)) βŠ† ℝ)
2827adantlr 714 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ π‘˜ ∈ 𝑋) β†’ ((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜)) βŠ† ℝ)
29 simpl 484 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) ∧ π‘˜ ∈ 𝑋) β†’ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)))
30 simpr 486 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) ∧ π‘˜ ∈ 𝑋) β†’ π‘˜ ∈ 𝑋)
31 fveq2 6846 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = π‘˜ β†’ (π΄β€˜π‘–) = (π΄β€˜π‘˜))
32 fveq2 6846 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = π‘˜ β†’ (π΅β€˜π‘–) = (π΅β€˜π‘˜))
3331, 32oveq12d 7379 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = π‘˜ β†’ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) = ((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜)))
3433fvixp 8846 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ ((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜)))
3529, 30, 34syl2anc 585 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ ((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜)))
3635adantll 713 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ ((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜)))
3728, 36sseldd 3949 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ ℝ)
3837mnfltd 13053 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ π‘˜ ∈ 𝑋) β†’ -∞ < (π‘“β€˜π‘˜))
3925rexrd 11213 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘˜ ∈ 𝑋) β†’ (π΄β€˜π‘˜) ∈ ℝ*)
4039adantlr 714 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ π‘˜ ∈ 𝑋) β†’ (π΄β€˜π‘˜) ∈ ℝ*)
41 icoltub 43836 . . . . . . . . . . . . . . . . 17 (((π΄β€˜π‘˜) ∈ ℝ* ∧ (π΅β€˜π‘˜) ∈ ℝ* ∧ (π‘“β€˜π‘˜) ∈ ((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))) β†’ (π‘“β€˜π‘˜) < (π΅β€˜π‘˜))
4240, 23, 36, 41syl3anc 1372 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) < (π΅β€˜π‘˜))
4319, 23, 37, 38, 42eliood 43826 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ (-∞(,)(π΅β€˜π‘˜)))
4417, 43sselid 3946 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
4544adantlr 714 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
4645ralrimiva 3140 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
477, 46jca 513 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (𝑓 Fn 𝑋 ∧ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ)))
48 vex 3451 . . . . . . . . . . . 12 𝑓 ∈ V
4948elixp 8848 . . . . . . . . . . 11 (𝑓 ∈ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ) ↔ (𝑓 Fn 𝑋 ∧ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ)))
5047, 49sylibr 233 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
51 hspdifhsp.h . . . . . . . . . . . . 13 𝐻 = (π‘₯ ∈ Fin ↦ (𝑙 ∈ π‘₯, 𝑦 ∈ ℝ ↦ X𝑖 ∈ π‘₯ if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ)))
52 equequ1 2029 . . . . . . . . . . . . . . . . . 18 (𝑖 = π‘˜ β†’ (𝑖 = 𝑙 ↔ π‘˜ = 𝑙))
5352ifbid 4513 . . . . . . . . . . . . . . . . 17 (𝑖 = π‘˜ β†’ if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = if(π‘˜ = 𝑙, (-∞(,)𝑦), ℝ))
5453cbvixpv 8859 . . . . . . . . . . . . . . . 16 X𝑖 ∈ π‘₯ if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = Xπ‘˜ ∈ π‘₯ if(π‘˜ = 𝑙, (-∞(,)𝑦), ℝ)
5554a1i 11 . . . . . . . . . . . . . . 15 ((𝑙 ∈ π‘₯ ∧ 𝑦 ∈ ℝ) β†’ X𝑖 ∈ π‘₯ if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = Xπ‘˜ ∈ π‘₯ if(π‘˜ = 𝑙, (-∞(,)𝑦), ℝ))
5655mpoeq3ia 7439 . . . . . . . . . . . . . 14 (𝑙 ∈ π‘₯, 𝑦 ∈ ℝ ↦ X𝑖 ∈ π‘₯ if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ)) = (𝑙 ∈ π‘₯, 𝑦 ∈ ℝ ↦ Xπ‘˜ ∈ π‘₯ if(π‘˜ = 𝑙, (-∞(,)𝑦), ℝ))
5756mpteq2i 5214 . . . . . . . . . . . . 13 (π‘₯ ∈ Fin ↦ (𝑙 ∈ π‘₯, 𝑦 ∈ ℝ ↦ X𝑖 ∈ π‘₯ if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ))) = (π‘₯ ∈ Fin ↦ (𝑙 ∈ π‘₯, 𝑦 ∈ ℝ ↦ Xπ‘˜ ∈ π‘₯ if(π‘˜ = 𝑙, (-∞(,)𝑦), ℝ)))
5851, 57eqtri 2761 . . . . . . . . . . . 12 𝐻 = (π‘₯ ∈ Fin ↦ (𝑙 ∈ π‘₯, 𝑦 ∈ ℝ ↦ Xπ‘˜ ∈ π‘₯ if(π‘˜ = 𝑙, (-∞(,)𝑦), ℝ)))
59 hspdifhsp.x . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑋 ∈ Fin)
6059adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ 𝑋 ∈ Fin)
61 simpr 486 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ 𝑖 ∈ 𝑋)
6220adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ 𝐡:π‘‹βŸΆβ„)
6362, 61ffvelcdmd 7040 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (π΅β€˜π‘–) ∈ ℝ)
6458, 60, 61, 63hspval 44940 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) = Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
6564adantlr 714 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) = Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
6650, 65eleqtrrd 2837 . . . . . . . . 9 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)))
6718a1i 11 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) β†’ -∞ ∈ ℝ*)
6824adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ 𝐴:π‘‹βŸΆβ„)
6968, 61ffvelcdmd 7040 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (π΄β€˜π‘–) ∈ ℝ)
7069rexrd 11213 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (π΄β€˜π‘–) ∈ ℝ*)
7170adantr 482 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) β†’ (π΄β€˜π‘–) ∈ ℝ*)
72 simpr 486 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) β†’ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))
7358, 60, 61, 69hspval 44940 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)) = Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ))
7473adantr 482 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) β†’ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)) = Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ))
7572, 74eleqtrd 2836 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) β†’ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ))
7661adantr 482 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) β†’ 𝑖 ∈ 𝑋)
77 iftrue 4496 . . . . . . . . . . . . . 14 (π‘˜ = 𝑖 β†’ if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ) = (-∞(,)(π΄β€˜π‘–)))
7877fvixp 8846 . . . . . . . . . . . . 13 ((𝑓 ∈ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ (-∞(,)(π΄β€˜π‘–)))
7975, 76, 78syl2anc 585 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) β†’ (π‘“β€˜π‘–) ∈ (-∞(,)(π΄β€˜π‘–)))
80 iooltub 43838 . . . . . . . . . . . 12 ((-∞ ∈ ℝ* ∧ (π΄β€˜π‘–) ∈ ℝ* ∧ (π‘“β€˜π‘–) ∈ (-∞(,)(π΄β€˜π‘–))) β†’ (π‘“β€˜π‘–) < (π΄β€˜π‘–))
8167, 71, 79, 80syl3anc 1372 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) β†’ (π‘“β€˜π‘–) < (π΄β€˜π‘–))
8281adantllr 718 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) β†’ (π‘“β€˜π‘–) < (π΄β€˜π‘–))
8370adantlr 714 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (π΄β€˜π‘–) ∈ ℝ*)
8463rexrd 11213 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (π΅β€˜π‘–) ∈ ℝ*)
8584adantlr 714 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (π΅β€˜π‘–) ∈ ℝ*)
8648elixp 8848 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) ↔ (𝑓 Fn 𝑋 ∧ βˆ€π‘– ∈ 𝑋 (π‘“β€˜π‘–) ∈ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))))
8786biimpi 215 . . . . . . . . . . . . . . . 16 (𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) β†’ (𝑓 Fn 𝑋 ∧ βˆ€π‘– ∈ 𝑋 (π‘“β€˜π‘–) ∈ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))))
8887simprd 497 . . . . . . . . . . . . . . 15 (𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) β†’ βˆ€π‘– ∈ 𝑋 (π‘“β€˜π‘–) ∈ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)))
89 rspa 3230 . . . . . . . . . . . . . . 15 ((βˆ€π‘– ∈ 𝑋 (π‘“β€˜π‘–) ∈ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)))
9088, 89sylan 581 . . . . . . . . . . . . . 14 ((𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)))
9190adantll 713 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)))
92 icogelb 13324 . . . . . . . . . . . . 13 (((π΄β€˜π‘–) ∈ ℝ* ∧ (π΅β€˜π‘–) ∈ ℝ* ∧ (π‘“β€˜π‘–) ∈ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) β†’ (π΄β€˜π‘–) ≀ (π‘“β€˜π‘–))
9383, 85, 91, 92syl3anc 1372 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (π΄β€˜π‘–) ≀ (π‘“β€˜π‘–))
9469adantlr 714 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (π΄β€˜π‘–) ∈ ℝ)
95 icossre 13354 . . . . . . . . . . . . . . . 16 (((π΄β€˜π‘–) ∈ ℝ ∧ (π΅β€˜π‘–) ∈ ℝ*) β†’ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) βŠ† ℝ)
9669, 84, 95syl2anc 585 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) βŠ† ℝ)
9796adantlr 714 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) βŠ† ℝ)
9897, 91sseldd 3949 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ℝ)
9994, 98lenltd 11309 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ ((π΄β€˜π‘–) ≀ (π‘“β€˜π‘–) ↔ Β¬ (π‘“β€˜π‘–) < (π΄β€˜π‘–)))
10093, 99mpbid 231 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ Β¬ (π‘“β€˜π‘–) < (π΄β€˜π‘–))
101100adantr 482 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) β†’ Β¬ (π‘“β€˜π‘–) < (π΄β€˜π‘–))
10282, 101pm2.65da 816 . . . . . . . . 9 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ Β¬ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))
10366, 102eldifd 3925 . . . . . . . 8 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))))
104103ex 414 . . . . . . 7 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) β†’ (𝑖 ∈ 𝑋 β†’ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))))
1055, 104ralrimi 3239 . . . . . 6 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) β†’ βˆ€π‘– ∈ 𝑋 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))))
106 eliin 4963 . . . . . . 7 (𝑓 ∈ V β†’ (𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) ↔ βˆ€π‘– ∈ 𝑋 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))))
10748, 106ax-mp 5 . . . . . 6 (𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) ↔ βˆ€π‘– ∈ 𝑋 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))))
108105, 107sylibr 233 . . . . 5 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) β†’ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))))
109108ex 414 . . . 4 (πœ‘ β†’ (𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) β†’ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))))
110 hspdifhsp.n . . . . . . . . . 10 (πœ‘ β†’ 𝑋 β‰  βˆ…)
111 n0 4310 . . . . . . . . . . 11 (𝑋 β‰  βˆ… ↔ βˆƒπ‘˜ π‘˜ ∈ 𝑋)
112111biimpi 215 . . . . . . . . . 10 (𝑋 β‰  βˆ… β†’ βˆƒπ‘˜ π‘˜ ∈ 𝑋)
113110, 112syl 17 . . . . . . . . 9 (πœ‘ β†’ βˆƒπ‘˜ π‘˜ ∈ 𝑋)
114113adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) β†’ βˆƒπ‘˜ π‘˜ ∈ 𝑋)
115 simpl 484 . . . . . . . . . . . . . . 15 ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) ∧ π‘˜ ∈ 𝑋) β†’ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))))
116 simpr 486 . . . . . . . . . . . . . . 15 ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) ∧ π‘˜ ∈ 𝑋) β†’ π‘˜ ∈ 𝑋)
117 id 22 . . . . . . . . . . . . . . . . . 18 (𝑖 = π‘˜ β†’ 𝑖 = π‘˜)
118117, 32oveq12d 7379 . . . . . . . . . . . . . . . . 17 (𝑖 = π‘˜ β†’ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) = (π‘˜(π»β€˜π‘‹)(π΅β€˜π‘˜)))
119117, 31oveq12d 7379 . . . . . . . . . . . . . . . . 17 (𝑖 = π‘˜ β†’ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)) = (π‘˜(π»β€˜π‘‹)(π΄β€˜π‘˜)))
120118, 119difeq12d 4087 . . . . . . . . . . . . . . . 16 (𝑖 = π‘˜ β†’ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) = ((π‘˜(π»β€˜π‘‹)(π΅β€˜π‘˜)) βˆ– (π‘˜(π»β€˜π‘‹)(π΄β€˜π‘˜))))
121120eleq2d 2820 . . . . . . . . . . . . . . 15 (𝑖 = π‘˜ β†’ (𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) ↔ 𝑓 ∈ ((π‘˜(π»β€˜π‘‹)(π΅β€˜π‘˜)) βˆ– (π‘˜(π»β€˜π‘‹)(π΄β€˜π‘˜)))))
122115, 116, 121eliind 43371 . . . . . . . . . . . . . 14 ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) ∧ π‘˜ ∈ 𝑋) β†’ 𝑓 ∈ ((π‘˜(π»β€˜π‘‹)(π΅β€˜π‘˜)) βˆ– (π‘˜(π»β€˜π‘‹)(π΄β€˜π‘˜))))
123122eldifad 3926 . . . . . . . . . . . . 13 ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) ∧ π‘˜ ∈ 𝑋) β†’ 𝑓 ∈ (π‘˜(π»β€˜π‘‹)(π΅β€˜π‘˜)))
124123adantll 713 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ π‘˜ ∈ 𝑋) β†’ 𝑓 ∈ (π‘˜(π»β€˜π‘‹)(π΅β€˜π‘˜)))
125 equequ1 2029 . . . . . . . . . . . . . . . . . . 19 (𝑖 = β„Ž β†’ (𝑖 = 𝑙 ↔ β„Ž = 𝑙))
126125ifbid 4513 . . . . . . . . . . . . . . . . . 18 (𝑖 = β„Ž β†’ if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = if(β„Ž = 𝑙, (-∞(,)𝑦), ℝ))
127126cbvixpv 8859 . . . . . . . . . . . . . . . . 17 X𝑖 ∈ π‘₯ if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = Xβ„Ž ∈ π‘₯ if(β„Ž = 𝑙, (-∞(,)𝑦), ℝ)
128127a1i 11 . . . . . . . . . . . . . . . 16 ((𝑙 ∈ π‘₯ ∧ 𝑦 ∈ ℝ) β†’ X𝑖 ∈ π‘₯ if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = Xβ„Ž ∈ π‘₯ if(β„Ž = 𝑙, (-∞(,)𝑦), ℝ))
129128mpoeq3ia 7439 . . . . . . . . . . . . . . 15 (𝑙 ∈ π‘₯, 𝑦 ∈ ℝ ↦ X𝑖 ∈ π‘₯ if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ)) = (𝑙 ∈ π‘₯, 𝑦 ∈ ℝ ↦ Xβ„Ž ∈ π‘₯ if(β„Ž = 𝑙, (-∞(,)𝑦), ℝ))
130129mpteq2i 5214 . . . . . . . . . . . . . 14 (π‘₯ ∈ Fin ↦ (𝑙 ∈ π‘₯, 𝑦 ∈ ℝ ↦ X𝑖 ∈ π‘₯ if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ))) = (π‘₯ ∈ Fin ↦ (𝑙 ∈ π‘₯, 𝑦 ∈ ℝ ↦ Xβ„Ž ∈ π‘₯ if(β„Ž = 𝑙, (-∞(,)𝑦), ℝ)))
13151, 130eqtri 2761 . . . . . . . . . . . . 13 𝐻 = (π‘₯ ∈ Fin ↦ (𝑙 ∈ π‘₯, 𝑦 ∈ ℝ ↦ Xβ„Ž ∈ π‘₯ if(β„Ž = 𝑙, (-∞(,)𝑦), ℝ)))
13259ad2antrr 725 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ π‘˜ ∈ 𝑋) β†’ 𝑋 ∈ Fin)
133 simpr 486 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ π‘˜ ∈ 𝑋) β†’ π‘˜ ∈ 𝑋)
13421adantlr 714 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ π‘˜ ∈ 𝑋) β†’ (π΅β€˜π‘˜) ∈ ℝ)
135131, 132, 133, 134hspval 44940 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘˜(π»β€˜π‘‹)(π΅β€˜π‘˜)) = Xβ„Ž ∈ 𝑋 if(β„Ž = π‘˜, (-∞(,)(π΅β€˜π‘˜)), ℝ))
136124, 135eleqtrd 2836 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ π‘˜ ∈ 𝑋) β†’ 𝑓 ∈ Xβ„Ž ∈ 𝑋 if(β„Ž = π‘˜, (-∞(,)(π΅β€˜π‘˜)), ℝ))
137 ixpfn 8847 . . . . . . . . . . 11 (𝑓 ∈ Xβ„Ž ∈ 𝑋 if(β„Ž = π‘˜, (-∞(,)(π΅β€˜π‘˜)), ℝ) β†’ 𝑓 Fn 𝑋)
138136, 137syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ π‘˜ ∈ 𝑋) β†’ 𝑓 Fn 𝑋)
139138ex 414 . . . . . . . . 9 ((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) β†’ (π‘˜ ∈ 𝑋 β†’ 𝑓 Fn 𝑋))
140139exlimdv 1937 . . . . . . . 8 ((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) β†’ (βˆƒπ‘˜ π‘˜ ∈ 𝑋 β†’ 𝑓 Fn 𝑋))
141114, 140mpd 15 . . . . . . 7 ((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) β†’ 𝑓 Fn 𝑋)
142 nfii1 4993 . . . . . . . . . 10 β„²π‘–βˆ© 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))
1432, 142nfel 2918 . . . . . . . . 9 Ⅎ𝑖 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))
1441, 143nfan 1903 . . . . . . . 8 Ⅎ𝑖(πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))))
145 simpll 766 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ πœ‘)
146107biimpi 215 . . . . . . . . . . . . 13 (𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) β†’ βˆ€π‘– ∈ 𝑋 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))))
147146adantr 482 . . . . . . . . . . . 12 ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ βˆ€π‘– ∈ 𝑋 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))))
148 simpr 486 . . . . . . . . . . . 12 ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑖 ∈ 𝑋)
149 rspa 3230 . . . . . . . . . . . 12 ((βˆ€π‘– ∈ 𝑋 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))))
150147, 148, 149syl2anc 585 . . . . . . . . . . 11 ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))))
151150adantll 713 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))))
152 simpr 486 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑖 ∈ 𝑋)
15370adantlr 714 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ (π΄β€˜π‘–) ∈ ℝ*)
15484adantlr 714 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ (π΅β€˜π‘–) ∈ ℝ*)
155 simpll 766 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ πœ‘)
156 eldifi 4090 . . . . . . . . . . . . . 14 (𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) β†’ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)))
157156ad2antlr 726 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)))
158 simpr 486 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑖 ∈ 𝑋)
159 ioossre 13334 . . . . . . . . . . . . . 14 (-∞(,)(π΅β€˜π‘–)) βŠ† ℝ
160 simplr 768 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)))
16164adantlr 714 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) = Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
162160, 161eleqtrd 2836 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
163 simpr 486 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑖 ∈ 𝑋)
16410fvixp 8846 . . . . . . . . . . . . . . 15 ((𝑓 ∈ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ (-∞(,)(π΅β€˜π‘–)))
165162, 163, 164syl2anc 585 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ (-∞(,)(π΅β€˜π‘–)))
166159, 165sselid 3946 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ℝ)
167155, 157, 158, 166syl21anc 837 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ℝ)
168167rexrd 11213 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ℝ*)
169 simpl 484 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) β†’ πœ‘)
170156adantl 483 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) β†’ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)))
171169, 170jca 513 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) β†’ (πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))))
172171ad2antrr 725 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ (πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))))
173 simplr 768 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ 𝑖 ∈ 𝑋)
174 simpr 486 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ (π‘“β€˜π‘–) < (π΄β€˜π‘–))
175 ixpfn 8847 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ) β†’ 𝑓 Fn 𝑋)
176162, 175syl 17 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑓 Fn 𝑋)
177176adantr 482 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ 𝑓 Fn 𝑋)
178 fveq2 6846 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘˜ = 𝑖 β†’ (π‘“β€˜π‘˜) = (π‘“β€˜π‘–))
179178adantl 483 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) ∧ π‘˜ = 𝑖) β†’ (π‘“β€˜π‘˜) = (π‘“β€˜π‘–))
18018a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ -∞ ∈ ℝ*)
18170ad4ant13 750 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ (π΄β€˜π‘–) ∈ ℝ*)
182166adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ (π‘“β€˜π‘–) ∈ ℝ)
183182mnfltd 13053 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ -∞ < (π‘“β€˜π‘–))
184 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ (π‘“β€˜π‘–) < (π΄β€˜π‘–))
185180, 181, 182, 183, 184eliood 43826 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ (π‘“β€˜π‘–) ∈ (-∞(,)(π΄β€˜π‘–)))
186185adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) ∧ π‘˜ = 𝑖) β†’ (π‘“β€˜π‘–) ∈ (-∞(,)(π΄β€˜π‘–)))
187179, 186eqeltrd 2834 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) ∧ π‘˜ = 𝑖) β†’ (π‘“β€˜π‘˜) ∈ (-∞(,)(π΄β€˜π‘–)))
188187adantlr 714 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝑖) β†’ (π‘“β€˜π‘˜) ∈ (-∞(,)(π΄β€˜π‘–)))
18977eqcomd 2739 . . . . . . . . . . . . . . . . . . . . 21 (π‘˜ = 𝑖 β†’ (-∞(,)(π΄β€˜π‘–)) = if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ))
190189adantl 483 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝑖) β†’ (-∞(,)(π΄β€˜π‘–)) = if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ))
191188, 190eleqtrd 2836 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝑖) β†’ (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ))
19210, 159eqsstrdi 4002 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘˜ = 𝑖 β†’ if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ) βŠ† ℝ)
193 ssid 3970 . . . . . . . . . . . . . . . . . . . . . . . . 25 ℝ βŠ† ℝ
19415, 193eqsstrdi 4002 . . . . . . . . . . . . . . . . . . . . . . . 24 (Β¬ π‘˜ = 𝑖 β†’ if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ) βŠ† ℝ)
195192, 194pm2.61i 182 . . . . . . . . . . . . . . . . . . . . . . 23 if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ) βŠ† ℝ
196162adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ π‘˜ ∈ 𝑋) β†’ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
197 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ π‘˜ ∈ 𝑋) β†’ π‘˜ ∈ 𝑋)
198 fvixp2 43511 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓 ∈ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
199196, 197, 198syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
200195, 199sselid 3946 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ ℝ)
201200adantr 482 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ π‘˜ ∈ 𝑋) ∧ Β¬ π‘˜ = 𝑖) β†’ (π‘“β€˜π‘˜) ∈ ℝ)
202 iffalse 4499 . . . . . . . . . . . . . . . . . . . . . . 23 (Β¬ π‘˜ = 𝑖 β†’ if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ) = ℝ)
203202eqcomd 2739 . . . . . . . . . . . . . . . . . . . . . 22 (Β¬ π‘˜ = 𝑖 β†’ ℝ = if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ))
204203adantl 483 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ π‘˜ ∈ 𝑋) ∧ Β¬ π‘˜ = 𝑖) β†’ ℝ = if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ))
205201, 204eleqtrd 2836 . . . . . . . . . . . . . . . . . . . 20 (((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ π‘˜ ∈ 𝑋) ∧ Β¬ π‘˜ = 𝑖) β†’ (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ))
206205adantllr 718 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) ∧ π‘˜ ∈ 𝑋) ∧ Β¬ π‘˜ = 𝑖) β†’ (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ))
207191, 206pm2.61dan 812 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ))
208207ralrimiva 3140 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ))
209177, 208jca 513 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ (𝑓 Fn 𝑋 ∧ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ)))
21048elixp 8848 . . . . . . . . . . . . . . . 16 (𝑓 ∈ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ) ↔ (𝑓 Fn 𝑋 ∧ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ)))
211209, 210sylibr 233 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ))
21273eqcomd 2739 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ) = (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))
213212ad4ant13 750 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ) = (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))
214211, 213eleqtrd 2836 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))
215172, 173, 174, 214syl21anc 837 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))
216 eldifn 4091 . . . . . . . . . . . . . 14 (𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) β†’ Β¬ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))
217216ad3antlr 730 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ Β¬ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))
218215, 217pm2.65da 816 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ Β¬ (π‘“β€˜π‘–) < (π΄β€˜π‘–))
219155, 158, 69syl2anc 585 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ (π΄β€˜π‘–) ∈ ℝ)
220219, 167lenltd 11309 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ ((π΄β€˜π‘–) ≀ (π‘“β€˜π‘–) ↔ Β¬ (π‘“β€˜π‘–) < (π΄β€˜π‘–)))
221218, 220mpbird 257 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ (π΄β€˜π‘–) ≀ (π‘“β€˜π‘–))
22218a1i 11 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ -∞ ∈ ℝ*)
22384adantlr 714 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (π΅β€˜π‘–) ∈ ℝ*)
224 iooltub 43838 . . . . . . . . . . . . 13 ((-∞ ∈ ℝ* ∧ (π΅β€˜π‘–) ∈ ℝ* ∧ (π‘“β€˜π‘–) ∈ (-∞(,)(π΅β€˜π‘–))) β†’ (π‘“β€˜π‘–) < (π΅β€˜π‘–))
225222, 223, 165, 224syl3anc 1372 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) < (π΅β€˜π‘–))
226155, 157, 158, 225syl21anc 837 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) < (π΅β€˜π‘–))
227153, 154, 168, 221, 226elicod 13323 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)))
228145, 151, 152, 227syl21anc 837 . . . . . . . . 9 (((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)))
229228ex 414 . . . . . . . 8 ((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) β†’ (𝑖 ∈ 𝑋 β†’ (π‘“β€˜π‘–) ∈ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))))
230144, 229ralrimi 3239 . . . . . . 7 ((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) β†’ βˆ€π‘– ∈ 𝑋 (π‘“β€˜π‘–) ∈ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)))
231141, 230jca 513 . . . . . 6 ((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) β†’ (𝑓 Fn 𝑋 ∧ βˆ€π‘– ∈ 𝑋 (π‘“β€˜π‘–) ∈ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))))
232231, 86sylibr 233 . . . . 5 ((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) β†’ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)))
233232ex 414 . . . 4 (πœ‘ β†’ (𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) β†’ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))))
234109, 233impbid 211 . . 3 (πœ‘ β†’ (𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) ↔ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))))
235234alrimiv 1931 . 2 (πœ‘ β†’ βˆ€π‘“(𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) ↔ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))))
236 dfcleq 2726 . 2 (X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) = ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) ↔ βˆ€π‘“(𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) ↔ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))))
237235, 236sylibr 233 1 (πœ‘ β†’ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) = ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397  βˆ€wal 1540   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107   β‰  wne 2940  βˆ€wral 3061  Vcvv 3447   βˆ– cdif 3911   βŠ† wss 3914  βˆ…c0 4286  ifcif 4490  βˆ© ciin 4959   class class class wbr 5109   ↦ cmpt 5192   Fn wfn 6495  βŸΆwf 6496  β€˜cfv 6500  (class class class)co 7361   ∈ cmpo 7363  Xcixp 8841  Fincfn 8889  β„cr 11058  -∞cmnf 11195  β„*cxr 11196   < clt 11197   ≀ cle 11198  (,)cioo 13273  [,)cico 13275
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5246  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-cnex 11115  ax-resscn 11116  ax-pre-lttri 11133  ax-pre-lttrn 11134
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-iun 4960  df-iin 4961  df-br 5110  df-opab 5172  df-mpt 5193  df-id 5535  df-po 5549  df-so 5550  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7364  df-oprab 7365  df-mpo 7366  df-1st 7925  df-2nd 7926  df-er 8654  df-ixp 8842  df-en 8890  df-dom 8891  df-sdom 8892  df-pnf 11199  df-mnf 11200  df-xr 11201  df-ltxr 11202  df-le 11203  df-ioo 13277  df-ico 13279
This theorem is referenced by:  hoimbllem  44961
  Copyright terms: Public domain W3C validator