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

Theorem ioorrnopnxrlem 44649
Description: Given a point 𝐹 that belongs to an indexed product of (possibly unbounded) open intervals, then 𝐹 belongs to an open product of bounded open intervals that's a subset of the original indexed product. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
Hypotheses
Ref Expression
ioorrnopnxrlem.x (πœ‘ β†’ 𝑋 ∈ Fin)
ioorrnopnxrlem.a (πœ‘ β†’ 𝐴:π‘‹βŸΆβ„*)
ioorrnopnxrlem.b (πœ‘ β†’ 𝐡:π‘‹βŸΆβ„*)
ioorrnopnxrlem.f (πœ‘ β†’ 𝐹 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)(,)(π΅β€˜π‘–)))
ioorrnopnxrlem.l 𝐿 = (𝑖 ∈ 𝑋 ↦ if((π΄β€˜π‘–) = -∞, ((πΉβ€˜π‘–) βˆ’ 1), (π΄β€˜π‘–)))
ioorrnopnxrlem.r 𝑅 = (𝑖 ∈ 𝑋 ↦ if((π΅β€˜π‘–) = +∞, ((πΉβ€˜π‘–) + 1), (π΅β€˜π‘–)))
ioorrnopnxrlem.v 𝑉 = X𝑖 ∈ 𝑋 ((πΏβ€˜π‘–)(,)(π‘…β€˜π‘–))
Assertion
Ref Expression
ioorrnopnxrlem (πœ‘ β†’ βˆƒπ‘£ ∈ (TopOpenβ€˜(ℝ^β€˜π‘‹))(𝐹 ∈ 𝑣 ∧ 𝑣 βŠ† X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)(,)(π΅β€˜π‘–))))
Distinct variable groups:   𝑣,𝐴   𝑣,𝐡   𝑖,𝐹,𝑣   𝑖,𝐿   𝑅,𝑖   𝑣,𝑉   𝑖,𝑋,𝑣   πœ‘,𝑖
Allowed substitution hints:   πœ‘(𝑣)   𝐴(𝑖)   𝐡(𝑖)   𝑅(𝑣)   𝐿(𝑣)   𝑉(𝑖)

