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 45322
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 1917 . . . . . . . 8 β„²π‘–πœ‘
2 nfcv 2903 . . . . . . . . 9 Ⅎ𝑖𝑓
3 nfixp1 8911 . . . . . . . . 9 Ⅎ𝑖X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))
42, 3nfel 2917 . . . . . . . 8 Ⅎ𝑖 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))
51, 4nfan 1902 . . . . . . 7 Ⅎ𝑖(πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)))
6 ixpfn 8896 . . . . . . . . . . . . 13 (𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) β†’ 𝑓 Fn 𝑋)
76ad2antlr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑓 Fn 𝑋)
8 fveq2 6891 . . . . . . . . . . . . . . . . . . 19 (π‘˜ = 𝑖 β†’ (π΅β€˜π‘˜) = (π΅β€˜π‘–))
98oveq2d 7424 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑖 β†’ (-∞(,)(π΅β€˜π‘˜)) = (-∞(,)(π΅β€˜π‘–)))
10 iftrue 4534 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑖 β†’ if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ) = (-∞(,)(π΅β€˜π‘–)))
119, 10eqtr4d 2775 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑖 β†’ (-∞(,)(π΅β€˜π‘˜)) = if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
12 eqimss 4040 . . . . . . . . . . . . . . . . 17 ((-∞(,)(π΅β€˜π‘˜)) = if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ) β†’ (-∞(,)(π΅β€˜π‘˜)) βŠ† if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
1311, 12syl 17 . . . . . . . . . . . . . . . 16 (π‘˜ = 𝑖 β†’ (-∞(,)(π΅β€˜π‘˜)) βŠ† if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
14 ioossre 13384 . . . . . . . . . . . . . . . . 17 (-∞(,)(π΅β€˜π‘˜)) βŠ† ℝ
15 iffalse 4537 . . . . . . . . . . . . . . . . 17 (Β¬ π‘˜ = 𝑖 β†’ if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ) = ℝ)
1614, 15sseqtrrid 4035 . . . . . . . . . . . . . . . 16 (Β¬ π‘˜ = 𝑖 β†’ (-∞(,)(π΅β€˜π‘˜)) βŠ† if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
1713, 16pm2.61i 182 . . . . . . . . . . . . . . 15 (-∞(,)(π΅β€˜π‘˜)) βŠ† if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ)
18 mnfxr 11270 . . . . . . . . . . . . . . . . 17 -∞ ∈ ℝ*
1918a1i 11 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ π‘˜ ∈ 𝑋) β†’ -∞ ∈ ℝ*)
20 hspdifhsp.b . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐡:π‘‹βŸΆβ„)
2120ffvelcdmda 7086 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘˜ ∈ 𝑋) β†’ (π΅β€˜π‘˜) ∈ ℝ)
2221rexrd 11263 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘˜ ∈ 𝑋) β†’ (π΅β€˜π‘˜) ∈ ℝ*)
2322adantlr 713 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ π‘˜ ∈ 𝑋) β†’ (π΅β€˜π‘˜) ∈ ℝ*)
24 hspdifhsp.a . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐴:π‘‹βŸΆβ„)
2524ffvelcdmda 7086 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘˜ ∈ 𝑋) β†’ (π΄β€˜π‘˜) ∈ ℝ)
26 icossre 13404 . . . . . . . . . . . . . . . . . . 19 (((π΄β€˜π‘˜) ∈ ℝ ∧ (π΅β€˜π‘˜) ∈ ℝ*) β†’ ((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜)) βŠ† ℝ)
2725, 22, 26syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘˜ ∈ 𝑋) β†’ ((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜)) βŠ† ℝ)
2827adantlr 713 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ π‘˜ ∈ 𝑋) β†’ ((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜)) βŠ† ℝ)
29 simpl 483 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) ∧ π‘˜ ∈ 𝑋) β†’ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)))
30 simpr 485 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) ∧ π‘˜ ∈ 𝑋) β†’ π‘˜ ∈ 𝑋)
31 fveq2 6891 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = π‘˜ β†’ (π΄β€˜π‘–) = (π΄β€˜π‘˜))
32 fveq2 6891 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = π‘˜ β†’ (π΅β€˜π‘–) = (π΅β€˜π‘˜))
3331, 32oveq12d 7426 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = π‘˜ β†’ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) = ((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜)))
3433fvixp 8895 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ ((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜)))
3529, 30, 34syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ ((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜)))
3635adantll 712 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ ((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜)))
3728, 36sseldd 3983 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ ℝ)
3837mnfltd 13103 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ π‘˜ ∈ 𝑋) β†’ -∞ < (π‘“β€˜π‘˜))
3925rexrd 11263 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘˜ ∈ 𝑋) β†’ (π΄β€˜π‘˜) ∈ ℝ*)
4039adantlr 713 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ π‘˜ ∈ 𝑋) β†’ (π΄β€˜π‘˜) ∈ ℝ*)
41 icoltub 44211 . . . . . . . . . . . . . . . . 17 (((π΄β€˜π‘˜) ∈ ℝ* ∧ (π΅β€˜π‘˜) ∈ ℝ* ∧ (π‘“β€˜π‘˜) ∈ ((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))) β†’ (π‘“β€˜π‘˜) < (π΅β€˜π‘˜))
4240, 23, 36, 41syl3anc 1371 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) < (π΅β€˜π‘˜))
4319, 23, 37, 38, 42eliood 44201 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ (-∞(,)(π΅β€˜π‘˜)))
4417, 43sselid 3980 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
4544adantlr 713 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
4645ralrimiva 3146 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
477, 46jca 512 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (𝑓 Fn 𝑋 ∧ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ)))
48 vex 3478 . . . . . . . . . . . 12 𝑓 ∈ V
4948elixp 8897 . . . . . . . . . . 11 (𝑓 ∈ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ) ↔ (𝑓 Fn 𝑋 ∧ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ)))
5047, 49sylibr 233 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
51 hspdifhsp.h . . . . . . . . . . . . 13 𝐻 = (π‘₯ ∈ Fin ↦ (𝑙 ∈ π‘₯, 𝑦 ∈ ℝ ↦ X𝑖 ∈ π‘₯ if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ)))
52 equequ1 2028 . . . . . . . . . . . . . . . . . 18 (𝑖 = π‘˜ β†’ (𝑖 = 𝑙 ↔ π‘˜ = 𝑙))
5352ifbid 4551 . . . . . . . . . . . . . . . . 17 (𝑖 = π‘˜ β†’ if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = if(π‘˜ = 𝑙, (-∞(,)𝑦), ℝ))
5453cbvixpv 8908 . . . . . . . . . . . . . . . 16 X𝑖 ∈ π‘₯ if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = Xπ‘˜ ∈ π‘₯ if(π‘˜ = 𝑙, (-∞(,)𝑦), ℝ)
5554a1i 11 . . . . . . . . . . . . . . 15 ((𝑙 ∈ π‘₯ ∧ 𝑦 ∈ ℝ) β†’ X𝑖 ∈ π‘₯ if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = Xπ‘˜ ∈ π‘₯ if(π‘˜ = 𝑙, (-∞(,)𝑦), ℝ))
5655mpoeq3ia 7486 . . . . . . . . . . . . . 14 (𝑙 ∈ π‘₯, 𝑦 ∈ ℝ ↦ X𝑖 ∈ π‘₯ if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ)) = (𝑙 ∈ π‘₯, 𝑦 ∈ ℝ ↦ Xπ‘˜ ∈ π‘₯ if(π‘˜ = 𝑙, (-∞(,)𝑦), ℝ))
5756mpteq2i 5253 . . . . . . . . . . . . 13 (π‘₯ ∈ Fin ↦ (𝑙 ∈ π‘₯, 𝑦 ∈ ℝ ↦ X𝑖 ∈ π‘₯ if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ))) = (π‘₯ ∈ Fin ↦ (𝑙 ∈ π‘₯, 𝑦 ∈ ℝ ↦ Xπ‘˜ ∈ π‘₯ if(π‘˜ = 𝑙, (-∞(,)𝑦), ℝ)))
5851, 57eqtri 2760 . . . . . . . . . . . 12 𝐻 = (π‘₯ ∈ Fin ↦ (𝑙 ∈ π‘₯, 𝑦 ∈ ℝ ↦ Xπ‘˜ ∈ π‘₯ if(π‘˜ = 𝑙, (-∞(,)𝑦), ℝ)))
59 hspdifhsp.x . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑋 ∈ Fin)
6059adantr 481 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ 𝑋 ∈ Fin)
61 simpr 485 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ 𝑖 ∈ 𝑋)
6220adantr 481 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ 𝐡:π‘‹βŸΆβ„)
6362, 61ffvelcdmd 7087 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (π΅β€˜π‘–) ∈ ℝ)
6458, 60, 61, 63hspval 45315 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) = Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
6564adantlr 713 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) = Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
6650, 65eleqtrrd 2836 . . . . . . . . 9 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)))
6718a1i 11 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) β†’ -∞ ∈ ℝ*)
6824adantr 481 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ 𝐴:π‘‹βŸΆβ„)
6968, 61ffvelcdmd 7087 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (π΄β€˜π‘–) ∈ ℝ)
7069rexrd 11263 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (π΄β€˜π‘–) ∈ ℝ*)
7170adantr 481 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) β†’ (π΄β€˜π‘–) ∈ ℝ*)
72 simpr 485 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) β†’ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))
7358, 60, 61, 69hspval 45315 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)) = Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ))
7473adantr 481 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) β†’ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)) = Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ))
7572, 74eleqtrd 2835 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) β†’ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ))
7661adantr 481 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) β†’ 𝑖 ∈ 𝑋)
77 iftrue 4534 . . . . . . . . . . . . . 14 (π‘˜ = 𝑖 β†’ if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ) = (-∞(,)(π΄β€˜π‘–)))
7877fvixp 8895 . . . . . . . . . . . . 13 ((𝑓 ∈ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ (-∞(,)(π΄β€˜π‘–)))
7975, 76, 78syl2anc 584 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) β†’ (π‘“β€˜π‘–) ∈ (-∞(,)(π΄β€˜π‘–)))
80 iooltub 44213 . . . . . . . . . . . 12 ((-∞ ∈ ℝ* ∧ (π΄β€˜π‘–) ∈ ℝ* ∧ (π‘“β€˜π‘–) ∈ (-∞(,)(π΄β€˜π‘–))) β†’ (π‘“β€˜π‘–) < (π΄β€˜π‘–))
8167, 71, 79, 80syl3anc 1371 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) β†’ (π‘“β€˜π‘–) < (π΄β€˜π‘–))
8281adantllr 717 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) β†’ (π‘“β€˜π‘–) < (π΄β€˜π‘–))
8370adantlr 713 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (π΄β€˜π‘–) ∈ ℝ*)
8463rexrd 11263 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (π΅β€˜π‘–) ∈ ℝ*)
8584adantlr 713 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (π΅β€˜π‘–) ∈ ℝ*)
8648elixp 8897 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) ↔ (𝑓 Fn 𝑋 ∧ βˆ€π‘– ∈ 𝑋 (π‘“β€˜π‘–) ∈ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))))
8786biimpi 215 . . . . . . . . . . . . . . . 16 (𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) β†’ (𝑓 Fn 𝑋 ∧ βˆ€π‘– ∈ 𝑋 (π‘“β€˜π‘–) ∈ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))))
8887simprd 496 . . . . . . . . . . . . . . 15 (𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) β†’ βˆ€π‘– ∈ 𝑋 (π‘“β€˜π‘–) ∈ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)))
89 rspa 3245 . . . . . . . . . . . . . . 15 ((βˆ€π‘– ∈ 𝑋 (π‘“β€˜π‘–) ∈ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)))
9088, 89sylan 580 . . . . . . . . . . . . . 14 ((𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)))
9190adantll 712 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)))
92 icogelb 13374 . . . . . . . . . . . . 13 (((π΄β€˜π‘–) ∈ ℝ* ∧ (π΅β€˜π‘–) ∈ ℝ* ∧ (π‘“β€˜π‘–) ∈ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) β†’ (π΄β€˜π‘–) ≀ (π‘“β€˜π‘–))
9383, 85, 91, 92syl3anc 1371 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (π΄β€˜π‘–) ≀ (π‘“β€˜π‘–))
9469adantlr 713 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (π΄β€˜π‘–) ∈ ℝ)
95 icossre 13404 . . . . . . . . . . . . . . . 16 (((π΄β€˜π‘–) ∈ ℝ ∧ (π΅β€˜π‘–) ∈ ℝ*) β†’ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) βŠ† ℝ)
9669, 84, 95syl2anc 584 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) βŠ† ℝ)
9796adantlr 713 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) βŠ† ℝ)
9897, 91sseldd 3983 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ℝ)
9994, 98lenltd 11359 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ ((π΄β€˜π‘–) ≀ (π‘“β€˜π‘–) ↔ Β¬ (π‘“β€˜π‘–) < (π΄β€˜π‘–)))
10093, 99mpbid 231 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ Β¬ (π‘“β€˜π‘–) < (π΄β€˜π‘–))
101100adantr 481 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) β†’ Β¬ (π‘“β€˜π‘–) < (π΄β€˜π‘–))
10282, 101pm2.65da 815 . . . . . . . . 9 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ Β¬ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))
10366, 102eldifd 3959 . . . . . . . 8 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))))
104103ex 413 . . . . . . 7 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) β†’ (𝑖 ∈ 𝑋 β†’ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))))
1055, 104ralrimi 3254 . . . . . 6 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) β†’ βˆ€π‘– ∈ 𝑋 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))))
106 eliin 5002 . . . . . . 7 (𝑓 ∈ V β†’ (𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) ↔ βˆ€π‘– ∈ 𝑋 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))))
10748, 106ax-mp 5 . . . . . 6 (𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) ↔ βˆ€π‘– ∈ 𝑋 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))))
108105, 107sylibr 233 . . . . 5 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))) β†’ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))))
109108ex 413 . . . 4 (πœ‘ β†’ (𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) β†’ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))))
110 hspdifhsp.n . . . . . . . . . 10 (πœ‘ β†’ 𝑋 β‰  βˆ…)
111 n0 4346 . . . . . . . . . . 11 (𝑋 β‰  βˆ… ↔ βˆƒπ‘˜ π‘˜ ∈ 𝑋)
112111biimpi 215 . . . . . . . . . 10 (𝑋 β‰  βˆ… β†’ βˆƒπ‘˜ π‘˜ ∈ 𝑋)
113110, 112syl 17 . . . . . . . . 9 (πœ‘ β†’ βˆƒπ‘˜ π‘˜ ∈ 𝑋)
114113adantr 481 . . . . . . . 8 ((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) β†’ βˆƒπ‘˜ π‘˜ ∈ 𝑋)
115 simpl 483 . . . . . . . . . . . . . . 15 ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) ∧ π‘˜ ∈ 𝑋) β†’ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))))
116 simpr 485 . . . . . . . . . . . . . . 15 ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) ∧ π‘˜ ∈ 𝑋) β†’ π‘˜ ∈ 𝑋)
117 id 22 . . . . . . . . . . . . . . . . . 18 (𝑖 = π‘˜ β†’ 𝑖 = π‘˜)
118117, 32oveq12d 7426 . . . . . . . . . . . . . . . . 17 (𝑖 = π‘˜ β†’ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) = (π‘˜(π»β€˜π‘‹)(π΅β€˜π‘˜)))
119117, 31oveq12d 7426 . . . . . . . . . . . . . . . . 17 (𝑖 = π‘˜ β†’ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)) = (π‘˜(π»β€˜π‘‹)(π΄β€˜π‘˜)))
120118, 119difeq12d 4123 . . . . . . . . . . . . . . . 16 (𝑖 = π‘˜ β†’ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) = ((π‘˜(π»β€˜π‘‹)(π΅β€˜π‘˜)) βˆ– (π‘˜(π»β€˜π‘‹)(π΄β€˜π‘˜))))
121120eleq2d 2819 . . . . . . . . . . . . . . 15 (𝑖 = π‘˜ β†’ (𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) ↔ 𝑓 ∈ ((π‘˜(π»β€˜π‘‹)(π΅β€˜π‘˜)) βˆ– (π‘˜(π»β€˜π‘‹)(π΄β€˜π‘˜)))))
122115, 116, 121eliind 43748 . . . . . . . . . . . . . 14 ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) ∧ π‘˜ ∈ 𝑋) β†’ 𝑓 ∈ ((π‘˜(π»β€˜π‘‹)(π΅β€˜π‘˜)) βˆ– (π‘˜(π»β€˜π‘‹)(π΄β€˜π‘˜))))
123122eldifad 3960 . . . . . . . . . . . . 13 ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) ∧ π‘˜ ∈ 𝑋) β†’ 𝑓 ∈ (π‘˜(π»β€˜π‘‹)(π΅β€˜π‘˜)))
124123adantll 712 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ π‘˜ ∈ 𝑋) β†’ 𝑓 ∈ (π‘˜(π»β€˜π‘‹)(π΅β€˜π‘˜)))
125 equequ1 2028 . . . . . . . . . . . . . . . . . . 19 (𝑖 = β„Ž β†’ (𝑖 = 𝑙 ↔ β„Ž = 𝑙))
126125ifbid 4551 . . . . . . . . . . . . . . . . . 18 (𝑖 = β„Ž β†’ if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = if(β„Ž = 𝑙, (-∞(,)𝑦), ℝ))
127126cbvixpv 8908 . . . . . . . . . . . . . . . . 17 X𝑖 ∈ π‘₯ if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = Xβ„Ž ∈ π‘₯ if(β„Ž = 𝑙, (-∞(,)𝑦), ℝ)
128127a1i 11 . . . . . . . . . . . . . . . 16 ((𝑙 ∈ π‘₯ ∧ 𝑦 ∈ ℝ) β†’ X𝑖 ∈ π‘₯ if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = Xβ„Ž ∈ π‘₯ if(β„Ž = 𝑙, (-∞(,)𝑦), ℝ))
129128mpoeq3ia 7486 . . . . . . . . . . . . . . 15 (𝑙 ∈ π‘₯, 𝑦 ∈ ℝ ↦ X𝑖 ∈ π‘₯ if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ)) = (𝑙 ∈ π‘₯, 𝑦 ∈ ℝ ↦ Xβ„Ž ∈ π‘₯ if(β„Ž = 𝑙, (-∞(,)𝑦), ℝ))
130129mpteq2i 5253 . . . . . . . . . . . . . 14 (π‘₯ ∈ Fin ↦ (𝑙 ∈ π‘₯, 𝑦 ∈ ℝ ↦ X𝑖 ∈ π‘₯ if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ))) = (π‘₯ ∈ Fin ↦ (𝑙 ∈ π‘₯, 𝑦 ∈ ℝ ↦ Xβ„Ž ∈ π‘₯ if(β„Ž = 𝑙, (-∞(,)𝑦), ℝ)))
13151, 130eqtri 2760 . . . . . . . . . . . . 13 𝐻 = (π‘₯ ∈ Fin ↦ (𝑙 ∈ π‘₯, 𝑦 ∈ ℝ ↦ Xβ„Ž ∈ π‘₯ if(β„Ž = 𝑙, (-∞(,)𝑦), ℝ)))
13259ad2antrr 724 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ π‘˜ ∈ 𝑋) β†’ 𝑋 ∈ Fin)
133 simpr 485 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ π‘˜ ∈ 𝑋) β†’ π‘˜ ∈ 𝑋)
13421adantlr 713 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ π‘˜ ∈ 𝑋) β†’ (π΅β€˜π‘˜) ∈ ℝ)
135131, 132, 133, 134hspval 45315 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ π‘˜ ∈ 𝑋) β†’ (π‘˜(π»β€˜π‘‹)(π΅β€˜π‘˜)) = Xβ„Ž ∈ 𝑋 if(β„Ž = π‘˜, (-∞(,)(π΅β€˜π‘˜)), ℝ))
136124, 135eleqtrd 2835 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ π‘˜ ∈ 𝑋) β†’ 𝑓 ∈ Xβ„Ž ∈ 𝑋 if(β„Ž = π‘˜, (-∞(,)(π΅β€˜π‘˜)), ℝ))
137 ixpfn 8896 . . . . . . . . . . 11 (𝑓 ∈ Xβ„Ž ∈ 𝑋 if(β„Ž = π‘˜, (-∞(,)(π΅β€˜π‘˜)), ℝ) β†’ 𝑓 Fn 𝑋)
138136, 137syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ π‘˜ ∈ 𝑋) β†’ 𝑓 Fn 𝑋)
139138ex 413 . . . . . . . . 9 ((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) β†’ (π‘˜ ∈ 𝑋 β†’ 𝑓 Fn 𝑋))
140139exlimdv 1936 . . . . . . . 8 ((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) β†’ (βˆƒπ‘˜ π‘˜ ∈ 𝑋 β†’ 𝑓 Fn 𝑋))
141114, 140mpd 15 . . . . . . 7 ((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) β†’ 𝑓 Fn 𝑋)
142 nfii1 5032 . . . . . . . . . 10 β„²π‘–βˆ© 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))
1432, 142nfel 2917 . . . . . . . . 9 Ⅎ𝑖 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))
1441, 143nfan 1902 . . . . . . . 8 Ⅎ𝑖(πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))))
145 simpll 765 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ πœ‘)
146107biimpi 215 . . . . . . . . . . . . 13 (𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) β†’ βˆ€π‘– ∈ 𝑋 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))))
147146adantr 481 . . . . . . . . . . . 12 ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ βˆ€π‘– ∈ 𝑋 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))))
148 simpr 485 . . . . . . . . . . . 12 ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑖 ∈ 𝑋)
149 rspa 3245 . . . . . . . . . . . 12 ((βˆ€π‘– ∈ 𝑋 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))))
150147, 148, 149syl2anc 584 . . . . . . . . . . 11 ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))))
151150adantll 712 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))))
152 simpr 485 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑖 ∈ 𝑋)
15370adantlr 713 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ (π΄β€˜π‘–) ∈ ℝ*)
15484adantlr 713 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ (π΅β€˜π‘–) ∈ ℝ*)
155 simpll 765 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ πœ‘)
156 eldifi 4126 . . . . . . . . . . . . . 14 (𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) β†’ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)))
157156ad2antlr 725 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)))
158 simpr 485 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑖 ∈ 𝑋)
159 ioossre 13384 . . . . . . . . . . . . . 14 (-∞(,)(π΅β€˜π‘–)) βŠ† ℝ
160 simplr 767 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)))
16164adantlr 713 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) = Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
162160, 161eleqtrd 2835 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
163 simpr 485 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑖 ∈ 𝑋)
16410fvixp 8895 . . . . . . . . . . . . . . 15 ((𝑓 ∈ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ (-∞(,)(π΅β€˜π‘–)))
165162, 163, 164syl2anc 584 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ (-∞(,)(π΅β€˜π‘–)))
166159, 165sselid 3980 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ℝ)
167155, 157, 158, 166syl21anc 836 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ℝ)
168167rexrd 11263 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ℝ*)
169 simpl 483 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) β†’ πœ‘)
170156adantl 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) β†’ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)))
171169, 170jca 512 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) β†’ (πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))))
172171ad2antrr 724 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ (πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))))
173 simplr 767 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ 𝑖 ∈ 𝑋)
174 simpr 485 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ (π‘“β€˜π‘–) < (π΄β€˜π‘–))
175 ixpfn 8896 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ) β†’ 𝑓 Fn 𝑋)
176162, 175syl 17 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑓 Fn 𝑋)
177176adantr 481 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ 𝑓 Fn 𝑋)
178 fveq2 6891 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘˜ = 𝑖 β†’ (π‘“β€˜π‘˜) = (π‘“β€˜π‘–))
179178adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) ∧ π‘˜ = 𝑖) β†’ (π‘“β€˜π‘˜) = (π‘“β€˜π‘–))
18018a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ -∞ ∈ ℝ*)
18170ad4ant13 749 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ (π΄β€˜π‘–) ∈ ℝ*)
182166adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ (π‘“β€˜π‘–) ∈ ℝ)
183182mnfltd 13103 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ -∞ < (π‘“β€˜π‘–))
184 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ (π‘“β€˜π‘–) < (π΄β€˜π‘–))
185180, 181, 182, 183, 184eliood 44201 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ (π‘“β€˜π‘–) ∈ (-∞(,)(π΄β€˜π‘–)))
186185adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) ∧ π‘˜ = 𝑖) β†’ (π‘“β€˜π‘–) ∈ (-∞(,)(π΄β€˜π‘–)))
187179, 186eqeltrd 2833 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) ∧ π‘˜ = 𝑖) β†’ (π‘“β€˜π‘˜) ∈ (-∞(,)(π΄β€˜π‘–)))
188187adantlr 713 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝑖) β†’ (π‘“β€˜π‘˜) ∈ (-∞(,)(π΄β€˜π‘–)))
18977eqcomd 2738 . . . . . . . . . . . . . . . . . . . . 21 (π‘˜ = 𝑖 β†’ (-∞(,)(π΄β€˜π‘–)) = if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ))
190189adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝑖) β†’ (-∞(,)(π΄β€˜π‘–)) = if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ))
191188, 190eleqtrd 2835 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) ∧ π‘˜ ∈ 𝑋) ∧ π‘˜ = 𝑖) β†’ (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ))
19210, 159eqsstrdi 4036 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘˜ = 𝑖 β†’ if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ) βŠ† ℝ)
193 ssid 4004 . . . . . . . . . . . . . . . . . . . . . . . . 25 ℝ βŠ† ℝ
19415, 193eqsstrdi 4036 . . . . . . . . . . . . . . . . . . . . . . . 24 (Β¬ π‘˜ = 𝑖 β†’ if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ) βŠ† ℝ)
195192, 194pm2.61i 182 . . . . . . . . . . . . . . . . . . . . . . 23 if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ) βŠ† ℝ
196162adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ π‘˜ ∈ 𝑋) β†’ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
197 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ π‘˜ ∈ 𝑋) β†’ π‘˜ ∈ 𝑋)
198 fvixp2 43888 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓 ∈ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
199196, 197, 198syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝑖, (-∞(,)(π΅β€˜π‘–)), ℝ))
200195, 199sselid 3980 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ ℝ)
201200adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ π‘˜ ∈ 𝑋) ∧ Β¬ π‘˜ = 𝑖) β†’ (π‘“β€˜π‘˜) ∈ ℝ)
202 iffalse 4537 . . . . . . . . . . . . . . . . . . . . . . 23 (Β¬ π‘˜ = 𝑖 β†’ if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ) = ℝ)
203202eqcomd 2738 . . . . . . . . . . . . . . . . . . . . . 22 (Β¬ π‘˜ = 𝑖 β†’ ℝ = if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ))
204203adantl 482 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ π‘˜ ∈ 𝑋) ∧ Β¬ π‘˜ = 𝑖) β†’ ℝ = if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ))
205201, 204eleqtrd 2835 . . . . . . . . . . . . . . . . . . . 20 (((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ π‘˜ ∈ 𝑋) ∧ Β¬ π‘˜ = 𝑖) β†’ (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ))
206205adantllr 717 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) ∧ π‘˜ ∈ 𝑋) ∧ Β¬ π‘˜ = 𝑖) β†’ (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ))
207191, 206pm2.61dan 811 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) ∧ π‘˜ ∈ 𝑋) β†’ (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ))
208207ralrimiva 3146 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ))
209177, 208jca 512 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ (𝑓 Fn 𝑋 ∧ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ)))
21048elixp 8897 . . . . . . . . . . . . . . . 16 (𝑓 ∈ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ) ↔ (𝑓 Fn 𝑋 ∧ βˆ€π‘˜ ∈ 𝑋 (π‘“β€˜π‘˜) ∈ if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ)))
211209, 210sylibr 233 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ 𝑓 ∈ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ))
21273eqcomd 2738 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ) = (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))
213212ad4ant13 749 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ Xπ‘˜ ∈ 𝑋 if(π‘˜ = 𝑖, (-∞(,)(π΄β€˜π‘–)), ℝ) = (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))
214211, 213eleqtrd 2835 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))
215172, 173, 174, 214syl21anc 836 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))
216 eldifn 4127 . . . . . . . . . . . . . 14 (𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) β†’ Β¬ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))
217216ad3antlr 729 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) ∧ (π‘“β€˜π‘–) < (π΄β€˜π‘–)) β†’ Β¬ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))
218215, 217pm2.65da 815 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ Β¬ (π‘“β€˜π‘–) < (π΄β€˜π‘–))
219155, 158, 69syl2anc 584 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ (π΄β€˜π‘–) ∈ ℝ)
220219, 167lenltd 11359 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ ((π΄β€˜π‘–) ≀ (π‘“β€˜π‘–) ↔ Β¬ (π‘“β€˜π‘–) < (π΄β€˜π‘–)))
221218, 220mpbird 256 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ (π΄β€˜π‘–) ≀ (π‘“β€˜π‘–))
22218a1i 11 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ -∞ ∈ ℝ*)
22384adantlr 713 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (π΅β€˜π‘–) ∈ ℝ*)
224 iooltub 44213 . . . . . . . . . . . . 13 ((-∞ ∈ ℝ* ∧ (π΅β€˜π‘–) ∈ ℝ* ∧ (π‘“β€˜π‘–) ∈ (-∞(,)(π΅β€˜π‘–))) β†’ (π‘“β€˜π‘–) < (π΅β€˜π‘–))
225222, 223, 165, 224syl3anc 1371 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 ∈ (𝑖(π»β€˜π‘‹)(π΅β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) < (π΅β€˜π‘–))
226155, 157, 158, 225syl21anc 836 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) < (π΅β€˜π‘–))
227153, 154, 168, 221, 226elicod 13373 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)))
228145, 151, 152, 227syl21anc 836 . . . . . . . . 9 (((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)))
229228ex 413 . . . . . . . 8 ((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) β†’ (𝑖 ∈ 𝑋 β†’ (π‘“β€˜π‘–) ∈ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))))
230144, 229ralrimi 3254 . . . . . . 7 ((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) β†’ βˆ€π‘– ∈ 𝑋 (π‘“β€˜π‘–) ∈ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)))
231141, 230jca 512 . . . . . 6 ((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) β†’ (𝑓 Fn 𝑋 ∧ βˆ€π‘– ∈ 𝑋 (π‘“β€˜π‘–) ∈ ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))))
232231, 86sylibr 233 . . . . 5 ((πœ‘ ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))) β†’ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)))
233232ex 413 . . . 4 (πœ‘ β†’ (𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) β†’ 𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–))))
234109, 233impbid 211 . . 3 (πœ‘ β†’ (𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) ↔ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))))
235234alrimiv 1930 . 2 (πœ‘ β†’ βˆ€π‘“(𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) ↔ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))))
236 dfcleq 2725 . 2 (X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) = ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))) ↔ βˆ€π‘“(𝑓 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) ↔ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–)))))
237235, 236sylibr 233 1 (πœ‘ β†’ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)[,)(π΅β€˜π‘–)) = ∩ 𝑖 ∈ 𝑋 ((𝑖(π»β€˜π‘‹)(π΅β€˜π‘–)) βˆ– (𝑖(π»β€˜π‘‹)(π΄β€˜π‘–))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396  βˆ€wal 1539   = wceq 1541  βˆƒwex 1781   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  Vcvv 3474   βˆ– cdif 3945   βŠ† wss 3948  βˆ…c0 4322  ifcif 4528  βˆ© ciin 4998   class class class wbr 5148   ↦ cmpt 5231   Fn wfn 6538  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7408   ∈ cmpo 7410  Xcixp 8890  Fincfn 8938  β„cr 11108  -∞cmnf 11245  β„*cxr 11246   < clt 11247   ≀ cle 11248  (,)cioo 13323  [,)cico 13325
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-cnex 11165  ax-resscn 11166  ax-pre-lttri 11183  ax-pre-lttrn 11184
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7411  df-oprab 7412  df-mpo 7413  df-1st 7974  df-2nd 7975  df-er 8702  df-ixp 8891  df-en 8939  df-dom 8940  df-sdom 8941  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-ioo 13327  df-ico 13329
This theorem is referenced by:  hoimbllem  45336
  Copyright terms: Public domain W3C validator