Proof of Theorem ioorrnopnxrlem
StepHypRef Expression
1 ioorrnopnxrlem.v . . . 4 𝑉 = X𝑖 ∈ 𝑋 ((πΏβ€˜π‘–)(,)(π‘…β€˜π‘–))
21a1i 11 . . 3 (πœ‘ β†’ 𝑉 = X𝑖 ∈ 𝑋 ((πΏβ€˜π‘–)(,)(π‘…β€˜π‘–)))
3 ioorrnopnxrlem.x . . . 4 (πœ‘ β†’ 𝑋 ∈ Fin)
4 iftrue 4498 . . . . . . . 8 ((π΄β€˜π‘–) = -∞ β†’ if((π΄β€˜π‘–) = -∞, ((πΉβ€˜π‘–) βˆ’ 1), (π΄β€˜π‘–)) = ((πΉβ€˜π‘–) βˆ’ 1))
54adantl 483 . . . . . . 7 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΄β€˜π‘–) = -∞) β†’ if((π΄β€˜π‘–) = -∞, ((πΉβ€˜π‘–) βˆ’ 1), (π΄β€˜π‘–)) = ((πΉβ€˜π‘–) βˆ’ 1))
6 ioorrnopnxrlem.f . . . . . . . . . . . 12 (πœ‘ β†’ 𝐹 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)(,)(π΅β€˜π‘–)))
76adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ 𝐹 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)(,)(π΅β€˜π‘–)))
8 simpr 486 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ 𝑖 ∈ 𝑋)
9 fvixp2 43523 . . . . . . . . . . 11 ((𝐹 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)(,)(π΅β€˜π‘–)) ∧ 𝑖 ∈ 𝑋) β†’ (πΉβ€˜π‘–) ∈ ((π΄β€˜π‘–)(,)(π΅β€˜π‘–)))
107, 8, 9syl2anc 585 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (πΉβ€˜π‘–) ∈ ((π΄β€˜π‘–)(,)(π΅β€˜π‘–)))
1110elioored 43889 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (πΉβ€˜π‘–) ∈ ℝ)
12 1red 11166 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ 1 ∈ ℝ)
1311, 12resubcld 11593 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ ((πΉβ€˜π‘–) βˆ’ 1) ∈ ℝ)
1413adantr 482 . . . . . . 7 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΄β€˜π‘–) = -∞) β†’ ((πΉβ€˜π‘–) βˆ’ 1) ∈ ℝ)
155, 14eqeltrd 2833 . . . . . 6 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΄β€˜π‘–) = -∞) β†’ if((π΄β€˜π‘–) = -∞, ((πΉβ€˜π‘–) βˆ’ 1), (π΄β€˜π‘–)) ∈ ℝ)
16 iffalse 4501 . . . . . . . 8 (Β¬ (π΄β€˜π‘–) = -∞ β†’ if((π΄β€˜π‘–) = -∞, ((πΉβ€˜π‘–) βˆ’ 1), (π΄β€˜π‘–)) = (π΄β€˜π‘–))
1716adantl 483 . . . . . . 7 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ Β¬ (π΄β€˜π‘–) = -∞) β†’ if((π΄β€˜π‘–) = -∞, ((πΉβ€˜π‘–) βˆ’ 1), (π΄β€˜π‘–)) = (π΄β€˜π‘–))
18 neqne 2948 . . . . . . . . 9 (Β¬ (π΄β€˜π‘–) = -∞ β†’ (π΄β€˜π‘–) β‰  -∞)
1918adantl 483 . . . . . . . 8 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ Β¬ (π΄β€˜π‘–) = -∞) β†’ (π΄β€˜π‘–) β‰  -∞)
20 ioorrnopnxrlem.a . . . . . . . . . . 11 (πœ‘ β†’ 𝐴:π‘‹βŸΆβ„*)
2120ffvelcdmda 7041 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (π΄β€˜π‘–) ∈ ℝ*)
2221adantr 482 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΄β€˜π‘–) β‰  -∞) β†’ (π΄β€˜π‘–) ∈ ℝ*)
23 simpr 486 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΄β€˜π‘–) β‰  -∞) β†’ (π΄β€˜π‘–) β‰  -∞)
24 pnfxr 11219 . . . . . . . . . . . 12 +∞ ∈ ℝ*
2524a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ +∞ ∈ ℝ*)
2611rexrd 11215 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (πΉβ€˜π‘–) ∈ ℝ*)
27 ioorrnopnxrlem.b . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐡:π‘‹βŸΆβ„*)
2827ffvelcdmda 7041 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (π΅β€˜π‘–) ∈ ℝ*)
29 ioogtlb 43835 . . . . . . . . . . . . 13 (((π΄β€˜π‘–) ∈ ℝ* ∧ (π΅β€˜π‘–) ∈ ℝ* ∧ (πΉβ€˜π‘–) ∈ ((π΄β€˜π‘–)(,)(π΅β€˜π‘–))) β†’ (π΄β€˜π‘–) < (πΉβ€˜π‘–))
3021, 28, 10, 29syl3anc 1372 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (π΄β€˜π‘–) < (πΉβ€˜π‘–))
3111ltpnfd 13052 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (πΉβ€˜π‘–) < +∞)
3221, 26, 25, 30, 31xrlttrd 13089 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (π΄β€˜π‘–) < +∞)
3321, 25, 32xrltned 43694 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (π΄β€˜π‘–) β‰  +∞)
3433adantr 482 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΄β€˜π‘–) β‰  -∞) β†’ (π΄β€˜π‘–) β‰  +∞)
3522, 23, 34xrred 43702 . . . . . . . 8 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΄β€˜π‘–) β‰  -∞) β†’ (π΄β€˜π‘–) ∈ ℝ)
3619, 35syldan 592 . . . . . . 7 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ Β¬ (π΄β€˜π‘–) = -∞) β†’ (π΄β€˜π‘–) ∈ ℝ)
3717, 36eqeltrd 2833 . . . . . 6 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ Β¬ (π΄β€˜π‘–) = -∞) β†’ if((π΄β€˜π‘–) = -∞, ((πΉβ€˜π‘–) βˆ’ 1), (π΄β€˜π‘–)) ∈ ℝ)
3815, 37pm2.61dan 812 . . . . 5 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ if((π΄β€˜π‘–) = -∞, ((πΉβ€˜π‘–) βˆ’ 1), (π΄β€˜π‘–)) ∈ ℝ)
39 ioorrnopnxrlem.l . . . . 5 𝐿 = (𝑖 ∈ 𝑋 ↦ if((π΄β€˜π‘–) = -∞, ((πΉβ€˜π‘–) βˆ’ 1), (π΄β€˜π‘–)))
4038, 39fmptd 7068 . . . 4 (πœ‘ β†’ 𝐿:π‘‹βŸΆβ„)
41 iftrue 4498 . . . . . . . 8 ((π΅β€˜π‘–) = +∞ β†’ if((π΅β€˜π‘–) = +∞, ((πΉβ€˜π‘–) + 1), (π΅β€˜π‘–)) = ((πΉβ€˜π‘–) + 1))
4241adantl 483 . . . . . . 7 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΅β€˜π‘–) = +∞) β†’ if((π΅β€˜π‘–) = +∞, ((πΉβ€˜π‘–) + 1), (π΅β€˜π‘–)) = ((πΉβ€˜π‘–) + 1))
4311, 12readdcld 11194 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ ((πΉβ€˜π‘–) + 1) ∈ ℝ)
4443adantr 482 . . . . . . 7 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΅β€˜π‘–) = +∞) β†’ ((πΉβ€˜π‘–) + 1) ∈ ℝ)
4542, 44eqeltrd 2833 . . . . . 6 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΅β€˜π‘–) = +∞) β†’ if((π΅β€˜π‘–) = +∞, ((πΉβ€˜π‘–) + 1), (π΅β€˜π‘–)) ∈ ℝ)
46 iffalse 4501 . . . . . . . 8 (Β¬ (π΅β€˜π‘–) = +∞ β†’ if((π΅β€˜π‘–) = +∞, ((πΉβ€˜π‘–) + 1), (π΅β€˜π‘–)) = (π΅β€˜π‘–))
4746adantl 483 . . . . . . 7 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ Β¬ (π΅β€˜π‘–) = +∞) β†’ if((π΅β€˜π‘–) = +∞, ((πΉβ€˜π‘–) + 1), (π΅β€˜π‘–)) = (π΅β€˜π‘–))
48 neqne 2948 . . . . . . . . 9 (Β¬ (π΅β€˜π‘–) = +∞ β†’ (π΅β€˜π‘–) β‰  +∞)
4948adantl 483 . . . . . . . 8 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ Β¬ (π΅β€˜π‘–) = +∞) β†’ (π΅β€˜π‘–) β‰  +∞)
5028adantr 482 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΅β€˜π‘–) β‰  +∞) β†’ (π΅β€˜π‘–) ∈ ℝ*)
51 mnfxr 11222 . . . . . . . . . . . 12 -∞ ∈ ℝ*
5251a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ -∞ ∈ ℝ*)
5311mnfltd 13055 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ -∞ < (πΉβ€˜π‘–))
54 iooltub 43850 . . . . . . . . . . . . 13 (((π΄β€˜π‘–) ∈ ℝ* ∧ (π΅β€˜π‘–) ∈ ℝ* ∧ (πΉβ€˜π‘–) ∈ ((π΄β€˜π‘–)(,)(π΅β€˜π‘–))) β†’ (πΉβ€˜π‘–) < (π΅β€˜π‘–))
5521, 28, 10, 54syl3anc 1372 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (πΉβ€˜π‘–) < (π΅β€˜π‘–))
5652, 26, 28, 53, 55xrlttrd 13089 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ -∞ < (π΅β€˜π‘–))
5752, 28, 56xrgtned 43659 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (π΅β€˜π‘–) β‰  -∞)
5857adantr 482 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΅β€˜π‘–) β‰  +∞) β†’ (π΅β€˜π‘–) β‰  -∞)
59 simpr 486 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΅β€˜π‘–) β‰  +∞) β†’ (π΅β€˜π‘–) β‰  +∞)
6050, 58, 59xrred 43702 . . . . . . . 8 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΅β€˜π‘–) β‰  +∞) β†’ (π΅β€˜π‘–) ∈ ℝ)
6149, 60syldan 592 . . . . . . 7 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ Β¬ (π΅β€˜π‘–) = +∞) β†’ (π΅β€˜π‘–) ∈ ℝ)
6247, 61eqeltrd 2833 . . . . . 6 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ Β¬ (π΅β€˜π‘–) = +∞) β†’ if((π΅β€˜π‘–) = +∞, ((πΉβ€˜π‘–) + 1), (π΅β€˜π‘–)) ∈ ℝ)
6345, 62pm2.61dan 812 . . . . 5 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ if((π΅β€˜π‘–) = +∞, ((πΉβ€˜π‘–) + 1), (π΅β€˜π‘–)) ∈ ℝ)
64 ioorrnopnxrlem.r . . . . 5 𝑅 = (𝑖 ∈ 𝑋 ↦ if((π΅β€˜π‘–) = +∞, ((πΉβ€˜π‘–) + 1), (π΅β€˜π‘–)))
6563, 64fmptd 7068 . . . 4 (πœ‘ β†’ 𝑅:π‘‹βŸΆβ„)
663, 40, 65ioorrnopn 44648 . . 3 (πœ‘ β†’ X𝑖 ∈ 𝑋 ((πΏβ€˜π‘–)(,)(π‘…β€˜π‘–)) ∈ (TopOpenβ€˜(ℝ^β€˜π‘‹)))
672, 66eqeltrd 2833 . 2 (πœ‘ β†’ 𝑉 ∈ (TopOpenβ€˜(ℝ^β€˜π‘‹)))
686elexd 3467 . . . . . 6 (πœ‘ β†’ 𝐹 ∈ V)
69 ixpfn 8849 . . . . . . 7 (𝐹 ∈ X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)(,)(π΅β€˜π‘–)) β†’ 𝐹 Fn 𝑋)
706, 69syl 17 . . . . . 6 (πœ‘ β†’ 𝐹 Fn 𝑋)
7140ffvelcdmda 7041 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (πΏβ€˜π‘–) ∈ ℝ)
7271rexrd 11215 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (πΏβ€˜π‘–) ∈ ℝ*)
7365ffvelcdmda 7041 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (π‘…β€˜π‘–) ∈ ℝ)
7473rexrd 11215 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (π‘…β€˜π‘–) ∈ ℝ*)
7539a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐿 = (𝑖 ∈ 𝑋 ↦ if((π΄β€˜π‘–) = -∞, ((πΉβ€˜π‘–) βˆ’ 1), (π΄β€˜π‘–))))
7638elexd 3467 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ if((π΄β€˜π‘–) = -∞, ((πΉβ€˜π‘–) βˆ’ 1), (π΄β€˜π‘–)) ∈ V)
7775, 76fvmpt2d 6967 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (πΏβ€˜π‘–) = if((π΄β€˜π‘–) = -∞, ((πΉβ€˜π‘–) βˆ’ 1), (π΄β€˜π‘–)))
7877adantr 482 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΄β€˜π‘–) = -∞) β†’ (πΏβ€˜π‘–) = if((π΄β€˜π‘–) = -∞, ((πΉβ€˜π‘–) βˆ’ 1), (π΄β€˜π‘–)))
7978, 5eqtrd 2772 . . . . . . . . . 10 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΄β€˜π‘–) = -∞) β†’ (πΏβ€˜π‘–) = ((πΉβ€˜π‘–) βˆ’ 1))
8011ltm1d 12097 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ ((πΉβ€˜π‘–) βˆ’ 1) < (πΉβ€˜π‘–))
8180adantr 482 . . . . . . . . . 10 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΄β€˜π‘–) = -∞) β†’ ((πΉβ€˜π‘–) βˆ’ 1) < (πΉβ€˜π‘–))
8279, 81eqbrtrd 5133 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΄β€˜π‘–) = -∞) β†’ (πΏβ€˜π‘–) < (πΉβ€˜π‘–))
8377adantr 482 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ Β¬ (π΄β€˜π‘–) = -∞) β†’ (πΏβ€˜π‘–) = if((π΄β€˜π‘–) = -∞, ((πΉβ€˜π‘–) βˆ’ 1), (π΄β€˜π‘–)))
8483, 17eqtrd 2772 . . . . . . . . . 10 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ Β¬ (π΄β€˜π‘–) = -∞) β†’ (πΏβ€˜π‘–) = (π΄β€˜π‘–))
8530adantr 482 . . . . . . . . . 10 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ Β¬ (π΄β€˜π‘–) = -∞) β†’ (π΄β€˜π‘–) < (πΉβ€˜π‘–))
8684, 85eqbrtrd 5133 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ Β¬ (π΄β€˜π‘–) = -∞) β†’ (πΏβ€˜π‘–) < (πΉβ€˜π‘–))
8782, 86pm2.61dan 812 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (πΏβ€˜π‘–) < (πΉβ€˜π‘–))
8811ltp1d 12095 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (πΉβ€˜π‘–) < ((πΉβ€˜π‘–) + 1))
8988adantr 482 . . . . . . . . . 10 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΅β€˜π‘–) = +∞) β†’ (πΉβ€˜π‘–) < ((πΉβ€˜π‘–) + 1))
9064a1i 11 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑅 = (𝑖 ∈ 𝑋 ↦ if((π΅β€˜π‘–) = +∞, ((πΉβ€˜π‘–) + 1), (π΅β€˜π‘–))))
9163elexd 3467 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ if((π΅β€˜π‘–) = +∞, ((πΉβ€˜π‘–) + 1), (π΅β€˜π‘–)) ∈ V)
9290, 91fvmpt2d 6967 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (π‘…β€˜π‘–) = if((π΅β€˜π‘–) = +∞, ((πΉβ€˜π‘–) + 1), (π΅β€˜π‘–)))
9392adantr 482 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΅β€˜π‘–) = +∞) β†’ (π‘…β€˜π‘–) = if((π΅β€˜π‘–) = +∞, ((πΉβ€˜π‘–) + 1), (π΅β€˜π‘–)))
9493, 42eqtrd 2772 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΅β€˜π‘–) = +∞) β†’ (π‘…β€˜π‘–) = ((πΉβ€˜π‘–) + 1))
9594eqcomd 2738 . . . . . . . . . 10 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΅β€˜π‘–) = +∞) β†’ ((πΉβ€˜π‘–) + 1) = (π‘…β€˜π‘–))
9689, 95breqtrd 5137 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΅β€˜π‘–) = +∞) β†’ (πΉβ€˜π‘–) < (π‘…β€˜π‘–))
9755adantr 482 . . . . . . . . . 10 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ Β¬ (π΅β€˜π‘–) = +∞) β†’ (πΉβ€˜π‘–) < (π΅β€˜π‘–))
9892adantr 482 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ Β¬ (π΅β€˜π‘–) = +∞) β†’ (π‘…β€˜π‘–) = if((π΅β€˜π‘–) = +∞, ((πΉβ€˜π‘–) + 1), (π΅β€˜π‘–)))
9998, 47eqtrd 2772 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ Β¬ (π΅β€˜π‘–) = +∞) β†’ (π‘…β€˜π‘–) = (π΅β€˜π‘–))
10099eqcomd 2738 . . . . . . . . . 10 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ Β¬ (π΅β€˜π‘–) = +∞) β†’ (π΅β€˜π‘–) = (π‘…β€˜π‘–))
10197, 100breqtrd 5137 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ Β¬ (π΅β€˜π‘–) = +∞) β†’ (πΉβ€˜π‘–) < (π‘…β€˜π‘–))
10296, 101pm2.61dan 812 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (πΉβ€˜π‘–) < (π‘…β€˜π‘–))
10372, 74, 11, 87, 102eliood 43838 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (πΉβ€˜π‘–) ∈ ((πΏβ€˜π‘–)(,)(π‘…β€˜π‘–)))
104103ralrimiva 3140 . . . . . 6 (πœ‘ β†’ βˆ€π‘– ∈ 𝑋 (πΉβ€˜π‘–) ∈ ((πΏβ€˜π‘–)(,)(π‘…β€˜π‘–)))
10568, 70, 1043jca 1129 . . . . 5 (πœ‘ β†’ (𝐹 ∈ V ∧ 𝐹 Fn 𝑋 ∧ βˆ€π‘– ∈ 𝑋 (πΉβ€˜π‘–) ∈ ((πΏβ€˜π‘–)(,)(π‘…β€˜π‘–))))
106 elixp2 8847 . . . . 5 (𝐹 ∈ X𝑖 ∈ 𝑋 ((πΏβ€˜π‘–)(,)(π‘…β€˜π‘–)) ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝑋 ∧ βˆ€π‘– ∈ 𝑋 (πΉβ€˜π‘–) ∈ ((πΏβ€˜π‘–)(,)(π‘…β€˜π‘–))))
107105, 106sylibr 233 . . . 4 (πœ‘ β†’ 𝐹 ∈ X𝑖 ∈ 𝑋 ((πΏβ€˜π‘–)(,)(π‘…β€˜π‘–)))
108107, 1eleqtrrdi 2844 . . 3 (πœ‘ β†’ 𝐹 ∈ 𝑉)
10921adantr 482 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΄β€˜π‘–) = -∞) β†’ (π΄β€˜π‘–) ∈ ℝ*)
11072adantr 482 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΄β€˜π‘–) = -∞) β†’ (πΏβ€˜π‘–) ∈ ℝ*)
11115mnfltd 13055 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΄β€˜π‘–) = -∞) β†’ -∞ < if((π΄β€˜π‘–) = -∞, ((πΉβ€˜π‘–) βˆ’ 1), (π΄β€˜π‘–)))
112111, 5breqtrd 5137 . . . . . . . . . 10 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΄β€˜π‘–) = -∞) β†’ -∞ < ((πΉβ€˜π‘–) βˆ’ 1))
113 simpr 486 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΄β€˜π‘–) = -∞) β†’ (π΄β€˜π‘–) = -∞)
114113, 79breq12d 5124 . . . . . . . . . 10 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΄β€˜π‘–) = -∞) β†’ ((π΄β€˜π‘–) < (πΏβ€˜π‘–) ↔ -∞ < ((πΉβ€˜π‘–) βˆ’ 1)))
115112, 114mpbird 257 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΄β€˜π‘–) = -∞) β†’ (π΄β€˜π‘–) < (πΏβ€˜π‘–))
116109, 110, 115xrltled 13080 . . . . . . . 8 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΄β€˜π‘–) = -∞) β†’ (π΄β€˜π‘–) ≀ (πΏβ€˜π‘–))
11784eqcomd 2738 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ Β¬ (π΄β€˜π‘–) = -∞) β†’ (π΄β€˜π‘–) = (πΏβ€˜π‘–))
11836, 117eqled 11268 . . . . . . . 8 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ Β¬ (π΄β€˜π‘–) = -∞) β†’ (π΄β€˜π‘–) ≀ (πΏβ€˜π‘–))
119116, 118pm2.61dan 812 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (π΄β€˜π‘–) ≀ (πΏβ€˜π‘–))
12074adantr 482 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΅β€˜π‘–) = +∞) β†’ (π‘…β€˜π‘–) ∈ ℝ*)
12128adantr 482 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΅β€˜π‘–) = +∞) β†’ (π΅β€˜π‘–) ∈ ℝ*)
12244ltpnfd 13052 . . . . . . . . . 10 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΅β€˜π‘–) = +∞) β†’ ((πΉβ€˜π‘–) + 1) < +∞)
123 simpr 486 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΅β€˜π‘–) = +∞) β†’ (π΅β€˜π‘–) = +∞)
12494, 123breq12d 5124 . . . . . . . . . 10 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΅β€˜π‘–) = +∞) β†’ ((π‘…β€˜π‘–) < (π΅β€˜π‘–) ↔ ((πΉβ€˜π‘–) + 1) < +∞))
125122, 124mpbird 257 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΅β€˜π‘–) = +∞) β†’ (π‘…β€˜π‘–) < (π΅β€˜π‘–))
126120, 121, 125xrltled 13080 . . . . . . . 8 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ (π΅β€˜π‘–) = +∞) β†’ (π‘…β€˜π‘–) ≀ (π΅β€˜π‘–))
12773adantr 482 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ Β¬ (π΅β€˜π‘–) = +∞) β†’ (π‘…β€˜π‘–) ∈ ℝ)
128127, 99eqled 11268 . . . . . . . 8 (((πœ‘ ∧ 𝑖 ∈ 𝑋) ∧ Β¬ (π΅β€˜π‘–) = +∞) β†’ (π‘…β€˜π‘–) ≀ (π΅β€˜π‘–))
129126, 128pm2.61dan 812 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (π‘…β€˜π‘–) ≀ (π΅β€˜π‘–))
130 ioossioo 13369 . . . . . . 7 ((((π΄β€˜π‘–) ∈ ℝ* ∧ (π΅β€˜π‘–) ∈ ℝ*) ∧ ((π΄β€˜π‘–) ≀ (πΏβ€˜π‘–) ∧ (π‘…β€˜π‘–) ≀ (π΅β€˜π‘–))) β†’ ((πΏβ€˜π‘–)(,)(π‘…β€˜π‘–)) βŠ† ((π΄β€˜π‘–)(,)(π΅β€˜π‘–)))
13121, 28, 119, 129, 130syl22anc 838 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ ((πΏβ€˜π‘–)(,)(π‘…β€˜π‘–)) βŠ† ((π΄β€˜π‘–)(,)(π΅β€˜π‘–)))
132131ralrimiva 3140 . . . . 5 (πœ‘ β†’ βˆ€π‘– ∈ 𝑋 ((πΏβ€˜π‘–)(,)(π‘…β€˜π‘–)) βŠ† ((π΄β€˜π‘–)(,)(π΅β€˜π‘–)))
133 ss2ixp 8856 . . . . 5 (βˆ€π‘– ∈ 𝑋 ((πΏβ€˜π‘–)(,)(π‘…β€˜π‘–)) βŠ† ((π΄β€˜π‘–)(,)(π΅β€˜π‘–)) β†’ X𝑖 ∈ 𝑋 ((πΏβ€˜π‘–)(,)(π‘…β€˜π‘–)) βŠ† X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)(,)(π΅β€˜π‘–)))
134132, 133syl 17 . . . 4 (πœ‘ β†’ X𝑖 ∈ 𝑋 ((πΏβ€˜π‘–)(,)(π‘…β€˜π‘–)) βŠ† X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)(,)(π΅β€˜π‘–)))
1352, 134eqsstrd 3986 . . 3 (πœ‘ β†’ 𝑉 βŠ† X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)(,)(π΅β€˜π‘–)))
136108, 135jca 513 . 2 (πœ‘ β†’ (𝐹 ∈ 𝑉 ∧ 𝑉 βŠ† X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)(,)(π΅β€˜π‘–))))
137 eleq2 2822 . . . 4 (𝑣 = 𝑉 β†’ (𝐹 ∈ 𝑣 ↔ 𝐹 ∈ 𝑉))
138 sseq1 3973 . . . 4 (𝑣 = 𝑉 β†’ (𝑣 βŠ† X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)(,)(π΅β€˜π‘–)) ↔ 𝑉 βŠ† X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)(,)(π΅β€˜π‘–))))
139137, 138anbi12d 632 . . 3 (𝑣 = 𝑉 β†’ ((𝐹 ∈ 𝑣 ∧ 𝑣 βŠ† X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)(,)(π΅β€˜π‘–))) ↔ (𝐹 ∈ 𝑉 ∧ 𝑉 βŠ† X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)(,)(π΅β€˜π‘–)))))
140139rspcev 3583 . 2 ((𝑉 ∈ (TopOpenβ€˜(ℝ^β€˜π‘‹)) ∧ (𝐹 ∈ 𝑉 ∧ 𝑉 βŠ† X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)(,)(π΅β€˜π‘–)))) β†’ βˆƒπ‘£ ∈ (TopOpenβ€˜(ℝ^β€˜π‘‹))(𝐹 ∈ 𝑣 ∧ 𝑣 βŠ† X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)(,)(π΅β€˜π‘–))))
14167, 136, 140syl2anc 585 1 (πœ‘ β†’ βˆƒπ‘£ ∈ (TopOpenβ€˜(ℝ^β€˜π‘‹))(𝐹 ∈ 𝑣 ∧ 𝑣 βŠ† X𝑖 ∈ 𝑋 ((π΄β€˜π‘–)(,)(π΅β€˜π‘–))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  Vcvv 3447   βŠ† wss 3914  ifcif 4492   class class class wbr 5111   ↦ cmpt 5194   Fn wfn 6497  βŸΆwf 6498  β€˜cfv 6502  (class class class)co 7363  Xcixp 8843  Fincfn 8891  β„cr 11060  1c1 11062   + caddc 11064  +∞cpnf 11196  -∞cmnf 11197  β„*cxr 11198   < clt 11199   ≀ cle 11200   βˆ’ cmin 11395  (,)cioo 13275  TopOpenctopn 17318  β„^crrx 24785
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 2703  ax-rep 5248  ax-sep 5262  ax-nul 5269  ax-pow 5326  ax-pr 5390  ax-un 7678  ax-inf2 9587  ax-cnex 11117  ax-resscn 11118  ax-1cn 11119  ax-icn 11120  ax-addcl 11121  ax-addrcl 11122  ax-mulcl 11123  ax-mulrcl 11124  ax-mulcom 11125  ax-addass 11126  ax-mulass 11127  ax-distr 11128  ax-i2m1 11129  ax-1ne0 11130  ax-1rid 11131  ax-rnegex 11132  ax-rrecex 11133  ax-cnre 11134  ax-pre-lttri 11135  ax-pre-lttrn 11136  ax-pre-ltadd 11137  ax-pre-mulgt0 11138  ax-pre-sup 11139  ax-addf 11140  ax-mulf 11141
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 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-rmo 3352  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-pss 3933  df-nul 4289  df-if 4493  df-pw 4568  df-sn 4593  df-pr 4595  df-tp 4597  df-op 4599  df-uni 4872  df-int 4914  df-iun 4962  df-br 5112  df-opab 5174  df-mpt 5195  df-tr 5229  df-id 5537  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5594  df-se 5595  df-we 5596  df-xp 5645  df-rel 5646  df-cnv 5647  df-co 5648  df-dm 5649  df-rn 5650  df-res 5651  df-ima 5652  df-pred 6259  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-isom 6511  df-riota 7319  df-ov 7366  df-oprab 7367  df-mpo 7368  df-of 7623  df-om 7809  df-1st 7927  df-2nd 7928  df-supp 8099  df-tpos 8163  df-frecs 8218  df-wrecs 8249  df-recs 8323  df-rdg 8362  df-1o 8418  df-er 8656  df-map 8775  df-ixp 8844  df-en 8892  df-dom 8893  df-sdom 8894  df-fin 8895  df-fsupp 9314  df-sup 9388  df-inf 9389  df-oi 9456  df-card 9885  df-pnf 11201  df-mnf 11202  df-xr 11203  df-ltxr 11204  df-le 11205  df-sub 11397  df-neg 11398  df-div 11823  df-nn 12164  df-2 12226  df-3 12227  df-4 12228  df-5 12229  df-6 12230  df-7 12231  df-8 12232  df-9 12233  df-n0 12424  df-z 12510  df-dec 12629  df-uz 12774  df-q 12884  df-rp 12926  df-xneg 13043  df-xadd 13044  df-xmul 13045  df-ioo 13279  df-ico 13281  df-fz 13436  df-fzo 13579  df-seq 13918  df-exp 13979  df-hash 14242  df-cj 14997  df-re 14998  df-im 14999  df-sqrt 15133  df-abs 15134  df-clim 15383  df-sum 15584  df-struct 17031  df-sets 17048  df-slot 17066  df-ndx 17078  df-base 17096  df-ress 17125  df-plusg 17161  df-mulr 17162  df-starv 17163  df-sca 17164  df-vsca 17165  df-ip 17166  df-tset 17167  df-ple 17168  df-ds 17170  df-unif 17171  df-hom 17172  df-cco 17173  df-rest 17319  df-topn 17320  df-0g 17338  df-gsum 17339  df-topgen 17340  df-prds 17344  df-pws 17346  df-mgm 18512  df-sgrp 18561  df-mnd 18572  df-mhm 18616  df-submnd 18617  df-grp 18766  df-minusg 18767  df-sbg 18768  df-subg 18940  df-ghm 19021  df-cntz 19112  df-cmn 19579  df-abl 19580  df-mgp 19912  df-ur 19929  df-ring 19981  df-cring 19982  df-oppr 20064  df-dvdsr 20085  df-unit 20086  df-invr 20116  df-dvr 20127  df-rnghom 20163  df-drng 20228  df-field 20229  df-subrg 20269  df-abv 20333  df-staf 20361  df-srng 20362  df-lmod 20381  df-lss 20451  df-lmhm 20541  df-lvec 20622  df-sra 20693  df-rgmod 20694  df-psmet 20826  df-xmet 20827  df-met 20828  df-bl 20829  df-mopn 20830  df-cnfld 20835  df-refld 21047  df-phl 21068  df-dsmm 21176  df-frlm 21191  df-top 22281  df-topon 22298  df-topsp 22320  df-bases 22334  df-xms 23711  df-ms 23712  df-nm 23976  df-ngp 23977  df-tng 23978  df-nrg 23979  df-nlm 23980  df-clm 24464  df-cph 24570  df-tcph 24571  df-rrx 24787
This theorem is referenced by:  ioorrnopnxr  44650
  Copyright terms: Public domain W3C validator